| changeset 67443 | 3abf6a722518 |
| parent 63167 | 0909deb8059b |
| child 67613 | ce654b0e6d69 |
--- a/src/HOL/Algebra/RingHom.thy Tue Jan 16 09:12:16 2018 +0100 +++ b/src/HOL/Algebra/RingHom.thy Tue Jan 16 09:30:00 2018 +0100 @@ -102,7 +102,7 @@ subsection \<open>The Kernel of a Ring Homomorphism\<close> -\<comment>"the kernel of a ring homomorphism is an ideal" +\<comment> \<open>the kernel of a ring homomorphism is an ideal\<close> lemma (in ring_hom_ring) kernel_is_ideal: shows "ideal (a_kernel R S h) R" apply (rule idealI)