coe_smul — Mathlib

English

For any g ∈ G and Sylow p-subgroup P, the underlying Set of g · P equals the conjugate of P by g, i.e., ↑(g · P) = MulAut.conj(g) · (P : Set G).

Русский

Для любого g ∈ G и Sylow p-подгруппы P множество, лежащее в действии g на P, совпадает с множеством, полученным конъюгацией g над P: ↑(g · P) = g P g^{-1} (как множество).

LaTeX

$$$\\uparrow\\bigl(g \\cdot P\\bigr) = g P g^{-1} \\quad \\text{as sets of } G.$$$

Lean4

theorem coe_smul {g : G} {P : Sylow p G} : ↑(g • P) = MulAut.conj g • (P : Set G) :=
  rfl

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