Nuprl Definition : quot_ring
r / d == <Carrier(r/d), λx,y. (d (x +r (-r y))), λx,y. tt, λx,y. (x +r y), 0, λx.(-r x), λx,y. (x * y), 1, λx,y. (inr ⋅\000C )>
Definitions occuring in Statement :
quot_ring_car: Carrier(r/d),
rng_one: 1,
rng_times: *,
rng_minus: -r,
rng_zero: 0,
rng_plus: +r,
btrue: tt,
it: ⋅,
infix_ap: x f y,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x
Definitions occuring in definition :
quot_ring_car: Carrier(r/d),
btrue: tt,
rng_plus: +r,
rng_zero: 0,
apply: f a,
rng_minus: -r,
infix_ap: x f y,
rng_times: *,
pair: <a, b>,
rng_one: 1,
lambda: λx.A[x],
inr: inr x ,
it: ⋅
Latex:
r / d ==
<Carrier(r/d), \mlambda{}x,y. (d (x +r (-r y))), \mlambda{}x,y. tt, \mlambda{}x,y. (x +r y), 0, \mlambda{}x.(-r x), \mlambda{}x,y. (x * y), 1, \000C\mlambda{}x,y. (inr \mcdot{} )>
Date html generated:
2016_05_15-PM-00_23_42
Last ObjectModification:
2015_09_23-AM-06_25_56
Theory : rings_1
Home
Index