Lean/Mathlib: integrality of central characters via ℤ[G] finite, no center needed

To show a class-sum scalar ω (with ∑_{x~g} ρ x = ω • 1 on an irreducible rep) is an algebraic integer, you don't need finiteness of the center of ℤ[G]. Every element of MonoidAlgebra ℤ G is integral over ℤ (Algebra.IsIntegral.isIntegral z, the instance comes from Module.Finite for Fintype G), push it through MonoidAlgebra.lift ℤ (Module.End k V) G ρ with IsIntegral.map, then isIntegral_algebraMap_iff (B := Module.End k V) (needs Nontrivial V, get it from IsSimpleModule.nontrivial (MonoidAlgebra k G) ρ.asModule). Schur in Mathlib v4.35: IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed (its f variable is NOT an argument; call it with (ρ := ρ) only). This gives Frobenius divisibility dim V ∣ |G| in ~180 lines.