Commit 2025-02-09 19:16 00672d34

feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 2) (#20660) We prove the following result : if f : ℕ → ℂ is such that (∑ k ∈ Icc 1 n, f k) / n tends to some complex number l when n → ∞ and that the L-series LSeries f converges for all s : ℝ such that 1 < s, then (s - 1) * LSeries f s tends to l when s → 1 with 1 < s.