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