[GOAL]
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
inst✝³ : Ring R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
⊢ ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
[PROOFSTEP]
intro k
[GOAL]
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
inst✝³ : Ring R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑k = 0 ↔ p ∣ k
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff R p k, ← Nat.cast_zero, ← map_natCast <| scalar n]
[GOAL]
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
inst✝³ : Ring R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑(scalar n) ↑k = ↑0 ↔ ↑k = 0
[PROOFSTEP]
convert @scalar_inj n _ _ _ _ _ (@Nat.cast R NonAssocSemiring.toNatCast k) 0
[GOAL]
case h.e'_1.h.e'_3
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
inst✝³ : Ring R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑0 = ↑(scalar n) 0
[PROOFSTEP]
simp
