Nuprl Definition : prime_ideal_p
IsPrimeIdeal(R;P) == (¬(P 1)) ∧ (∀a,b:|R|. ((P (a * b)) ⇒ ((P a) ∨ (P b))))
Definitions occuring in Statement :
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,
apply: f a
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,
apply: f a
Latex:
IsPrimeIdeal(R;P) == (\mneg{}(P 1)) \mwedge{} (\mforall{}a,b:|R|. ((P (a * b)) {}\mRightarrow{} ((P a) \mvee{} (P b))))
Date html generated:
2016_05_15-PM-00_24_41
Last ObjectModification:
2015_09_23-AM-06_25_57
Theory : rings_1
Home
Index