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

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].