Nuprl Definition : drng
DRng == {r:RngSig| IsRing(|r|;+r;0;-r;*;1) ∧ IsEqFun(|r|;=b)}
Definitions occuring in Statement :
ring_p: IsRing(T;plus;zero;neg;times;one),
rng_one: 1,
rng_times: *,
rng_minus: -r,
rng_zero: 0,
rng_plus: +r,
rng_eq: =b,
rng_car: |r|,
rng_sig: RngSig,
eqfun_p: IsEqFun(T;eq),
and: P ∧ Q,
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
rng_sig: RngSig,
and: P ∧ Q,
ring_p: IsRing(T;plus;zero;neg;times;one),
rng_plus: +r,
rng_zero: 0,
rng_minus: -r,
rng_times: *,
rng_one: 1,
eqfun_p: IsEqFun(T;eq),
rng_car: |r|,
rng_eq: =b
Latex:
DRng == \{r:RngSig| IsRing(|r|;+r;0;-r;*;1) \mwedge{} IsEqFun(|r|;=\msubb{})\}
Date html generated:
2016_05_15-PM-00_20_24
Last ObjectModification:
2015_09_23-AM-06_25_33
Theory : rings_1
Home
Index