lean_workbook_plus_35594
Provedprove :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35594 (p : ℕ) (k : ℕ) (h₁ : p * p ≤ k) (h₂ : k < (p + 1) * (p + 1)) : ⌊Real.sqrt k⌋ = p := by sorry
Source
prove :
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35594 (p : ℕ) (k : ℕ) (h₁ : p * p ≤ k) (h₂ : k < (p + 1) * (p + 1)) : ⌊Real.sqrt k⌋ = p := by sorry