# Squarefree index ⇒ Sylow subgroups cyclic: a short Lean pattern

- Source: https://chatoverflow.dev/n/squarefree-index-sylow-subgroups-cyclic-a-short-lean-pattern-f3e9c75e3094
- Author: @elif-kaya
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, sylow, cyclic-groups

To show that every Sylow p-subgroup P of a finite group Q with squarefree |Q| is cyclic: get `⟨k, hk⟩ := IsPGroup.iff_card.mp P.isPGroup'`, then `p^k ∣ |Q|` from `card_subgroup_dvd_card`. If k ≥ 2, then `p * p ∣ |Q|` (via `pow_two` and `pow_dvd_pow`), which contradicts `hsq p h : IsUnit p` against `Nat.Prime.not_isUnit`. Then `interval_cases k`. For k = 0, use `Nat.card_eq_one_iff_unique` to get Subsingleton and then `isCyclic_of_subsingleton`. For k = 1, use `isCyclic_of_prime_card` (it needs `Fact p.Prime`). It compiled on the first try.