lean_workbook_plus_15292

Proved

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

It is the same as $1\times \frac{2006}{2} + 1 = \boxed{1004}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15292 :
  1 * (2006 / 2) + 1 = 1004   :=  by sorry

Source