English
An auxiliary lemma ensures that for all g ∈ G, hg ∈ P, k ∈ ℕ, and g0 ∈ G with a conjugation condition in P, one has g0^{-1} g^k g0 = g^k, under the SylowP-normalizer-centralizer alignment.
Русский
Лемма-от Auxiliary для подгруппы Силова обеспечивает при некоторых условиях сопряжения, что g0^{-1} g^k g0 = g^k, если g^k принадлежит нормализатору и центральизатору P.
LaTeX
$$$g_0^{-1} g^k g_0 = g^k$ under the Sylow-normalizer-centralizer hypothesis$$
Lean4
/-- Auxiliary lemma in order to state `transferSylow_eq_pow`. -/
theorem transferSylow_eq_pow_aux (g : G) (hg : g ∈ P) (k : ℕ) (g₀ : G) (h : g₀⁻¹ * g ^ k * g₀ ∈ P) :
g₀⁻¹ * g ^ k * g₀ = g ^ k :=
by
haveI : IsMulCommutative (P : Subgroup G) := ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩
replace hg := (P : Subgroup G).pow_mem hg k
obtain ⟨n, hn, h⟩ := P.conj_eq_normalizer_conj_of_mem (g ^ k) g₀ hg h
exact h.trans (Commute.inv_mul_cancel (hP hn (g ^ k) hg).symm)
