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