Nuprl Definition : rng_of_alg
a↓rg == <a.car, a.eq, a.le, a.plus, a.zero, a.minus, a.times, a.one, a.div>
Definitions occuring in Statement :
alg_div: a.div,
alg_one: a.one,
alg_times: a.times,
alg_minus: a.minus,
alg_zero: a.zero,
alg_plus: a.plus,
alg_le: a.le,
alg_eq: a.eq,
alg_car: a.car,
pair: <a, b>
Definitions occuring in definition :
alg_car: a.car,
alg_eq: a.eq,
alg_le: a.le,
alg_plus: a.plus,
alg_zero: a.zero,
alg_minus: a.minus,
alg_times: a.times,
pair: <a, b>,
alg_one: a.one,
alg_div: a.div
Latex:
a\mdownarrow{}rg == <a.car, a.eq, a.le, a.plus, a.zero, a.minus, a.times, a.one, a.div>
Date html generated:
2016_05_16-AM-07_26_17
Last ObjectModification:
2015_09_23-AM-09_50_59
Theory : algebras_1
Home
Index