Commit 2022-08-02 00:16 9264b15e

feat(algebra/algebra/bilinear): make algebra.lmul to apply to non-unital (non-assoc) algebras (#15310) Multiplication in an algebra is a bilinear map. Previously, this was called algebra.lmul ("l" for "linear") and what was actually constructed was an algebra homomorphism A →ₐ[R] (End R A), where A is an R-algebra. As a result, this object (and the derived linear maps algebra.lmul_left and algebra.lmul_right, and others) only exists when A is a unital R-algebra. Of course, when A is a non-unital (even non-associative) algebra, this bilinear map A →ₗ[R] A →ₗ[R] A still exists, but it can't be upgraded to an algebra homomorphism as above. When A is associative, it can be upgraded to non-unital algebra homomorphism. In this PR, we define all three of these multiplication maps as linear_map.mul, non_unital_alg_hom.lmul and algebra.lmul, along with appropriate simp lemmas stating that the underlying functions coincide. All existing lemmas about the maps are preserved, but each in the correct generality. In so doing, we also move most the results and definitions in this file into the linear_map namespace (which is also why we call the simplest map linear_map.mul instead of linear_map.lmul as the l in the latter would be redundant).