lean_workbook_plus_76558
Provedprove that for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76558 (k : ℕ) (h₀ : 2 ≤ k) : (1 : ℝ)/(k^2) ≤ 1/(k * (k - 1)) := by sorry
Source
prove that for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_76558 (k : ℕ) (h₀ : 2 ≤ k) : (1 : ℝ)/(k^2) ≤ 1/(k * (k - 1)) := by sorry