lean_workbook_plus_55532

Proved

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

0 is an even number because an even number is any integer that can be evenly divided by 2, and 0 can be even divided by 2 ( $\frac{0}{2}=0$ ).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55532 : 0 % 2 = 0   :=  by sorry

Source