Commit 2026-05-05 13:49 d6db0fd4

View on Github →

feat(Data/Finsupp): filtering a single element (#38904) Also rename filter_pos_add_filter_neg to filter_add_filter_not to match the Finset statement.

Estimated changes

Modified Mathlib/Data/DFinsupp/Defs.lean

added theorem DFinsupp.filter_add_filter_not

added theorem DFinsupp.filter_eq'

added theorem DFinsupp.filter_eq

deleted theorem DFinsupp.filter_pos_add_filter_neg

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.filter_add_filter_not

added theorem Finsupp.filter_eq'

added theorem Finsupp.filter_eq

deleted theorem Finsupp.filter_pos_add_filter_neg