Nuprl Definition : ring_divs
a | b in r == ∃c:|r|. ((c * a) = b ∈ |r|)
Definitions occuring in Statement :
rng_times: *,
rng_car: |r|,
infix_ap: x f y,
exists: ∃x:A. B[x],
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
equal: s = t ∈ T,
rng_car: |r|,
infix_ap: x f y,
rng_times: *
Latex:
a | b in r == \mexists{}c:|r|. ((c * a) = b)
Date html generated:
2016_05_15-PM-00_22_13
Last ObjectModification:
2015_09_23-AM-06_25_37
Theory : rings_1
Home
Index