mathlib3

9264b15e - feat(algebra/algebra/bilinear): make `algebra.lmul` to apply to non-unital (non-assoc) algebras (#15310)

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).