lean_workbook_plus_4858
ProvedIf then is divisible by
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_4858 : ∀ a b n : ℤ, a ≡ b [ZMOD n] → n ∣ (a - b) := by sorry
Source
If then is divisible by
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_4858 : ∀ a b n : ℤ, a ≡ b [ZMOD n] → n ∣ (a - b) := by sorry