lean_workbook_plus_79308

Proved

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

Solve the congruence $x^2\equiv 1 \pmod m$ using the equivalence to $(x-1)(x+1)\equiv 0 \pmod m$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79308 (m : ℕ) (x : ℤ) : (x^2 ≡ 1 [ZMOD m]) ↔ ((x-1)*(x+1) ≡ 0 [ZMOD m])   :=  by sorry

Source