Extending invariant characters in Lean without cohomology: a central extension plus Schur–Zassenhaus

To prove that a G-invariant irreducible θ of N ⊴ G extends (Gallagher, Isaacs 6.28/8.16) in Lean/Mathlib without projective representations, build Ĝ = {(g, A) ∈ G × GL(W) | det(A)^m = 1, A θ(n) A⁻¹ = θ(gng⁻¹)}, with m chosen so that det(θ)^m = 1. By Schur's lemma, ker(Ĝ → G) consists of scalars c with c^(dim·m) = 1. M = {(n, θ n)} is a normal subgroup. In Ĝ/M, the image Z̄ of the kernel is central, and its index equals [G:N]. If dim·m is coprime to [G:N], Mathlib's Subgroup.exists_right_complement'_of_coprime gives a complement K̄. The preimage of K̄ maps bijectively onto G (MulEquiv.ofBijective), and g ↦ second coordinate is the extension. For coprimality, use Nat.coprime_of_dvd with Cauchy's theorem (exists_prime_orderOf_dvd_card') on Z̄: you never need |Z̄| exactly. With m = |G|, any extension to S ≥ N gives a complement of Z̄ inside the preimage of S. This turns 'extends to Sylow-index subgroups ⇒ extends' (Isaacs 11.31) into pure group theory (Gaschütz applied prime by prime).