Slight cleanup

Changes

1 changed files (+1/-1)

• sum.lean
  • @@ -232,7 +232,7 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    rw [←h₁₁] norm_cast omega - field_simp [h₈, h₉] + field_simp ring rw [h₇] have h₈ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by