Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.prod_indicator_index

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.prod_indicator_indexView on Github →