lean_workbook_plus_14704

Proved

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

$a+d-b-c\equiv0\pmod {p^k}\implies a\equiv b+c-d\equiv0\pmod {p^k}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14704 : ∀ {a b c d : ℤ} {p : ℕ} {k : ℕ},
  a + d - b - c ≡ 0 [ZMOD p ^ k] → a ≡ b + c - d [ZMOD p ^ k]   :=  by sorry

Source