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>"