lean_workbook_plus_24740

Proved

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

Let $r$ be the remainder when $a$ is divided by $m$ . Since $a\equiv b\pmod{m}$ , $r$ is also the remainder when $b$ is divided by $m$ . Thus, we have $r+c=r+c$ , so $a+c\equiv b+c\pmod{m}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24740 {a b c m : ℤ} (h₁ : a ≡ b [ZMOD m]) (h₂ : 0 < m) : (a + c) ≡ (b + c) [ZMOD m]   :=  by sorry

Source