Nuprl Definition : field_p
IsField(r) == 0 ≠ 1 ∈ |r| ∧ (∀u:|r|. (u ≠ 0 ∈ |r| ⇒ u | 1 in r))
Definitions occuring in Statement :
ring_divs: a | b in r,
rng_one: 1,
rng_zero: 0,
rng_car: |r|,
all: ∀x:A. B[x],
nequal: a ≠ b ∈ T ,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
nequal: a ≠ b ∈ T ,
rng_car: |r|,
rng_zero: 0,
ring_divs: a | b in r,
rng_one: 1
Latex:
IsField(r) == 0 \mneq{} 1 \mmember{} |r| \mwedge{} (\mforall{}u:|r|. (u \mneq{} 0 \mmember{} |r| {}\mRightarrow{} u | 1 in r))
Date html generated:
2016_05_15-PM-00_22_28
Last ObjectModification:
2015_09_23-AM-06_25_40
Theory : rings_1
Home
Index