lean_workbook_plus_11736

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find if the series converges or diverges and if it converges, find its value.\n

\sum_{n=1}^{\infty}\frac1{n^2+1}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11736 (f : ℕ → ℝ) (hf : ∀ n, f n = 1 / (n ^ 2 + 1)) : ∃ l, ∑' n : ℕ, f n = l   :=  by sorry

Source