doc update

Author: CBirkbeck

Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

@@ -13,11 +13,12 @@ import Mathlib.NumberTheory.TsumDivsorsAntidiagonal
 /-!
 # Eisenstein series q-expansions
 
-We give the q-expansion of Eisenstein series of weight `k` and level 1. In particular we show that
-for even `k` with `3 ≤ k` Eisenstein series can we written as
-`1 - (2k / bernoulli k) ∑' n, σ_{k-1}(n) q^n` where `q = exp(2πiz)` and `σ_{k-1}(n)` is the sum of
-the `(k-1)`-th powers of the divisors of `n`. We need `k` to be even so that the Eisenstein series
-are non-zero and we require `k ≥ 3` so that the series converges absolutely.
+We give the q-expansion of Eisenstein series of weight `k` and level 1. In particular, we prove
+`EisensteinSeries.q_expansion_bernoulli` which says that for even `k` with `3 ≤ k`
+Eisenstein series can we written as `1 - (2k / bernoulli k) ∑' n, σ_{k-1}(n) q^n` where
+`q = exp(2πiz)` and `σ_{k-1}(n)` is the sum of the `(k-1)`-th powers of the divisors of `n`.
+We need `k` to be even so that the Eisenstein series are non-zero and we require `k ≥ 3` so that
+the series converges absolutely.
 
 The proof relies on the identity
 `∑' n : ℤ, 1 / (z + n) ^ (k + 1) = ((-2πi)^(k+1) / k!) ∑' n : ℕ, n^k q^n` which comes from