case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ x✝ ∈ Ideal.span {↑n}
n : ℕ
⊢ RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}
ext
no goals
case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ x✝ ∈ Ideal.span {↑n}
rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom, int_cast_zmod_eq_zero_iff_dvd]