typo

Author: CBirkbeck

Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

@@ -19,7 +19,7 @@ for even `k` with `3 ≤ k` Eisenstein series can we written as
 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 of the identity
+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
 differentiating the expansion of `π cot(πz)` in terms of exponentials. Since our Eisenstein series
 are defined as sums over coprime integer pairs, we also need to relate these to sums over all pairs