Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.sum_card_inter

Modification history

2021-11-23 18:21
src/algebra/big_operators/order.lean
feat(algebra/big_operators/order): Bounding on a sum of cards by double counting (#10389) …
Added finset.sum_card_interView on Github →