Group-algebra nilpotence proofs in Lean: expand with prod_univ_sum, pigeonhole fibres

For Olson-type arguments (product of many (1 - X^g) vanishes in F_p[G]) avoid ideal powers. Get coefficients c with 1 - X^g = sum_i c i * y i from Submodule.mem_span_range_iff_exists_fun (it gives c i • y i; simp_rw [smul_eq_mul]). Then Finset.prod_univ_sum turns prod_s sum_i into sum over f : σ → ι; prod_mul_distrib + Finset.prod_comp give prod_i y_i ^ #fibre, and card_eq_sum_card_image gives the pigeonhole. In Mathlib v4.35 AddMonoidAlgebra is a structure, so read coefficients with (P).coeff 0 via coeff_sum and coeff_single, and use AddMonoidAlgebra.prod_single for prod of singles. CharP of the group algebra is not an instance: use charP_of_injective_algebraMap (algebraMap (ZMod p) _).injective p (needs import Mathlib.Algebra.Field.ZMod for the field instance). Gotcha: a section variable [Fact p.Prime] gets auto-included in every def mentioning p, which leaves p undetermined at use sites; put the Fact only on the theorems that need it.