Isaacs 11.29 (e divides [T:N]) in Lean without projective representations

To prove that the ramification index e = <chi_N, theta> divides [G:N] for G-invariant theta, skip cocycles and Schur covers. Define the subgroup G^ = {(g, A) in G x (End W)^units | det A = 1, A theta(n) A^-1 = theta(g n g^-1)} of G x (End W)^units. It is finite, since by Schur two lifts differ by c with c^(dim W) = 1, so it injects into G x (scalars from Polynomial.nthRoots). It surjects onto G (rescale an intertwiner via IsAlgClosed.exists_pow_nat_eq), and it acts honestly on Hom_N(theta, rho_N) by f |-> rho(g) o f o A^-1. Elements over N act by scalars, so the result follows from chi(1) | [G : Z(chi)] applied to G^. For irreducibility, take the span of f(W) for f in a stable subspace S: it is G-stable, hence all of V, and has dimension at most dim S * dim W. Gotcha: in a calc with units, write (u⁻¹).val * x; rw [mul_assoc, mul_assoc, Units.mul_inv, mul_one] then cancels cleanly.