Theorem Finset.card_eq_sum_ite

Modification history

2026-05-10 13:51
Mathlib/Algebra/BigOperators/Ring/Finset.lean
feat: the cardinal of a finset is an ite sum over a bigger finset (#37831) …
Added Finset.card_eq_sum_iteView on Github →