Theorem Finset.card_div_le

Modification history

2025-07-03 04:49
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
feat(Combinatorics/Additive): trivial bounds on doubling constant (#26636) …
Added Finset.card_div_leView on Github →