Nuprl Definition : rng_abmon
rng_abmon{i}() == {r:RngSig| IsMonoid(|r|;+r;0) ∧ Comm(|r|;+r) ∧ IsEqFun(|r|;=b)}
Definitions occuring in Statement :
eqfun_p: IsEqFun(T;eq),
comm: Comm(T;op),
and: P ∧ Q,
set: {x:A| B[x]} ,
rng_zero: 0,
rng_plus: +r,
rng_eq: =b,
rng_car: |r|,
rng_sig: RngSig,
monoid_p: IsMonoid(T;op;id)
Definitions occuring in definition :
set: {x:A| B[x]} ,
rng_sig: RngSig,
monoid_p: IsMonoid(T;op;id),
rng_zero: 0,
and: P ∧ Q,
comm: Comm(T;op),
rng_plus: +r,
eqfun_p: IsEqFun(T;eq),
rng_car: |r|,
rng_eq: =b
Latex:
rng\_abmon\{i\}() == \{r:RngSig| IsMonoid(|r|;+r;0) \mwedge{} Comm(|r|;+r) \mwedge{} IsEqFun(|r|;=\msubb{})\}
Date html generated:
2016_05_16-AM-08_11_37
Last ObjectModification:
2015_09_23-AM-09_52_23
Theory : list_3
Home
Index