Commit 2023-01-29 02:08 8f7e7221

View on Github →

feat: port Data.Finsupp.Indicator (#1916)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Indicator.lean

added def Finsupp.indicator

added theorem Finsupp.indicator_apply

added theorem Finsupp.indicator_injective

added theorem Finsupp.indicator_of_mem

added theorem Finsupp.indicator_of_not_mem

added theorem Finsupp.support_indicator_subset