Commit 2026-09-14 12:25 609b2d37

View on Github →

chore: redefine Finsupp.indicator using Finsupp.onFinset (#33434)

Estimated changes

Modified Mathlib/Data/Finsupp/Indicator.lean

modified def Finsupp.indicator

modified theorem Finsupp.support_indicator_subset