Nuprl Definition : rng_hom_p
(compound):: rng_hom_p(r;s;f) == FunThru2op(|r|;|s|;+r;+s;f) ∧ FunThru2op(|r|;|s|;*;*;f) ∧ ((f 1) = 1 ∈ |s|)
Definitions occuring in Statement :
rng_one: 1,
rng_times: *,
rng_plus: +r,
rng_car: |r|,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
rng_plus: +r,
and: P ∧ Q,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
rng_times: *,
equal: s = t ∈ T,
rng_car: |r|,
apply: f a,
rng_one: 1
Latex:
(compound)::
rng\_hom\_p(r;s;f) ==
FunThru2op(|r|;|s|;+r;+s;f) \mwedge{} FunThru2op(|r|;|s|;*;*;f) \mwedge{} ((f 1) = 1)
Date html generated:
2016_05_15-PM-00_24_53
Last ObjectModification:
2015_09_23-AM-06_25_59
Theory : rings_1
Home
Index