Theorem Finsupp.filter_pos_add_filter_neg

Modification history

2026-05-05 13:49
Mathlib/Data/Finsupp/Basic.lean
feat(Data/Finsupp): filtering a single element (#38904) …
Deleted Finsupp.filter_pos_add_filter_negView on Github →
2024-02-23 00:32
Mathlib/Data/Finsupp/Basic.lean
refactor(Data/Finsupp): Make `Finsupp.filter` computable (#8979) …
Modified Finsupp.filter_pos_add_filter_negView on Github →
2023-02-01 05:31
Mathlib/Data/Finsupp/Basic.lean
feat: port Data.Finsupp.Basic (#1949) …
Added Finsupp.filter_pos_add_filter_negView on Github →