Commit 2025-12-06 14:46 371379bb

feat(RingTheory): improved linearity of Derivation.compDer (#32509) Given a scalar tower $$R\to A \to B \to M$$, we have the natural map $Der_R(B, M)\to Der_R(A, M)$. It was stated to be $$A$$-linear, but is in fact even $$B$$-linear. To be able to phrase this, I needed to change [IsScalarTower R A M] to [IsScalarTower R B M]. Those should be factually equivalent, due to IsScalarTower.to₁₃₄, however the inference of IsScalarTower R B M from IsScalarTower R A M does not seem to be automatic.