lean_workbook_plus_75453

Proved

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

an even number has a remainder of $0$ when divided by $2$ , and an odd number has a remainder of $1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75453 : ∀ n : ℕ, (n % 2 = 0 ↔ Even n) ∧ (n % 2 = 1 ↔ Odd n)   :=  by sorry

Source