src/HOL/Algebra/RingHom.thy
changeset 67613 ce654b0e6d69
parent 67443 3abf6a722518
child 68551 b680e74eb6f2
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -39,8 +39,8 @@
     1.4    assumes "ring R" "ring S"
     1.5    assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
     1.6            hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
     1.7 -      and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
     1.8 -      and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
     1.9 +      and compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    1.10 +      and compatible_add: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
    1.11        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    1.12    shows "ring_hom_ring R S h"
    1.13  proof -
    1.14 @@ -72,7 +72,7 @@
    1.15  lemma ring_hom_ringI3:
    1.16    fixes R (structure) and S (structure)
    1.17    assumes "abelian_group_hom R S h" "ring R" "ring S" 
    1.18 -  assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    1.19 +  assumes compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    1.20        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    1.21    shows "ring_hom_ring R S h"
    1.22  proof -