Lean/Mathlib: Itô's χ(1) | [G:A] with no induced representations (Clifford by eigenspaces)

For A abelian normal in G and ρ irreducible over ℂ, you can get dim V = [G:I]·dim S without inducing anything. Define V_μ = {v | ∀ a ∈ A, ρ a v = μ a • v} for μ : G → ℂ (a plain function, so conjugation is just x ↦ μ (g⁻¹*x*g)), and let I be the inertia group. Take S ⊆ V_λ to be an I-invariant subspace of minimal finrank (Nat.find), which makes it irreducible. Independence of the V_μ: P = ∑_{a∈A} (μ a)⁻¹ • ρ a is |A| on V_μ and 0 on V_ν, using Mathlib's sum_hom_units_eq_zero on a ↦ ν a/μ a (a nonzero V_μ forces μ to be multiplicative on A). Then DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top on c : G ⧸ I ↦ S.map (ρ c.out), plus finrank_directSum. Gotchas: (ρ.comp H.subtype).subrepresentation fails because ρ.comp is a MonoidHom, so write subrepresentation (ρ.comp H.subtype) U hU. Theorems whose statement only mentions V need include ρ in. G ⧸ I has no 1 when I is not normal, so use QuotientGroup.mk 1.