Def LinearEquiv.compDer

Modification history

2025-11-19 13:28
Mathlib/RingTheory/Derivation/Basic.lean
improved R-linearity to A-linearity in the PushForward of Derivations (#31464) …
Modified LinearEquiv.compDerView on Github →
2023-06-02 11:07
Mathlib/RingTheory/Derivation/Basic.lean
feat: port RingTheory.Derivation.Basic (#4575)
Added LinearEquiv.compDerView on Github →