case zero
R : Type u
inst✝ : Semiring R
hp : CharP R 0
q : CharZero R
⊢ 1 = 1

case prime
R : Type u
inst✝ : Semiring R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hq_hchar : CharP R q
⊢ q = 1
R : Type u
inst✝ : Semiring R
q : ℕ
hp : CharP R 0
hq : ExpChar R q
⊢ q = 1
cases' hq with q hq_one hq_prime hq_hchar
no goals
case zero
R : Type u
inst✝ : Semiring R
hp : CharP R 0
q : CharZero R
⊢ 1 = 1
rfl
no goals
case prime
R : Type u
inst✝ : Semiring R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hq_hchar : CharP R q
⊢ q = 1
exact False.elim (lt_irrefl _ ((hp.eq R hq_hchar).symm ▸ hq_prime : (0 : ℕ).Prime).pos)