R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
⊢ False
R : Type u_1
inst✝² : NonAssocRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Finite R
⊢ p ≠ 0
rintro rfl
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
⊢ False
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
⊢ False
haveI : CharZero R := charP_to_charZero R
case intro
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
val✝ : Fintype R
⊢ False
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
⊢ False
cases nonempty_fintype R
no goals
case intro
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
val✝ : Fintype R
⊢ False
exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))