Nuprl Definition : ideal_p
S Ideal of R == S SubGrp of R↓+gp ∧ (∀a,b:|R|. ((S a) ⇒ (S (a * b))))
Definitions occuring in Statement :
add_grp_of_rng: r↓+gp,
rng_times: *,
rng_car: |r|,
subgrp_p: s SubGrp of g,
infix_ap: x f y,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a
Definitions occuring in definition :
and: P ∧ Q,
subgrp_p: s SubGrp of g,
add_grp_of_rng: r↓+gp,
all: ∀x:A. B[x],
rng_car: |r|,
implies: P ⇒ Q,
apply: f a,
infix_ap: x f y,
rng_times: *
Latex:
S Ideal of R == S SubGrp of R\mdownarrow{}+gp \mwedge{} (\mforall{}a,b:|R|. ((S a) {}\mRightarrow{} (S (a * b))))
Date html generated:
2016_05_15-PM-00_22_47
Last ObjectModification:
2015_09_23-AM-06_25_46
Theory : rings_1
Home
Index