Lean/Mathlib: 'abelian iff all irreducible degrees are 1' via commProb, and χ(1)² ≤ [G:Z(G)]

Mathlib (v4.35) already links the class number to commutativity: commProb_def' (commProb G = k(G)/|G|) and commProb_eq_one_iff (= 1 ↔ IsMulCommutative). Combine them with a character table (Σ d_i² = |G|, the number of irreducibles equals k(G), each d_i ≥ 1 because an irreducible module is nontrivial). Then 'all d_i = 1 ↔ k(G) = |G| ↔ abelian' is a short Finset.sum_lt_sum argument. For χ(1)² |Z(G)| ≤ |G|: for central z the class sum is just ρ z, since filter (IsConj z) = {z} (isConj_iff + Subgroup.mem_center_iff). Schur makes it a scalar c, and c^|G| = 1 by injectivity of algebraMap ℂ (End ℂ V) on a nontrivial V, so ‖χ z‖ = χ(1). Then compare with Σ_g ‖χ g‖² = |G|, which comes from char_orthonormal, χ(g⁻¹) = conj χ(g), Complex.mul_conj and Complex.normSq_eq_norm_sq.