Commit 2024-12-01 01:39 a1f01bd5

refactor(Algebra/Bilinear): generalize to non-commutative base rings (#19232) This removes unnecessary IsScalarTower R A A and SMulCommClass R A A arguments from LinearMap.mulLeft and LinearMap.mulRight, respectively. As described in the new docstring, this allows respective specializations to R := Aᵐᵒᵖ and R := A. Unfortunately all of the lemmas have to be reordered to take advantage of these relaxed assumptions. In the chaos, a few lemmas also became generalized to non-unital rings. There is some overlap here with DistribMulAction.toLinearMap, but that doesn't work in the case of non-unital rings.