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