Lean/Mathlib: χ(1) ∣ [G:Z(G)] by tensor powers without proving the outer tensor power irreducible

Tate's tensor-power proof of χ(1) | [G:Z] usually needs ρ^{⊠m} to be irreducible on G^m, which is painful in Mathlib. You can skip that. Integrality criterion: let τ be a representation of a finite group Γ in which every class sum acts by a scalar, and let φ be a class function with integral values. If ∑ φ(γ)•τ(γ) = r•1, then r is integral: regroup the sum by ConjClasses with Finset.sum_fiberwise; the class-sum scalars are integral because ℤ[Γ] is finite over ℤ. You get scalar class sums from scalar conjugation averages ∑_ζ τ(ζ g ζ⁻¹) by swapping sums. For τ(x) = PiTensorProduct.map (ρ ∘ x) on Fin m → G, every average and every ∑ φ•τ factors through multilinearity: (PiTensorProduct.mapMultilinear ℂ _ _).map_sum and .map_smul_univ, plus Schur for each factor. The representation is PiTensorProduct.mapMonoidHom.comp (MonoidHom.pi fun i ↦ ρ.comp (Pi.evalMonoidHom _ i)). Pass to Γ = G^m ⧸ D with D = (∏-hom Z^m → Z).ker mapped by MonoidHom.compLeft Z.subtype, and use QuotientGroup.lift. Sum over the quotient with QuotientGroup.card_preimage_mk: ∑_x F(mk x) = |D| • ∑_q F q. Nontriviality of ⨂V comes from Basis.piTensorProduct. Gotchas: the notation ⨂[ℂ] needs open scoped _root_.TensorProduct inside namespace Representation, otherwise Representation.TensorProduct shadows it. To define a central character by choose, generalize (…).choose = a at h ⊢ before rewriting ρ ↑z, or rw fails with 'motive is not type correct'.