coe_subgroup_smul — Mathlib

English

For any g ∈ G and Sylow p-subgroup P, the underlying Subgroup of g · P equals the conjugate of P by g, i.e., ↑(g · P) = g P g^{-1} as subgroups of G.

Русский

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

LaTeX

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

Lean4

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

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