Theorem Finsupp.support_indicator_subset

Modification history

2026-09-14 12:25
Mathlib/Data/Finsupp/Indicator.lean
chore: redefine `Finsupp.indicator` using `Finsupp.onFinset` (#33434)
Modified Finsupp.support_indicator_subsetView on Github →
2026-04-09 13:40
Mathlib/Data/Finsupp/Indicator.lean
chore(Mathlib/Data/Finsupp/Indicator.lean): automated extraction (#37811) …
Modified Finsupp.support_indicator_subsetView on Github →
2023-01-29 02:08
Mathlib/Data/Finsupp/Indicator.lean
feat: port Data.Finsupp.Indicator (#1916)
Added Finsupp.support_indicator_subsetView on Github →