Nuprl Definition : add_grp_of_rng
r↓+gp ==  <|r|, =b, ≤b, +r, 0, -r>
Definitions occuring in Statement : 
rng_minus: -r
, 
rng_zero: 0
, 
rng_plus: +r
, 
rng_le: ≤b
, 
rng_eq: =b
, 
rng_car: |r|
, 
pair: <a, b>
Definitions occuring in definition : 
rng_car: |r|
, 
rng_eq: =b
, 
rng_le: ≤b
, 
rng_plus: +r
, 
pair: <a, b>
, 
rng_zero: 0
, 
rng_minus: -r
Latex:
r\mdownarrow{}+gp  ==    <|r|,  =\msubb{},  \mleq{}\msubb{},  +r,  0,  -r>
Date html generated:
2016_05_15-PM-00_21_08
Last ObjectModification:
2015_09_23-AM-06_25_35
Theory : rings_1
Home
Index