equal
deleted
inserted
replaced
6 imports Ideal |
6 imports Ideal |
7 begin |
7 begin |
8 |
8 |
9 section \<open>Homomorphisms of Non-Commutative Rings\<close> |
9 section \<open>Homomorphisms of Non-Commutative Rings\<close> |
10 |
10 |
11 text \<open>Lifting existing lemmas in a @{text ring_hom_ring} locale\<close> |
11 text \<open>Lifting existing lemmas in a \<open>ring_hom_ring\<close> locale\<close> |
12 locale ring_hom_ring = R?: ring R + S?: ring S |
12 locale ring_hom_ring = R?: ring R + S?: ring S |
13 for R (structure) and S (structure) + |
13 for R (structure) and S (structure) + |
14 fixes h |
14 fixes h |
15 assumes homh: "h \<in> ring_hom R S" |
15 assumes homh: "h \<in> ring_hom R S" |
16 notes hom_mult [simp] = ring_hom_mult [OF homh] |
16 notes hom_mult [simp] = ring_hom_mult [OF homh] |
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 --"the kernel of a ring homomorphism is an ideal" |
105 \<comment>"the kernel of a ring homomorphism is an ideal" |
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]) |