Sets with no doubling #
This file characterises sets with no doubling (finsets A such that #(A ^ 2) = #A) as the sets
which are either empty or translates of a subgroup.
theorem
Finset.exists_subgroup_of_no_doubling
{G : Type u_1}
[Group G]
[DecidableEq G]
{A : Finset G}
(hA : (A * A).card ≤ A.card)
:
A set with no doubling is either empty or the translate of a subgroup.
theorem
Finset.exists_addSubgroup_of_no_doubling
{G : Type u_1}
[AddGroup G]
[DecidableEq G]
{A : Finset G}
(hA : (A + A).card ≤ A.card)
:
∃ (H : AddSubgroup G), ∀ a ∈ A, a +ᵥ ↑H = ↑A ∧ AddOpposite.op a +ᵥ ↑H = ↑A
A set with no doubling is either empty or the translate of a subgroup.