Theorem DFinsupp.filter_add_filter_not

Modification history

2026-05-05 13:49
Mathlib/Data/DFinsupp/Defs.lean
feat(Data/Finsupp): filtering a single element (#38904) …
Added DFinsupp.filter_add_filter_notView on Github →