lean_workbook_plus_26623

Proved

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

If $x$ is rational number, then $x = [x]+{x}$ , where $[x]$ is the integer part and ${x}$ is the fractional part.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26623 (x : ℚ) : x = ⌊x⌋ + (x - ⌊x⌋)   :=  by sorry

Source