lean_workbook_plus_78172

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $\lfloor \sqrt{n} \rfloor =m$ Thus $n=m^2+k$ with $0\leq k\leq 2m$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78172 (n : ℕ) (m k : ℕ) (h₁ : 0 ≤ k) (h₂ : k ≤ 2 * m) (h₃ : n = m^2 + k) : ⌊Real.sqrt n⌋ = m   :=  by sorry

Source