lean_workbook_plus_64464
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64464 : ∀ x : ℝ, |x| < 1 → 1 / (1 - x) = ∑' k : ℕ, x ^ k := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_64464 : ∀ x : ℝ, |x| < 1 → 1 / (1 - x) = ∑' k : ℕ, x ^ k := by sorry