Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.card_eq_sum_ones

Modification history

2020-05-02 15:22
src/algebra/big_operators.lean
refactor(algebra/big_operators): introduce notation for finset.prod and finset.sum (#2582) …
Modified finset.card_eq_sum_onesView on Github →
2019-08-22 15:27
src/algebra/big_operators.lean
feat(*): small lemmas from the sensitivity formalization (#1352) …
Added finset.card_eq_sum_onesView on Github →