unique_of_normal — Mathlib

English

If a normal Sylow p-subgroup exists in G, it is the unique Sylow p-subgroup of G.

Русский

Если в G существует нормальная Sylow p-подгруппа, она уникальна среди Sylow p-подгрупп.

LaTeX

$$Unique (Sylow p G)$$

Lean4

/-- If `G` has a normal Sylow `p`-subgroup, then it is the only Sylow `p`-subgroup. -/
noncomputable def unique_of_normal {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) (h : P.Normal) :
    Unique (Sylow p G) := by
  refine { uniq := fun Q ↦ ?_ }
  obtain ⟨x, h1⟩ := exists_smul_eq G P Q
  obtain ⟨x, h2⟩ := exists_smul_eq G P default
  rw [smul_eq_of_normal] at h1 h2
  rw [← h1, ← h2]

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