Nuprl Definition : rprime
r-Prime(u) == (¬u | 1 in r) ∧ (∀v,w:|r|. (u | v * w in r ⇒ (u | v in r ∨ u | w in r)))
Definitions occuring in Statement :
ring_divs: a | b in r,
rng_one: 1,
rng_times: *,
rng_car: |r|,
infix_ap: x f y,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
not: ¬A,
rng_one: 1,
all: ∀x:A. B[x],
rng_car: |r|,
implies: P ⇒ Q,
infix_ap: x f y,
rng_times: *,
or: P ∨ Q,
ring_divs: a | b in r
Latex:
r-Prime(u) == (\mneg{}u | 1 in r) \mwedge{} (\mforall{}v,w:|r|. (u | v * w in r {}\mRightarrow{} (u | v in r \mvee{} u | w in r)))
Date html generated:
2016_05_15-PM-00_22_43
Last ObjectModification:
2015_09_23-AM-06_25_45
Theory : rings_1
Home
Index