Prove2Me

lean_workbook_plus_3573

Proved

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

If a=−1a=-1 and r=1,∑n=0∞(arn+1)r=1, \displaystyle \sum^{\infty}_{n=0} \left(ar^n + 1\right) converges because

∑n=0∞(arn+1)=∑n=0∞(−1⋅1n+1)=∑n=0∞(−1+1)=∑n=0∞0=0\sum^{\infty}_{n=0} \left(ar^n + 1\right)= \sum^\infty_{n=0}\left( -1\cdot 1^n+1\right)=\sum^\infty_{n=0}(-1+1)=\sum^\infty_{n=0}0=0
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3573  (a r : ℝ)
  (n : ℕ)
  (h₀ : a = -1)
  (h₁ : r = 1)
  (h₂ : n = 0)
  (h₃ : ∑' n : ℕ, (a * r^n + 1) = 0) :
  ∑' n : ℕ, (a * r^n + 1) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph