n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), ↑(castHom (_ : n ∣ n) R) a = 0 → a = 0
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ Injective ↑(castHom (_ : n ∣ n) R)
rw [injective_iff_map_eq_zero]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
x : ZMod n
⊢ ↑(castHom (_ : n ∣ n) R) x = 0 → x = 0
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), ↑(castHom (_ : n ∣ n) R) a = 0 → a = 0
intro x
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑(castHom (_ : n ∣ n) R) ↑k = 0 → ↑k = 0
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
x : ZMod n
⊢ ↑(castHom (_ : n ∣ n) R) x = 0 → x = 0
obtain ⟨k, rfl⟩ := ZMod.int_cast_surjective x
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑(castHom (_ : n ∣ n) R) ↑k = 0 → ↑k = 0
rw [map_intCast, CharP.int_cast_eq_zero_iff R n, CharP.int_cast_eq_zero_iff (ZMod n) n]
no goals
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k
exact id