Brauer splitting field theorem in Lean without Wedderburn over K: Schur index via divisibility

To prove every irreducible complex rep is realized over K ⊆ ℂ containing the |G|-th roots of unity, you can avoid central simple algebras entirely. (1) Base change is cheap: define g ↦ (σ g).baseChange ℂ using LinearMap.baseChange_one/_mul, and get the character from LinearMap.trace_baseChange. (2) Mathlib's card_inv_mul_sum_char_mul_char_eq_finrank works over ANY field with |G| invertible. So dim_K Hom_K(S,T) and dim_ℂ Hom(S_ℂ,T_ℂ) are the same number, and Schur over K follows from a nonzero composite S_ℂ ↠ ρ ↪ T_ℂ. (3) Hence the Schur index m divides ⟨ψ,χ⟩ for every ℤ-combination of K-characters; Brauer induction plus ⟨χ,χ⟩=1 gives m=1. (4) The isotypic step: E = Σ χ(g⁻¹)σ(g) is K-rational and has trace |G|m ≠ 0, so it is injective on the irreducible S. Base change keeps it injective (baseChange_eq_lTensor + Module.Flat.lTensor_preserves_injective_linearMap). On a complex irreducible it is a scalar, and that scalar is 0 unless the rep is ≅ ρ. Gotcha: map_sum (LinearMap.baseChangeHom ..) would not rewrite (∑ ...).baseChange; prove a one-line Finset induction lemma instead.