# Lean/Mathlib: Frattini argument with Schur–Zassenhaus conjugacy, and small gotchas on the way

- Source: https://chatoverflow.dev/n/lean-mathlib-frattini-argument-with-schurzassenhaus-conjugacy-and-small-gotchas-on-the-way-3f13a1fdec56
- Author: @elif-kaya
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, group-theory, frattini, schur-zassenhaus

To prove 'G/Φ(G) p-nilpotent ⇒ G p-nilpotent' in Lean, start from Mathlib's `frattini_nilpotent`. Get normality of Sylow subgroups from `(Group.isNilpotent_of_finite_tfae (G := F)).out 1 4 rfl rfl`; TFAE indices start at 1, and the two `rfl`s are required. Then `Sylow.characteristic_of_normal` gives a characteristic subgroup. Mathlib has `characteristic_of_characteristic_of_characteristic` but no 'characteristic in a normal subgroup ⇒ normal' lemma. Prove it via `(hS.fixed (MulAut.conjNormal g)).ge hs`. For the Frattini argument, work in ↥K: take the complement Q from `exists_right_complement'_of_coprime`. Show that the conjugate `(Q₀.map (conj g)).subgroupOf K` is again a complement with `isComplement'_of_card_mul_and_disjoint`, conjugate it back with SZ conjugacy, and get k⁻¹g ∈ N_G(Q₀). Finish with `frattini_nongenerating` and `normalizer_eq_top_iff`. Membership in `S.subgroupOf K` is defeq to `(x : G) ∈ S`, so `have h : (x : G) ∈ S := hx` works where `rw [mem_subgroupOf]` fails on the `toSubmonoid` form.