Nuprl Definition : module
A-Module ==
{m:algebra_sig{i:l}(|A|)|
IsGroup(m.car;m.plus;m.zero;m.minus)
∧ Comm(m.car;m.plus)
∧ IsAction(|A|;*;1;m.car;m.act)
∧ IsBilinear(|A|;m.car;m.car;+A;m.plus;m.plus;m.act)}
Definitions occuring in Statement :
alg_act: a.act,
alg_minus: a.minus,
alg_zero: a.zero,
alg_plus: a.plus,
alg_car: a.car,
algebra_sig: algebra_sig{i:l}(A),
comm: Comm(T;op),
and: P ∧ Q,
set: {x:A| B[x]} ,
rng_one: 1,
rng_times: *,
rng_plus: +r,
rng_car: |r|,
group_p: IsGroup(T;op;id;inv),
action_p: IsAction(A;x;e;S;f),
bilinear_p: IsBilinear(A;B;C;+a;+b;+c;f)
Definitions occuring in definition :
set: {x:A| B[x]} ,
algebra_sig: algebra_sig{i:l}(A),
group_p: IsGroup(T;op;id;inv),
alg_zero: a.zero,
alg_minus: a.minus,
comm: Comm(T;op),
and: P ∧ Q,
action_p: IsAction(A;x;e;S;f),
rng_times: *,
rng_one: 1,
bilinear_p: IsBilinear(A;B;C;+a;+b;+c;f),
rng_car: |r|,
alg_car: a.car,
rng_plus: +r,
alg_plus: a.plus,
alg_act: a.act
FDL editor aliases :
module
Latex:
A-Module ==
\{m:algebra\_sig\{i:l\}(|A|)|
IsGroup(m.car;m.plus;m.zero;m.minus)
\mwedge{} Comm(m.car;m.plus)
\mwedge{} IsAction(|A|;*;1;m.car;m.act)
\mwedge{} IsBilinear(|A|;m.car;m.car;+A;m.plus;m.plus;m.act)\}
Date html generated:
2016_05_16-AM-07_26_23
Last ObjectModification:
2015_09_23-AM-09_51_00
Theory : algebras_1
Home
Index