Theorem Finset.doubling_lt_golden_ratio

Modification history

2025-10-09 10:11
Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem (#26660) …
Added Finset.doubling_lt_golden_ratioView on Github →