Theorem Finset.one_le_mulConst

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_mulConstView on Github →