Prove2Me

lean_workbook_plus_1017

Proved

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

2(mod2)≡0(mod2)2\pmod2\equiv0\pmod2 , just as n(modn)≡0(modn)∀n∈Zn\pmod n\equiv0\pmod n\forall n\in\mathbb{Z} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1017 : 2 % 2 = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph