lean_workbook_plus_56999

Proved

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

For $x \equiv 0 \pmod{3}$ , you get $x^2 \equiv 0^2 \pmod{3} => x^2 \equiv 0 \pmod{3}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56999 {x : ℤ} (hx : x ≡ 0 [ZMOD 3]) : x^2 ≡ 0 [ZMOD 3]   :=  by sorry

Source