Nuprl Definition : max_ideal_p
IsMaxIdeal(r;m) == ∀u:|r|. (¬(m u) ⇐⇒ ∃v:|r|. (m ((u * v) +r (-r 1))))
Definitions occuring in Statement :
rng_one: 1,
rng_times: *,
rng_minus: -r,
rng_plus: +r,
rng_car: |r|,
infix_ap: x f y,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
exists: ∃x:A. B[x],
rng_car: |r|,
rng_plus: +r,
infix_ap: x f y,
rng_times: *,
apply: f a,
rng_minus: -r,
rng_one: 1
Latex:
IsMaxIdeal(r;m) == \mforall{}u:|r|. (\mneg{}(m u) \mLeftarrow{}{}\mRightarrow{} \mexists{}v:|r|. (m ((u * v) +r (-r 1))))
Date html generated:
2016_05_15-PM-00_24_49
Last ObjectModification:
2015_09_23-AM-06_25_58
Theory : rings_1
Home
Index