Prove2Me

thm_0_999_1

Proved

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

0-999-1direct-proofsnumber-theoryproofwiki

0.999... = 1

Preamble
import Mathlib.Topology.Algebra.InfiniteSum.Real
import Mathlib.Tactic
Formal statement
theorem thm_0_999_1 : ∑' (n : ℕ), (9 : ℝ) / 10 * (1 / 10) ^ n = 1 := by sorry
Source
https://proofwiki.org/wiki/0.999...=1

View graph