conj_eq_normalizer_conj_of_mem — Mathlib

English

If P is Sylow and x ∈ P, and g^{-1} x g ∈ P, then there exists n ∈ P.normalizer with g^{-1} x g = n^{-1} x n.

Русский

Если P — Sylow, x ∈ P и g^{-1} x g ∈ P, то существует n ∈ N_G(P) такое, что g^{-1} x g = n^{-1} x n.

LaTeX

$$$\\exists n \\in P.N_G: g^{-1} x g = n^{-1} x n.$$$

Lean4

theorem conj_eq_normalizer_conj_of_mem [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) [_hP : IsMulCommutative P]
    (x g : G) (hx : x ∈ P) (hy : g⁻¹ * x * g ∈ P) : ∃ n ∈ P.normalizer, g⁻¹ * x * g = n⁻¹ * x * n :=
  P.conj_eq_normalizer_conj_of_mem_centralizer x g (P.le_centralizer hx) (P.le_centralizer hy)

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