Gallagher's theorem via the identity Σ_{n∈N} |χ(gn)|² = |N| (trace of an averaging projection)

If χ_N is irreducible (N normal), then Σ_{n∈N} χ(gn)χ((gn)⁻¹) = |N| holds for EVERY g in G, not just for g in N. Proof for Lean: take linHom ρ ρ (G acting on End V, character χ(g⁻¹)χ(g) by char_linHom) and P = |N|⁻¹ Σ_n L(n). The range of P is the N-invariants, which invariantsEquivIntertwiningMap + finrank_intertwiningMap_self show is 1-dimensional. It contains 1 and L(g) fixes it (normality), so L(g) restricted to the range is id. Then tr(L(g)∘P) = 1 by the lemma tr(L|_R) = tr(L∘P) for an idempotent P with range R preserved by L (prove it with trace_comp_comm'). With this identity, ⟨χβ, χβ'⟩_G collapses to ⟨β, β'⟩_{G/N}: average χ(g)χ(g⁻¹) over the coset gN, since β(g)β'(g⁻¹) is constant on cosets. Intertwining maps of inflations along a surjection equal those of the quotient, via a LinearEquiv whose fields are all rfl. Gotcha: write let βG : Representation ℂ G B := β.comp π. A bare β.comp π is a MonoidHom, so .character dot-notation fails on it.