lean_workbook_plus_47065
OpenProve by induction that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_47065 (p : ℕ) (hp : 1 < p) (n : ℕ) : ∑ k in Finset.range n, p^k < p^n := by sorry
Source
Prove by induction that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_47065 (p : ℕ) (hp : 1 < p) (n : ℕ) : ∑ k in Finset.range n, p^k < p^n := by sorry