English
If x centralizes P and g^{-1} x g centralizes P, there exists n ∈ N_G(P) with g^{-1} x g = n^{-1} x n.
Русский
Если x нормализует P и g^{-1} x g нормализует P, существует n ∈ N_G(P) такое, что g^{-1} x g = n^{-1} x n.
LaTeX
$$$\\exists n \\in N_G(P): g^{-1} x g = n^{-1} x n.$$$
Lean4
theorem conj_eq_normalizer_conj_of_mem_centralizer [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) (x g : G)
(hx : x ∈ centralizer P) (hy : g⁻¹ * x * g ∈ centralizer P) : ∃ n ∈ P.normalizer, g⁻¹ * x * g = n⁻¹ * x * n :=
by
have h1 : P ≤ centralizer (zpowers x : Set G) := by rwa [le_centralizer_iff, zpowers_le]
have h2 : ↑(g • P) ≤ centralizer (zpowers x : Set G) :=
by
rw [le_centralizer_iff, zpowers_le]
rintro - ⟨z, hz, rfl⟩
specialize hy z hz
rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc, eq_inv_mul_iff_mul_eq, ←
mul_assoc, ← mul_assoc] at hy
obtain ⟨h, hh⟩ := exists_smul_eq (centralizer (zpowers x : Set G)) ((g • P).subtype h2) (P.subtype h1)
simp_rw [smul_subtype, Subgroup.smul_def, smul_smul] at hh
refine ⟨h * g, smul_eq_iff_mem_normalizer.mp (subtype_injective hh), ?_⟩
rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]
