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.7 -section {* Homomorphisms of Non-Commutative Rings *}
1.8 +section \<open>Homomorphisms of Non-Commutative Rings\<close>
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.19 -subsection {* The Kernel of a Ring Homomorphism *}
1.20 +subsection \<open>The Kernel of a Ring Homomorphism\<close>
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.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.35 -subsection {* Cosets *}
1.36 +subsection \<open>Cosets\<close>
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"