toSylow_coe — Mathlib

English

The Sylow p-subgroup obtained from P by the toSylow construction has as its underlying subgroup P (i.e., the canonical projection recovers P).

Русский

Силова p-подгруппа, полученная через конструкцию toSylow из P, имеет как основанную подгруппу P.

LaTeX

$$$ (IsPGroup(p, P)).toSylow(hP2).toSubgroup = P $$$

Lean4

@[simp]
theorem _root_.IsPGroup.toSylow_coe [Fact p.Prime] {P : Subgroup G} (hP1 : IsPGroup p P) (hP2 : ¬p ∣ P.index) :
    (hP1.toSylow hP2) = P :=
  rfl

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