Nuprl Definition : ring_hom
RingHom(R;S) == {f:|R| ⟶ |S|| 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,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
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:
RingHom(R;S) ==
\{f:|R| {}\mrightarrow{} |S|| FunThru2op(|R|;|S|;+R;+S;f) \mwedge{} FunThru2op(|R|;|S|;*;*;f) \mwedge{} ((f 1) = 1)\}
Date html generated:
2016_05_15-PM-00_25_11
Last ObjectModification:
2015_09_23-AM-06_26_03
Theory : rings_1
Home
Index