equal
deleted
inserted
replaced
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] |
17 and hom_one [simp] = ring_hom_one [OF homh] |
17 and hom_one [simp] = ring_hom_one [OF homh] |
18 |
18 |
19 interpretation ring_hom_cring \<subseteq> ring_hom_ring |
19 interpretation ring_hom_cring \<subseteq> ring_hom_ring |
20 by (unfold_locales, rule homh) |
20 proof qed (rule homh) |
21 |
21 |
22 interpretation ring_hom_ring \<subseteq> abelian_group_hom R S |
22 interpretation ring_hom_ring \<subseteq> abelian_group_hom R S |
23 apply (rule abelian_group_homI) |
23 apply (rule abelian_group_homI) |
24 apply (rule R.is_abelian_group) |
24 apply (rule R.is_abelian_group) |
25 apply (rule S.is_abelian_group) |
25 apply (rule S.is_abelian_group) |