changeset 35849 | b5522b51cb1e |
parent 30729 | 461ee3e49ad3 |
child 44655 | fe0365331566 |
--- a/src/HOL/Algebra/RingHom.thy Sun Mar 21 16:51:37 2010 +0100 +++ b/src/HOL/Algebra/RingHom.thy Sun Mar 21 17:12:31 2010 +0100 @@ -1,6 +1,5 @@ -(* - Title: HOL/Algebra/RingHom.thy - Author: Stephan Hohe, TU Muenchen +(* Title: HOL/Algebra/RingHom.thy + Author: Stephan Hohe, TU Muenchen *) theory RingHom @@ -100,6 +99,7 @@ (rule R.is_cring, rule S.is_cring, rule homh) qed + subsection {* The Kernel of a Ring Homomorphism *} --"the kernel of a ring homomorphism is an ideal"