Theorem Finset.exists_subgroup_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) …
Deleted Finset.exists_subgroup_of_no_doublingView on Github →
2024-12-10 17:35
Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
feat(Combinatorics/Additive): characterise sets with no doubling (#19513) …
Added Finset.exists_subgroup_of_no_doublingView on Github →