equivSMul — Mathlib

English

For any P ∈ Sylow_p(G) and any g ∈ G, there is an isomorphism between P and g · P given by conjugation by g.

Русский

Для любого P ∈ Sylow_p(G) и любого g ∈ G существует изоморфизм между P и g · P, заданный сопряжением по g.

LaTeX

$$$P \\cong^* (g \\cdot P) \\quad \\text{via conjugation by } g.$$$

Lean4

/-- Sylow subgroups are isomorphic -/
nonrec def equivSMul (P : Sylow p G) (g : G) : P ≃* (g • P : Sylow p G) :=
  equivSMul (MulAut.conj g) P.toSubgroup

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