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