lean_workbook_plus_45051Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)Case 1( a\mathbf{a}a is even): Thus x=2b+yx=2b+yx=2b+y for some natural number bbb . Then: [x]=[2b+y]=2b[x]=[2b+y]=2b[x]=[2b+y]=2b and [x2]=[2b+y2]=[b+y2]=b\left[ {\frac{x}{2}} \right] = \left[ {\frac{{2b + y}}{2}} \right] = \left[ {b + \frac{y}{2}} \right] = b[2x]=[22b+y]=[b+2y]=b because y/2y/2y/2 is less than 111 . So, [x]−2[x2]=2b−2b=0\left[ x \right] - 2\left[ {\frac{x}{2}} \right] = 2b - 2b = 0[x]−2[2x]=2b−2b=0 .Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_45051 (x : ℕ) (h₀ : Even x) : (x : ℤ) - 2 * (x / 2) = 0 := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph