Nuprl Definition : rng_to_alg
rng_to_alg(r) == <|r|, =b, ≤b, +r, 0, -r, *, 1, ÷r, *>
Definitions occuring in Statement :
pair: <a, b>,
rng_div: ÷r,
rng_one: 1,
rng_times: *,
rng_minus: -r,
rng_zero: 0,
rng_plus: +r,
rng_le: ≤b,
rng_eq: =b,
rng_car: |r|
Definitions occuring in definition :
rng_car: |r|,
rng_eq: =b,
rng_le: ≤b,
rng_plus: +r,
rng_zero: 0,
rng_minus: -r,
rng_one: 1,
pair: <a, b>,
rng_div: ÷r,
rng_times: *
Latex:
rng\_to\_alg(r) == <|r|, =\msubb{}, \mleq{}\msubb{}, +r, 0, -r, *, 1, \mdiv{}r, *>
Date html generated:
2016_05_16-AM-07_27_48
Last ObjectModification:
2015_09_23-AM-09_51_06
Theory : algebras_1
Home
Index