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