changeset 27717 | 21bbd410ba04 |
parent 27611 | 2c01c0bdb385 |
child 28823 | dcbef866c9e2 |
--- a/src/HOL/Algebra/RingHom.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/RingHom.thy Fri Aug 01 18:10:52 2008 +0200 @@ -99,7 +99,7 @@ (rule R.is_cring, rule S.is_cring, rule homh) qed -subsection {* The kernel of a ring homomorphism *} +subsection {* The Kernel of a Ring Homomorphism *} --"the kernel of a ring homomorphism is an ideal" lemma (in ring_hom_ring) kernel_is_ideal: