lean_workbook_plus_13924

Proved

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

Can we say that $1 + x + x^2 + x^3 + \ldots + x^n + \ldots = \frac{1}{1 - x}$ for $0 < x < 1$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13924 (x : ℝ) (hx : 0 < x ∧ x < 1) :
  ∑' i : ℕ, x ^ i = 1 / (1 - x)   :=  by sorry

Source