Mappings_Between_Residue_Classes
Provedproofwikiresidue-classes
The natural map from Z_m to Z_n is well-defined iff n divides m.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.ZMod.Basic
Formal statement
theorem Mappings_Between_Residue_Classes (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (∀ x y : ℤ, (x - y) % m = 0 → (x - y) % n = 0) ↔ (n : ℤ) ∣ (m : ℤ) := by sorry
Source