Facts about algebras involving bilinear maps and tensor products #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
We move a few basic statements about algebras out of
in order to avoid importing
The multiplication in a non-unital non-associative algebra is a bilinear map.
A weaker version of this for semirings exists as
The multiplication map on a non-unital algebra, as an
R-linear map from
A ⊗[R] A to
The multiplication on the left in a non-unital algebra is a linear map.
The multiplication on the right in an algebra is a linear map.
Simultaneous multiplication on the left and right is a linear map.
The multiplication in a non-unital algebra is a bilinear map.
A weaker version of this for non-unital non-associative algebras exists as
The multiplication in an algebra is an algebra homomorphism into the endomorphisms on
A weaker version of this for non-unital algebras exists as