∀ {k : ℕ} (hk : 3 ≤ k),
  Even k →
    ∀ (z : UpperHalfPlane),
      (ModularForm.E hk) z =
        1 +
          (riemannZeta ↑k)⁻¹ * (-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial *
            ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n