Theorem DFinsupp.filter_pos_add_filter_neg

Modification history

2026-05-05 13:49
Mathlib/Data/DFinsupp/Defs.lean
feat(Data/Finsupp): filtering a single element (#38904) …
Deleted DFinsupp.filter_pos_add_filter_negView on Github →
2023-07-12 02:40
Mathlib/Data/DFinsupp/Basic.lean
chore: rename `Dfinsupp` to `DFinsupp` (#5822) …
Added DFinsupp.filter_pos_add_filter_negView on Github →