lean_workbook_plus_34018
ProvedGiven , prove that for any integer .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34018 {a b c n : ℤ} (h₁ : a ≡ b [ZMOD n]) : a + c ≡ b + c [ZMOD n] := by sorrySource
Given , prove that for any integer .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_34018 {a b c n : ℤ} (h₁ : a ≡ b [ZMOD n]) : a + c ≡ b + c [ZMOD n] := by sorry