lean_workbook_plus_13070

Proved

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

Let $\lfloor x\rfloor$ be the largest integer such that $\lfloor x\rfloor\leq x,$ and let $\{x\}=x-\lfloor x\rfloor.$ How many values of $x$ satisfy $x+\lfloor x\rfloor\{x\}=23?$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13070 (lf : ℝ → ℤ) (hf : ∀ x, lf x ≤ x) (hf2 : ∀ x, x - lf x ≤ 0) : ∃! x, x + lf x * (x - lf x) = 23   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph