case zero
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 0

case prime
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hq : ExpChar R 1
⊢ p = 0
cases hq
no goals
case zero
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 0
exact CharP.eq R hp inferInstance
no goals
case prime
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0
exact False.elim (CharP.char_ne_one R 1 rfl)