smul_def — Mathlib

English

Let g be a group element and P a Sylow p-subgroup of G. The action of g on P coincides with conjugation by g on P; i.e., g · P = g P g^{-1} for every g ∈ G and P ∈ Sylow_p(G).

Русский

Пусть g ∈ G и P —Sylow p-подгруппа G. Действие g над P совпадает с сопряжением P двойным умножением g: g · P = g P g^{-1} для всех g ∈ G и P ∈ Sylow_p(G).

LaTeX

$$$\\forall g \\in G,\\ \\forall P \\in \\mathrm{Sylow}_p(G):\\ g \\cdot P = g P g^{-1}.$$$

Lean4

theorem smul_def {g : G} {P : Sylow p G} : g • P = MulAut.conj g • P :=
  rfl

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