lean_workbook_plus_30752
ProvedShow that for ,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30752 (n : ℕ) (hn : 1 ≤ n) : √n ≤ n := by sorry
Source
Show that for ,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_30752 (n : ℕ) (hn : 1 ≤ n) : √n ≤ n := by sorry