Nuprl Definition : rng_chom_p
(compound):: rng_chom_p(r;s;f) == rng_hom_p(r;s;f) ∧ (∀a,b:|r|. (((f a) * (f b)) = ((f b) * (f a)) ∈ |s|))
Definitions occuring in Statement :
rng_hom_p: rng_hom_p(r;s;f),
rng_times: *,
rng_car: |r|,
infix_ap: x f y,
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
rng_hom_p: rng_hom_p(r;s;f),
all: ∀x:A. B[x],
equal: s = t ∈ T,
rng_car: |r|,
infix_ap: x f y,
rng_times: *,
apply: f a
Latex:
(compound)::
rng\_chom\_p(r;s;f) ==
rng\_hom\_p(r;s;f) \mwedge{} (\mforall{}a,b:|r|. (((f a) * (f b)) = ((f b) * (f a))))
Date html generated:
2016_05_15-PM-00_25_05
Last ObjectModification:
2015_09_23-AM-06_26_01
Theory : rings_1
Home
Index