Commit 2026-01-19 09:42 230e7333
View on Github →chore(Algebra): deprecate DistribMulAction.toAddMonoidHom (#33724)
which is simply a specialized version of DistribSMul.toAddMonoidHom.
MulDistribMulAction.toMonoidHom has to be kept, since there is no MulDistribSMul yet.
also deprecate AddMonoidHom.smulLeft (same situation) and generalize DistribMulAction.toLinearMap