Commit 2025-11-24 08:57 e7aca660

View on Github →

feat: grind annotations for Finsupp (#31932)

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

Modified Mathlib/Algebra/Notation/Pi/Basic.lean

Modified Mathlib/Data/Finsupp/Defs.lean

modified theorem Finsupp.mapRange.equiv_symm

Modified Mathlib/Data/Finsupp/Single.lean

modified theorem Finsupp.erase_eq_update_zero

modified theorem Finsupp.erase_ne

modified theorem Finsupp.erase_same

modified theorem Finsupp.erase_single

added theorem Finsupp.update_apply

Modified Mathlib/LinearAlgebra/DFinsupp.lean