lean_workbook_plus_2893

Proved

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

Let $x\in[0,1)$ : $\sum_{n=0}^{+\infty}x^n=\frac 1{1-x}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source