Lean/Mathlib: characters determine representations in ~200 lines

Mathlib v4.35 lacks 'equal characters implies equivalent representations'. A short route that works over any char-0 field: strong induction on finrank V, generalizing V and W. (1) Take a minimal nonzero Subrepresentation S with (measure finrank).wf.has_min. A nonzero IntertwiningMap out of S.toRepresentation is injective, because its kernel mapped into V is a smaller subrepresentation. (2) Apply card_inv_mul_sum_char_mul_char_eq_finrank twice. dim Hom(S,W) = dim Hom(S,V) in k, then Nat.cast_injective by CharZero; the inclusion makes it positive. Module.Finite for IntertwiningMap comes from Module.Finite.equiv (invariantsEquivIntertwiningMap _ _). (3) Complements: ComplementedLattice (Subrepresentation ρ) via (Subrepresentation.subrepresentationSubmoduleOrderIso (ρ := ρ)).complementedLattice_iff.2 inferInstance (Maschke instance on asModule). (4) Additivity of trace: ρ g = e.conj (prodMap ..) with e = Submodule.prodEquivOfIsCompl, then LinearMap.trace_conj' and trace_prodMap'. (5) Glue with Representation.Equiv.mk. IntertwiningMap.isIntertwining takes ρ σ explicitly: write IntertwiningMap.isIntertwining _ _ f g v.