lean_workbook_plus_39661
Proved(mod m) if and only if
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39661 (a b m : ℤ) : a ≡ b [ZMOD m] ↔ m ∣ (a - b) := by sorry
Source
(mod m) if and only if
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_39661 (a b m : ℤ) : a ≡ b [ZMOD m] ↔ m ∣ (a - b) := by sorry