Nuprl Definition : ideal_p

Ideal of ==  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: SubGrp of g infix_ap: y all: x:A. B[x] implies:  Q and: P ∧ Q apply: a
Definitions occuring in definition :  and: P ∧ Q subgrp_p: SubGrp of g add_grp_of_rng: r↓+gp all: x:A. B[x] rng_car: |r| implies:  Q apply: a infix_ap: y rng_times: *

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