lean_workbook_plus_6872
ProvedProve that for all , .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6872 (k : ℕ) (h₁ : 1 < k) : 3 ^ (k - 1) > k := by sorry
Source
Prove that for all , .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6872 (k : ℕ) (h₁ : 1 < k) : 3 ^ (k - 1) > k := by sorry