Commit 2023-03-20 22:50 aa0f33a5

View on Github →

feat: add some lemmas about Finsupp.indicator (#2258) mathlib3 PR: https://github.com/leanprover-community/mathlib/pull/17413

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

added theorem Finsupp.indicator_eq_sum_single

added theorem Finsupp.prod_indicator_index

Modified Mathlib/Data/Finsupp/Defs.lean

deleted theorem Finsupp.single_eq_indicator

added theorem Finsupp.single_eq_set_indicator

modified theorem Finsupp.single_eq_zero

Modified Mathlib/Data/Finsupp/Indicator.lean

added theorem Finsupp.single_eq_indicator