Nuprl Definition : quot_ring_car
Carrier(r/d) == x,y:|r|//(↑(d (x +r (-r y))))
Definitions occuring in Statement :
rng_minus: -r,
rng_plus: +r,
rng_car: |r|,
quotient: x,y:A//B[x; y],
assert: ↑b,
infix_ap: x f y,
apply: f a
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
rng_car: |r|,
assert: ↑b,
infix_ap: x f y,
rng_plus: +r,
apply: f a,
rng_minus: -r
Latex:
Carrier(r/d) == x,y:|r|//(\muparrow{}(d (x +r (-r y))))
Date html generated:
2016_05_15-PM-00_23_30
Last ObjectModification:
2015_09_23-AM-06_25_55
Theory : rings_1
Home
Index