diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean
index 2d018f26c95902..74e2e4453f6936 100644
--- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean
+++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean
@@ -26,12 +26,17 @@ namespace ModularForm
 open EisensteinSeries CongruenceSubgroup
 
 /-- This defines Eisenstein series as modular forms of weight `k`, level `Γ(N)` and congruence
-condition given by `a: Fin 2 → ZMod N`. -/
-def eisensteinSeries_MF {k : ℤ} {N : ℕ+} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
+condition given by `a : Fin 2 → ZMod N`. -/
+def eisensteinSeries_MF {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
     ModularForm (Gamma N) k where
   toFun := eisensteinSeries_SIF a k
   slash_action_eq' := (eisensteinSeries_SIF a k).slash_action_eq'
   holo' := eisensteinSeries_SIF_MDifferentiable hk a
   bdd_at_infty' := isBoundedAtImInfty_eisensteinSeries_SIF a hk
 
+/-- Normalised Eisenstein series of level 1 and weight `k`,
+here they have been scaled by `1/2` since we sum over coprime pairs. -/
+noncomputable def E {k : ℕ} (hk : 3 ≤ k) : ModularForm Γ(1) k :=
+  (1/2 : ℂ) • eisensteinSeries_MF (mod_cast hk) 0
+
 end ModularForm
diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean
index 23a37fb69d8a00..d1bce1a2b068eb 100644
--- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean
+++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean
@@ -53,12 +53,12 @@ lemma norm_le_tsum_norm (N : ℕ) (a : Fin 2 → ZMod N) (k : ℤ) (hk : 3 ≤ k
 @[deprecated (since := "2025-02-17")] alias abs_le_tsum_abs := norm_le_tsum_norm
 
 /-- Eisenstein series are bounded at infinity. -/
-theorem isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ+} (a : Fin 2 → ZMod N) {k : ℤ} (hk : 3 ≤ k)
-    (A : SL(2, ℤ)) : IsBoundedAtImInfty ((eisensteinSeries_SIF a k).toFun ∣[k] A) := by
+theorem isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ}
+    (hk : 3 ≤ k) (A : SL(2, ℤ)) : IsBoundedAtImInfty ((eisensteinSeries_SIF a k).toFun ∣[k] A) := by
   simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeries_SIF] at *
   refine ⟨∑'(x : Fin 2 → ℤ), r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k) * ‖x‖ ^ (-k), 2, ?_⟩
   intro z hz
-  obtain ⟨n, hn⟩ := (ModularGroup_T_zpow_mem_verticalStrip z N.2)
+  obtain ⟨n, hn⟩ := (ModularGroup_T_zpow_mem_verticalStrip z (NeZero.pos N))
   rw [eisensteinSeries_slash_apply, ← eisensteinSeries_SIF_apply,
     ← T_zpow_width_invariant N k n (eisensteinSeries_SIF (a ᵥ* A) k) z]
   apply le_trans (norm_le_tsum_norm N (a ᵥ* A) k hk _)