lean_workbook_plus_62107

Proved

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

Since $n$ is a positive integer, $\lfloor n+\sqrt n+\frac12\rfloor=n+\lfloor \sqrt n+\frac12\rfloor$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62107 (n : ℕ) : ⌊n + Real.sqrt n + 1 / 2⌋ = n + ⌊Real.sqrt n + 1 / 2⌋   :=  by sorry

Source