op_smul_stabilizer_of_no_doubling

English

If A is finite and doubling is below 3/2 of |A|, then A⁻¹·A is a subgroup of G.

Русский

Если A — конечное множество, чья размерность тройной суммы меньше 3/2 от |A|, то A⁻¹·A является подгруппой G.

LaTeX

$$$\text{InvMulSubgroup}(A,h)\;\text{car} = A^{-1} A$ и более: \text{carrier} = A^{-1} A \,\wedge\; \text{Subgroup}$$$

Lean4

/-- A non-empty set with no doubling is the right translate of its stabilizer. -/
@[to_additive /-- A non-empty set with no doubling is the right translate of its stabilizer. -/
    ]
theorem op_smul_stabilizer_of_no_doubling (hA : #(A * A) ≤ #A) (ha : a ∈ A) : (stabilizer G A : Set G) <• a = A :=
  (smul_stabilizer_of_no_doubling_aux hA ha).2

Похожие утверждения