Nuprl Definition : alg_hom_p
(compound)::
alg_hom_p(a; m; n; f) ==
module_hom_p(a; m; n; f) ∧ FunThru2op(m.car;n.car;m.times;n.times;f) ∧ ((f m.one) = n.one ∈ n.car)
Definitions occuring in Statement :
module_hom_p: module_hom_p(a; m; n; f),
alg_one: a.one,
alg_times: a.times,
alg_car: a.car,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T,
fun_thru_2op: FunThru2op(A;B;opa;opb;f)
Definitions occuring in definition :
module_hom_p: module_hom_p(a; m; n; f),
and: P ∧ Q,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
alg_times: a.times,
equal: s = t ∈ T,
alg_car: a.car,
apply: f a,
alg_one: a.one
Latex:
(compound)::
alg\_hom\_p(a; m; n; f) ==
module\_hom\_p(a; m; n; f) \mwedge{} FunThru2op(m.car;n.car;m.times;n.times;f) \mwedge{} ((f m.one) = n.one)
Date html generated:
2016_05_16-AM-07_27_58
Last ObjectModification:
2015_09_23-AM-09_51_07
Theory : algebras_1
Home
Index