English
The multiplication in a non-unital algebra induces a bilinear map; left multiplication by a and right multiplication by b together define a bilinear action.
Русский
Умножение в неединообразной алгебре порождает билинейное отображение; левая умножение на a и правая на b задают билинейное действие.
LaTeX
$$$$ \text{The map } (a,b) \mapsto (x \mapsto a x b) \text{ is bilinear in } a,b. $$$$
Lean4
/-- The multiplication in a non-unital algebra is a bilinear map.
A weaker version of this for non-unital non-associative algebras exists as `LinearMap.mul`. -/
def _root_.NonUnitalAlgHom.lmul : A →ₙₐ[R] End R A
where
__ := mul R A
map_mul' := mulLeft_mul _ _
map_zero' := mulLeft_zero_eq_zero _ _
