Theorem Finset.one_le_mulConst_self

Modification history

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