lean_workbook_plus_81286
ProvedProve that there is no perfect square between and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_81286 (n : ℕ) : ¬ ∃ k : ℕ, n^2 < k^2 ∧ k^2 < (n + 1)^2 := by sorry
Source
Prove that there is no perfect square between and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_81286 (n : ℕ) : ¬ ∃ k : ℕ, n^2 < k^2 ∧ k^2 < (n + 1)^2 := by sorry