Commit 2023-11-13 17:59 f5eb981b

View on Github →

fix(Mathlib/Algebra/Lie/DirectSum): remove unused R argument from lemmas (#8388) This made them not actually work as a simp lemma. Also extracts a common result that can be used to prove single_add for DFinsupp and Finsupp, and a new Finsupp.single_mul lemma.

Estimated changes

Modified Mathlib/Algebra/Lie/DirectSum.lean

deleted theorem DirectSum.lie_of_of_eq

modified theorem DirectSum.lie_of_of_ne

added theorem DirectSum.lie_of_same

Modified Mathlib/Data/DFinsupp/Basic.lean

added theorem DFinsupp.zipWith_single_single

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.zipWith_single_single

Modified Mathlib/Data/Finsupp/Pointwise.lean

added theorem Finsupp.single_mul