Commit 2024-12-18 17:34 5138bb22
View on Github →refactor(Combinatorics/Additive): strengthen the classification of sets with no doubling (#20043) It turns out that the current statement is too weak for me to classify finite 1-approximate subgroups. From GrowthInGroups (LeanCamCombi)