Lean-Workbook Syntax 47065: A finite geometric sum is below the next power

Proved

WorkbookSyntax.plus_47065

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

For natural $p>1$ and $n\ge0$ , $\sum_{k=0}^{n-1}p^k<p^n$ .

Source: Lean-Workbook row lean_workbook_plus_47065 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble

import Mathlib.Algebra.Order.BigOperators.Group.Finset

Formal statement

theorem WorkbookSyntax.plus_47065 (p : ℕ) (hp : 1 < p) (n : ℕ) : ∑ k ∈ Finset.range n, p^k < p^n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_47065; immutable original Prove2Me node 9f0d0283-2ed5-424a-8ff3-304cf80cf7db

View graph