Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.sum_card_bipartite_above_eq_sum_card_bipartite_below

Modification history

2022-01-11 20:49
src/combinatorics/double_counting.lean
feat(combinatorics/double_counting): Double-counting the edges of a bipartite graph (#11372) …
Added finset.sum_card_bipartite_above_eq_sum_card_bipartite_belowView on Github →