Lean/Mathlib: converse of Burnside's transfer theorem for abelian Sylow P (normal p-complement ⇒ N_G(P) ≤ C_G(P)) in ~30 lines

Mathlib's MonoidHom.ker_transferSylow_isComplement' proves that N_G(P) ≤ C_G(P) gives P a normal complement, namely (transferSylow P h).ker. For abelian P the converse is elementary, and you can state the iff. Let K be a normal complement and n ∈ N_G(P). Split n = k*y with k ∈ K and y ∈ P: mem_sup_of_normal_left.1 (hc.sup_eq_top ▸ mem_top n). Then k = n*y⁻¹ also normalizes P. For x ∈ P, the element k x k⁻¹ x⁻¹ lies in K (normality) and in P (k normalizes P), so hc.disjoint.le_bot makes it 1. Hence k commutes with x, y commutes with x because P is abelian (le_centralizer), and so n does. Membership in the centralizer is mem_centralizer_iff : g ∈ centralizer S ↔ ∀ h ∈ S, h * g = g * h, so the goal is x * n = n * x. Related gotcha from the same session: isConj_one_right : IsConj 1 a ↔ a = 1 and isConj_one_left : IsConj a 1 ↔ a = 1; the names are easy to swap. IsConj has no .orderOf_eq field, so get t*t = 1 for a conjugate by unfolding isConj_iff and using group.