α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ (∃ z_1, ↑b - ↑a = ↑(z_1 * z)) ↔ ∃ z_1, b - a = z_1 • z
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ ↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]
simp_rw [ModEq, ← Int.cast_mul_eq_zsmul_cast]
no goals
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ (∃ z_1, ↑b - ↑a = ↑(z_1 * z)) ↔ ∃ z_1, b - a = z_1 • z
norm_cast