src/HOL/Algebra/RingHom.thy
changeset 61382 efac889fccbc
parent 61169 4de9ff3ea29a
child 61565 352c73a689da
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -6,9 +6,9 @@
     1.4  imports Ideal
     1.5  begin
     1.6  
     1.7 -section {* Homomorphisms of Non-Commutative Rings *}
     1.8 +section \<open>Homomorphisms of Non-Commutative Rings\<close>
     1.9  
    1.10 -text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
    1.11 +text \<open>Lifting existing lemmas in a @{text ring_hom_ring} locale\<close>
    1.12  locale ring_hom_ring = R: ring R + S: ring S
    1.13      for R (structure) and S (structure) +
    1.14    fixes h
    1.15 @@ -100,7 +100,7 @@
    1.16  qed
    1.17  
    1.18  
    1.19 -subsection {* The Kernel of a Ring Homomorphism *}
    1.20 +subsection \<open>The Kernel of a Ring Homomorphism\<close>
    1.21  
    1.22  --"the kernel of a ring homomorphism is an ideal"
    1.23  lemma (in ring_hom_ring) kernel_is_ideal:
    1.24 @@ -111,15 +111,15 @@
    1.25   apply (unfold a_kernel_def', simp+)
    1.26  done
    1.27  
    1.28 -text {* Elements of the kernel are mapped to zero *}
    1.29 +text \<open>Elements of the kernel are mapped to zero\<close>
    1.30  lemma (in abelian_group_hom) kernel_zero [simp]:
    1.31    "i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
    1.32  by (simp add: a_kernel_defs)
    1.33  
    1.34  
    1.35 -subsection {* Cosets *}
    1.36 +subsection \<open>Cosets\<close>
    1.37  
    1.38 -text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
    1.39 +text \<open>Cosets of the kernel correspond to the elements of the image of the homomorphism\<close>
    1.40  lemma (in ring_hom_ring) rcos_imp_homeq:
    1.41    assumes acarr: "a \<in> carrier R"
    1.42        and xrcos: "x \<in> a_kernel R S h +> a"