Nuprl Definition : quot_ring

==  <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: y apply: a lambda: λx.A[x] pair: <a, b> inr: inr 
Definitions occuring in definition :  quot_ring_car: Carrier(r/d) btrue: tt rng_plus: +r rng_zero: 0 apply: a rng_minus: -r infix_ap: y rng_times: * pair: <a, b> rng_one: 1 lambda: λx.A[x] inr: inr  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