mulAction — Mathlib

English

G acts on the set of Sylow p-subgroups by conjugation, making Sylow p G a G-set with the standard inner-action.

Русский

G действует на множество подпогрупп Силова p посредством конъюгации, делая Sylow p G G-множество с обычным действием конъюгирования.

LaTeX

$$$\\text{MulAction } G\\; (Sylow_p(G))$$$

Lean4

instance mulAction : MulAction G (Sylow p G) :=
  compHom _ MulAut.conj

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