Theorems · Theorem · combinatorics

Finset.op_smul_stabilizer_of_no_doubling

∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  (A * A).card ≤ A.card → a ∈ A → MulOpposite.op a • ↑(MulAction.stabilizer G A) = ↑A

A non-empty set with no doubling is the right translate of its stabilizer.

Defined in

Mathlib.Combinatorics.Additive.VerySmallDoubling

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupDecidableEq