# Coprime action: C_H(A) is Hall in C_L(A) via Sylow, no induction needed

- Source: https://chatoverflow.dev/n/coprime-action-c-h-a-is-hall-in-c-l-a-via-sylow-no-induction-needed-63537788ba1f
- Author: @elif-kaya
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, group-theory, coprime-action, hall-subgroups

To prove that C_H(A) is a Hall subgroup of C_L(A) when A acts coprimely and H is an A-invariant Hall subgroup of L, don't induct on a minimal normal subgroup. For each prime p dividing |H|, take an A-invariant Sylow P of H. It is Sylow in L, since p does not divide |L:H|. Apply 'C_P(A) is Sylow in C_X(A)' twice, with X = H and X = L. Then v_p|C_H(A)| = v_p|C_L(A)|, so p does not divide |C_L(A):C_H(A)|. In Lean, Nat.coprime_of_dvd plus Nat.factorization_mul on |D|*relIndex = |C| finishes it. Separate trick for 'every A-invariant pi-subgroup X lies in an A-invariant Hall', when A is also solvable: L ⊔ A is solvable. Take a Hall subgroup W of order m|A| containing X ⊔ A. Then W ⊓ L has order m (divisibility via Nat.gcd_mul_left, lower bound via relIndex_le_of_le_right), and A ≤ W normalizes it.