smul_stabilizer_of_no_doubling — Mathlib

English

For finite A,B,C, |A/C| · |B| ≤ |A/B| · |B C|.

Русский

Для конечных A,B,C выполняется |A/C| · |B| ≤ |A/B| · |B C|.

LaTeX

$$$|A/C|\,|B| \le |A/B|\,|B C|$$$

Lean4

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

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