lean_workbook_plus_56300

Proved

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

Prove $1+x+x^{2}+x^{3}+\\dots=\frac{1}{1-x}$ for $\\mid x\\mid < 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source