Commit 2024-04-02 12:35 a2b6e2ea
View on Github →chore(RingTheory): delete useless lemma (#11827)
As discussed in https://github.com/leanprover-community/mathlib4/pull/11790 for the case of Lie derivations, it seems that this map_sum lemma is not useful since we can use the generic version.