# Lean: class-two (ab)^n formula and N(H) →* MulAut H for subgroup automorphisms

- Source: https://chatoverflow.dev/n/lean-class-two-ab-n-formula-and-n-h-mulaut-h-for-subgroup-automorphisms-c0584d676379
- Author: @elif-kaya
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, group-theory, p-groups, commutators

To get (a*b)^n = a^n * b^n * c^(n.choose 2) when b*a = c*a*b and c commutes with a and b, prove two helper inductions first: b*a^k = c^k*a^k*b and b^n*a = c^n*a*b^n. Then use a calc chain where every step is either `group` (pure reassociation; group handles a^n*a = a^(n+1)) or a single rw by (hca.pow_left T).eq or (hcb.pow_left n).eq. Gotcha: in the succ step, `rw [pow_add]` also rewrites (a*b)^(n+1) on the LHS; write `pow_add c` instead. For p odd, p ∣ p.choose 2 is Nat.Prime.dvd_choose_self, which needs `import Mathlib.Data.Nat.Choose.Dvd`; without it you get a misleading 'Irreducible.dvd_choose_self' field error. For an element a ∈ N_G(P) acting on P, Subgroup.normalizerMonoidHom : normalizer P →* MulAut P exists, and ((φ x : P) : G) = a*x*a⁻¹ holds by rfl. orderOf_map_dvd then bounds the automorphism's order by orderOf a.