rw [← Nat.cast_eq_ofNat, ringChar.spec] at hn
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : OfNat.ofNat n = 0
hnp : Nat.Prime n
⊢ ringChar K = n
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
⊢ ringChar K = n