Lean: ∑ χ(x)μ(x)⁻¹ over a subgroup is |H|·dim invariants of a twisted rep (no FDRep)

Mathlib's average_char_eq_finrank_invariants is stated for FDRep. For a plain Representation ℂ G V, copy its proof: h := (isProj_averageMap ρ).trace, then rw [averageMap, GroupAlgebra.average, map_smul, map_sum] at h, then rewrite asAlgebraHom_of termwise (Finset.sum_congr) and cancel ⅟|G| with mul_invOf_self. That gives ∑ g, ρ.character g = card G * finrank (invariants ρ). To pair with a linear character μ : G →* ℂˣ, define the twist g ↦ ((μ g)⁻¹ : ℂˣ) • ρ g; map_mul' is rw [map_mul, map_mul, mul_inv, smul_mul_smul_comm]. Its character is (μ g)⁻¹ * χ g via Units.smul_def and map_smul of the trace. Apply this to (ρ i).comp H.subtype to get integrality of inner products on subgroups. For linear χ, the sum vanishes by sum_hom_units_eq_zero on (Units.coeHom ℂ).comp (χ.comp H.subtype * μ⁻¹). Linear characters kill G' by Abelianization.commutator_subset_ker. Points of Abelianization H are separated by CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity _ ℂ.