case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ AddMonoidHom.ker (Int.castAddHom (ZMod n)) ↔ x✝ ∈ AddSubgroup.zmultiples ↑n
n : ℕ
⊢ AddMonoidHom.ker (Int.castAddHom (ZMod n)) = AddSubgroup.zmultiples ↑n
ext
no goals
case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ AddMonoidHom.ker (Int.castAddHom (ZMod n)) ↔ x✝ ∈ AddSubgroup.zmultiples ↑n
rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
  int_cast_zmod_eq_zero_iff_dvd]