case inl
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : ℕ
hp : CharP R p
p_ne_zero : p ≠ 0
h : Nat.Prime p
⊢ Nat.Prime p

case inr
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : ℕ
hp : CharP R p
p_ne_zero : p ≠ 0
h : p = 0
⊢ Nat.Prime p
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : ℕ
hp : CharP R p
p_ne_zero : p ≠ 0
⊢ Nat.Prime p
cases' CharP.char_is_prime_or_zero R p with h h
no goals
case inl
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : ℕ
hp : CharP R p
p_ne_zero : p ≠ 0
h : Nat.Prime p
⊢ Nat.Prime p
exact h
no goals
case inr
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : ℕ
hp : CharP R p
p_ne_zero : p ≠ 0
h : p = 0
⊢ Nat.Prime p
contradiction