Commit 2025-11-19 13:28 86eaade1

improved R-linearity to A-linearity in the PushForward of Derivations (#31464) Let $A$ be an $R$-algebra for a commutative ring $R$ and $f:M\to N$ an $A$-module homomorphism. Given a derivation $D\in Der_R(A,M)$, we have a derivation $f \circ D$ of $Der_R(A,N)$. The induced map $Der_R(A,M)\to Der_R(A,N)$ is $A$-linear but was only reported to be $R$-linear in the previous implementation. All changes are in the PushForward section of the RingTheory/Derivation/Basic.lean file. The statements of definitions

• _root_.LinearMap.compDer
• llcomp
• _root_.LinearEquiv.compDer are changed from $R$-linear to $A$-linear. For the stronger linearity the proof of map_smul' in _root_.LinearMap.compDer had to be changed. The rest remains as is. Edit: Some files explicitly used the weaker version, these have now been changed, by applying .restrictScalars (R:=...), whereever the weaker linearity version of compDer was needed.