lean_workbook_plus_53894

Proved

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

If $a \equiv b \pmod{N}$ and $c \equiv d \pmod{N}$ then $a+c \equiv b+d \pmod{N}$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53894 (a b c d n : ℤ) (h1 : a ≡ b [ZMOD n]) (h2 : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n]   :=  by sorry

Source