simpa [h] using CharP.char_is_prime_or_zero K (ringChar K)
case inl
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
h : ringChar K = 1
⊢ ringChar K = n
no goals