Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.indicator_eq_sum_single

Modification history

2023-03-01 21:21
src/algebra/big_operators/finsupp.lean
feat(data/finsupp/indicator, algebra/big_operators/finsupp): add some lemmas about `finsupp.indicator` (#17413) …
Added finsupp.indicator_eq_sum_singleView on Github →