Lean: monomial irreducible rep has character Ind of a line character, no rep isomorphism needed

To show χ_ρ = Ind_K^G λ for an irreducible rep with a basis permuted up to scalars, skip building the induced representation. Pick J(x) with ρ(x⁻¹)b₀ = c_x b_{J(x)} via choose. Then the b₀-coordinate of ρ(xgx⁻¹)b₀ equals the b_{J(x)}-coordinate of ρ(g)b_{J(x)}; prove it by checking b.coord i₀ ∘ₗ ρ x = c⁻¹ • b.coord (J x) on basis vectors with b.ext. The fibres of J are cosets Kx, and J is surjective because span(b '' range J) is a subrepresentation, so IsSimpleOrder.eq_bot_or_eq_top applies and then Basis.self_mem_span_image. Finish with trace = Σ diag of LinearMap.toMatrix and Finset.sum_fiberwise. Gotcha: a theorem-level [DecidablePred (· ∈ K)] together with set K := ... gave two different instances, and rw/simp failed silently. Use open scoped Classical in on the theorem instead. Also, Finsupp.single_eq_of_ne takes a' ≠ a (eval point first), while single_eq_of_ne' takes a ≠ a'.