Nuprl Definition : alg_from_rng
alg_from_rng(A;r;act) == <|r|, =b, ≤b, +r, 0, -r, *, 1, ÷r, act>
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_times: *,
rng_one: 1,
pair: <a, b>,
rng_div: ÷r
Latex:
alg\_from\_rng(A;r;act) == <|r|, =\msubb{}, \mleq{}\msubb{}, +r, 0, -r, *, 1, \mdiv{}r, act>
Date html generated:
2016_05_16-AM-08_14_43
Last ObjectModification:
2015_09_23-AM-09_52_46
Theory : polynom_1
Home
Index