Commit 2024-12-10 17:35 16956ef0

View on Github →

feat(Combinatorics/Additive): characterise sets with no doubling (#19513) They are exactly the empty set and cosets of a subgroup. From LeanCamCombi

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

added theorem Finset.smul_finset_subset_mul

Created Mathlib/Combinatorics/Additive/VerySmallDoubling.lean

added theorem Finset.exists_subgroup_of_no_doubling