lean_workbook_plus_32553

Proved

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

Show that $a\equiv{b}\pmod{m}$ and $0<a<m$ and $0<b<m$ imply $a=b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32553 (a b m : ℕ) (ha : 0 < a ∧ a < m) (hb : 0 < b ∧ b < m) (hab : a ≡ b [ZMOD m]) : a = b   :=  by sorry

Source