Theorem Finset.mulConst_le_card

Modification history

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