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