src/HOL/Algebra/RingHom.thy
changeset 26204 da9778392d8c
parent 23464 bc2563c37b1a
child 27611 2c01c0bdb385
equal deleted inserted replaced
26203:9625f3579b48 26204:da9778392d8c
    31 done
    31 done
    32 
    32 
    33 lemma (in ring_hom_ring) is_ring_hom_ring:
    33 lemma (in ring_hom_ring) is_ring_hom_ring:
    34   includes struct R + struct S
    34   includes struct R + struct S
    35   shows "ring_hom_ring R S h"
    35   shows "ring_hom_ring R S h"
    36 by fact
    36 by (rule ring_hom_ring_axioms)
    37 
    37 
    38 lemma ring_hom_ringI:
    38 lemma ring_hom_ringI:
    39   includes ring R + ring S
    39   includes ring R + ring S
    40   assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
    40   assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
    41           hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
    41           hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"