Nuprl Definition : rng_p
rng_p(r) == grp_p(r↓+gp) ∧ mon_p(r↓xmn) ∧ BiLinear(|r|;+r;*)
Definitions occuring in Statement :
grp_p: grp_p(g),
mon_p: mon_p(g),
and: P ∧ Q,
add_grp_of_rng: r↓+gp,
mul_mon_of_rng: r↓xmn,
rng_times: *,
rng_plus: +r,
rng_car: |r|,
bilinear: BiLinear(T;pl;tm)
Definitions occuring in definition :
grp_p: grp_p(g),
add_grp_of_rng: r↓+gp,
and: P ∧ Q,
mon_p: mon_p(g),
mul_mon_of_rng: r↓xmn,
bilinear: BiLinear(T;pl;tm),
rng_car: |r|,
rng_plus: +r,
rng_times: *
Latex:
rng\_p(r) == grp\_p(r\mdownarrow{}+gp) \mwedge{} mon\_p(r\mdownarrow{}xmn) \mwedge{} BiLinear(|r|;+r;*)
Date html generated:
2016_05_16-AM-08_13_54
Last ObjectModification:
2015_09_23-AM-09_52_36
Theory : polynom_1
Home
Index