m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
unfold ModEq Nat.ModEq
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
rw [← Int.ofNat_inj]
no goals
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
simp [coe_nat_mod]