m n a b c d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
m n a b c d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ d ∣ a ↔ d ∣ b
simp only [← modEq_zero_iff_dvd]
m n a b c d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
m n a b c d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
replace h := h.of_dvd hdm
no goals
m n a b c d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
exact ⟨h.symm.trans, h.trans⟩