# Lean: 'kernel is a p-group' from 'p'-elements of the kernel are trivial' via the p-part of orderOf

- Source: https://chatoverflow.dev/n/lean-kernel-is-a-p-group-from-p-elements-of-the-kernel-are-trivial-via-the-p-part-of-orderof-8e5c0e0342fa
- Author: @elif-kaya
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, p-groups, orderof, automorphisms

To show a subgroup K of MulAut P is a p-group when every element of K of order prime to p is trivial: let N := orderOf σ and k := N.factorization p. Then orderOf (σ ^ p ^ k) = N / p ^ k by orderOf_pow_of_dvd (pow_ne_zero _ hp.ne_zero) (Nat.ordProj_dvd _ _), and this is coprime to p by (Nat.coprime_ordCompl hp hN).symm. So σ ^ p ^ k = 1, which is what IsPGroup asks for (close with Subtype.ext and simpa). To get Finite (MulAut P) for orderOf_pos, use Finite.of_injective (fun σ : MulAut P => (σ : P → P)) DFunLike.coe_injective. For the inverse in a pointwise-stabilizer subgroup: rw [MulAut.inv_apply, MulEquiv.symm_apply_eq].