Counting primitive roots with characters in Lean: expand ∏(a_q + F_q) with Finset.prod_add

To prove 'some n ≤ X is a primitive root mod p' from character-sum bounds: take r with IsPrimitiveRoot r (p-1) (HasEnoughRootsOfUnity.exists_isPrimitiveRoot, needs import Mathlib.RingTheory.ZMod.Torsion) and ψ := e.symm hr.unit where e comes from DirichletCharacter.mulEquiv_units ℂ p (import ...DirichletCharacter.Orthogonality and RootsOfUnity.AlgebraicallyClosed for the ℂ instance). MulEquiv.orderOf_eq and ← orderOf_units give orderOf ψ = p-1, and ψ r is a primitive root of unity via MulChar.ext + eq_pow_of_pow_eq_one. For n = r^i, IsPrimitiveRoot.pow_iff_coprime turns the indicator into [i coprime m] = ∏_{q|m}(1 - [q|i]), and [q|i] = (1/q)Σ_{j<q} ζ^{(m/q)ji} (geom_sum_eq). Split off j = 0 with sum_range_succ', expand with Finset.prod_add (sum over S ∈ powerset), then Finset.prod_sum turns ∏_{q∈S} Σ_j into a sum over S.pi; the card of S.pi is easiest as prod_sum with f = 1. Nontriviality of ψ^e for e = Σ_{q∈S}(m/q)j_q, 0<j_q<q, avoids valuations: multiply by R = ∏_{q∈S, q≠q₀} q, so m | R(m/q₀)j_{q₀}, hence q₀ | R j_{q₀}, impossible. Result: #prim roots ≤ X ≥ (φ(m)/m)(X - (2^ω-1)B).