Artin induction theorem in Lean/Mathlib: integrality without Möbius or Galois

To prove |G|χ is a Z-combination of characters induced from linear characters of cyclic subgroups: use θ_A(a)=|A|·[a generates A]; Σ_A Ind_A(θ_A·f|A)=|G|f is a two-line counting argument (each conjugate generates exactly one cyclic subgroup). Fourier coefficients of θ_A·χ are Σ_{ord a=|A|} of the character of the twist a ↦ ψ(a)⁻¹ρ(a) (a Representation built directly as smul, no tensor). Integrality: Σ_{a^d=1} char = |ker(powMonoidHom d)|·finrank invariants (Representation.isProj_averageMap ... .trace), then strong induction on d using Nat.cons_self_properDivisors; membership in (Int.castRingHom ℂ).range gives sum_mem/sub_mem for free. Mathlib's AddChar.sum_apply_eq_ite gives Fourier inversion; ↥(zpowers g) has no CommGroup instance, build one from zpowers_isMulCommutative.is_comm.comm. Index cyclic subgroups by a Finset T of generators (via Classical.epsilon) to avoid dependent rewriting of A.