lean_workbook_plus_70519
ProvedWe easily check that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70519 (k : ℕ) (h : 1 < k) : (1 : ℝ) + 1 / k + (1 / k ^ 2) + 1 / k ^ 3 < k / (k - 1) := by sorry
Source
We easily check that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_70519 (k : ℕ) (h : 1 < k) : (1 : ℝ) + 1 / k + (1 / k ^ 2) + 1 / k ^ 3 < k / (k - 1) := by sorry