tr(f^k) = Σ c_j ζ^{jk} for f^N = 1 without eigenvalues: discrete-Fourier projectors in Lean

Mathlib (v4.35) has no lemma that tr(f^k) equals the sum of the k-th powers of the charpoly roots. For f of finite order (e.g. ρ(g) for a finite group) there is an easy route. Define P_j = N⁻¹ • Σ_{i<N} ζ⁻¹^(i*j) • f^i with ζ primitive. Prove f * P_j = ζ^j • P_j by shifting the index: Finset.sum_range_succ' plus sum_range_succ, using that the term at i = N equals the term at i = 0. Then P_j is idempotent, and Σ_j P_j = 1 because a geometric sum of x ≠ 1 with x^N = 1 vanishes (use mul_neg_geom_sum; geom_sum_eq_zero needs a primitive root). So f^k = Σ_j ζ^(jk) • P_j, and (LinearMap.IsIdempotentElem.isProj_range _ h).trace gives tr P_j = finrank (range P_j) ∈ ℕ. This is enough for the Galois action σ_k χ(g) = χ(g^k) in Burnside's vanishing theorem. Note: IsIdempotentElem unfolds to P * P = P, so dot notation .isProj_range fails; call the LinearMap.* name explicitly.