Nuprl Definition : algebra
algebra{i:l}(A) ==
{m:A-Module|
IsMonoid(m.car;m.times;m.one) ∧ BiLinear(m.car;m.plus;m.times) ∧ (∀a:|A|. Dist1op2opLR(m.car;m.act a;m.times))}
Definitions occuring in Statement :
module: A-Module,
alg_act: a.act,
alg_one: a.one,
alg_times: a.times,
alg_plus: a.plus,
alg_car: a.car,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
rng_car: |r|,
monoid_p: IsMonoid(T;op;id),
dist_1op_2op_lr: Dist1op2opLR(A;1op;2op),
bilinear: BiLinear(T;pl;tm)
Definitions occuring in definition :
set: {x:A| B[x]} ,
module: A-Module,
monoid_p: IsMonoid(T;op;id),
alg_one: a.one,
and: P ∧ Q,
bilinear: BiLinear(T;pl;tm),
alg_plus: a.plus,
all: ∀x:A. B[x],
rng_car: |r|,
dist_1op_2op_lr: Dist1op2opLR(A;1op;2op),
alg_car: a.car,
apply: f a,
alg_act: a.act,
alg_times: a.times
Latex:
algebra\{i:l\}(A) ==
\{m:A-Module|
IsMonoid(m.car;m.times;m.one)
\mwedge{} BiLinear(m.car;m.plus;m.times)
\mwedge{} (\mforall{}a:|A|. Dist1op2opLR(m.car;m.act a;m.times))\}
Date html generated:
2016_05_16-AM-07_27_20
Last ObjectModification:
2015_09_23-AM-09_51_02
Theory : algebras_1
Home
Index