equal
deleted
inserted
replaced
9 begin |
9 begin |
10 |
10 |
11 |
11 |
12 section {* Homomorphisms of Non-Commutative Rings *} |
12 section {* Homomorphisms of Non-Commutative Rings *} |
13 |
13 |
14 text {* Lifting existing lemmas in a ring\_hom\_ring locale *} |
14 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *} |
15 locale ring_hom_ring = ring R + ring S + var h + |
15 locale ring_hom_ring = ring R + ring S + var h + |
16 assumes homh: "h \<in> ring_hom R S" |
16 assumes homh: "h \<in> ring_hom R S" |
17 notes hom_mult [simp] = ring_hom_mult [OF homh] |
17 notes hom_mult [simp] = ring_hom_mult [OF homh] |
18 and hom_one [simp] = ring_hom_one [OF homh] |
18 and hom_one [simp] = ring_hom_one [OF homh] |
19 |
19 |