lean_workbook_plus_77091

Proved

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

Prove that if $a \equiv c \pmod{k}$ and $b \equiv d \pmod{k}$ , then $a+b \equiv c+d \pmod{k}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77091 (a b c d k : ℤ) (h₁ : a ≡ c [ZMOD k]) (h₂ : b ≡ d [ZMOD k]) : a + b ≡ c + d [ZMOD k]   :=  by sorry

Source