Nuprl Definition : rng_from_grp
rng_from_grp(g;times;one;div) == <|g|, =b, ≤b, *, e, ~, times, one, div>
Definitions occuring in Statement :
pair: <a, b>,
grp_inv: ~,
grp_id: e,
grp_op: *,
grp_le: ≤b,
grp_eq: =b,
grp_car: |g|
Definitions occuring in definition :
grp_car: |g|,
grp_eq: =b,
grp_le: ≤b,
grp_op: *,
grp_id: e,
grp_inv: ~,
pair: <a, b>
Latex:
rng\_from\_grp(g;times;one;div) == <|g|, =\msubb{}, \mleq{}\msubb{}, *, e, \msim{}, times, one, div>
Date html generated:
2016_05_16-AM-08_14_39
Last ObjectModification:
2015_09_23-AM-09_52_45
Theory : polynom_1
Home
Index