Nuprl Definition : monoid_hom_p
(compound):: IsMonHom{M1,M2}(f) == FunThru2op(|M1|;|M2|;*;*;f) ∧ ((f e) = e ∈ |M2|)
Definitions occuring in Statement :
grp_id: e,
grp_op: *,
grp_car: |g|,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
grp_op: *,
equal: s = t ∈ T,
grp_car: |g|,
apply: f a,
grp_id: e
Latex:
(compound):: IsMonHom\{M1,M2\}(f) == FunThru2op(|M1|;|M2|;*;*;f) \mwedge{} ((f e) = e)
Date html generated:
2016_05_15-PM-00_09_44
Last ObjectModification:
2015_09_23-AM-06_24_32
Theory : groups_1
Home
Index