lean_workbook_plus_37712

Proved

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

If $n$ is a square, then $\sqrt{n}-\left\lfloor\sqrt{n}\right\rfloor=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37712 (n : ℕ) (h : ∃ k, k^2 = n) : √n - ⌊√n⌋ = 0   :=  by sorry

Source