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