lean_workbook_plus_71332
ProvedFor and holds that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71332 (m : ℕ) (k : ℕ) : m >= 3 ∧ k > 1 → k^(m+1) ≥ 1 + k^2 := by sorry
Source
For and holds that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71332 (m : ℕ) (k : ℕ) : m >= 3 ∧ k > 1 → k^(m+1) ≥ 1 + k^2 := by sorry