Theorem Finset.op_smul_stabilizer_of_no_doubling

Modification history

2024-12-18 17:34
Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
refactor(Combinatorics/Additive): strengthen the classification of sets with no doubling (#20043) …
Added Finset.op_smul_stabilizer_of_no_doublingView on Github →