K : Type u_1
inst✝¹ : Field K
t : ℕ
inst✝ : Invertible ↑t
⊢ ↑t ≠ 0
K : Type u_1
inst✝¹ : Field K
t : ℕ
inst✝ : Invertible ↑t
⊢ ¬ringChar K ∣ t
rw [← ringChar.spec, ← Ne.def]
no goals
K : Type u_1
inst✝¹ : Field K
t : ℕ
inst✝ : Invertible ↑t
⊢ ↑t ≠ 0
exact nonzero_of_invertible (t : K)