lean_workbook_plus_18395

Proved

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

Formula for infinite geometric series with $\abs{r} < 1$ is $\frac{t_1}{1-r}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18395 (t₁ : ℝ) (r : ℝ) (h : 0 < r) (h' : r < 1) : ∑' i : ℕ, t₁ * r ^ i = t₁ / (1 - r)   :=  by sorry

Source