equal
deleted
inserted
replaced
100 qed |
100 qed |
101 |
101 |
102 |
102 |
103 subsection \<open>The Kernel of a Ring Homomorphism\<close> |
103 subsection \<open>The Kernel of a Ring Homomorphism\<close> |
104 |
104 |
105 \<comment>"the kernel of a ring homomorphism is an ideal" |
105 \<comment> \<open>the kernel of a ring homomorphism is an ideal\<close> |
106 lemma (in ring_hom_ring) kernel_is_ideal: |
106 lemma (in ring_hom_ring) kernel_is_ideal: |
107 shows "ideal (a_kernel R S h) R" |
107 shows "ideal (a_kernel R S h) R" |
108 apply (rule idealI) |
108 apply (rule idealI) |
109 apply (rule R.is_ring) |
109 apply (rule R.is_ring) |
110 apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel]) |
110 apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel]) |