[GOAL]
R : Type u
inst✝ : Semiring R
q : ℕ
hp : CharP R 0
hq : ExpChar R q
⊢ q = 1
[PROOFSTEP]
cases' hq with q hq_one hq_prime hq_hchar
[GOAL]
case zero
R : Type u
inst✝ : Semiring R
hp : CharP R 0
q : CharZero R
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
exact False.elim (lt_irrefl _ ((hp.eq R hq_hchar).symm ▸ hq_prime : (0 : ℕ).Prime).pos)
[GOAL]
R : Type u
inst✝ : Semiring R
p q : ℕ
hp : CharP R p
hq : ExpChar R q
⊢ p = q ↔ Nat.Prime p
[PROOFSTEP]
cases' hq with q hq_one hq_prime hq_hchar
[GOAL]
case zero
R : Type u
inst✝ : Semiring R
p : ℕ
hp : CharP R p
q : CharZero R
⊢ p = 1 ↔ Nat.Prime p
[PROOFSTEP]
rw [(CharP.eq R hp inferInstance : p = 0)]
[GOAL]
case zero
R : Type u
inst✝ : Semiring R
p : ℕ
hp : CharP R p
q : CharZero R
⊢ 0 = 1 ↔ Nat.Prime 0
[PROOFSTEP]
decide
[GOAL]
case prime
R : Type u
inst✝ : Semiring R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hq_hchar : CharP R q
⊢ p = q ↔ Nat.Prime p
[PROOFSTEP]
exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp hq_hchar⟩
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hq : ExpChar R 1
⊢ p = 0
[PROOFSTEP]
cases hq
[GOAL]
case zero
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 0
[PROOFSTEP]
exact CharP.eq R hp inferInstance
[GOAL]
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
[PROOFSTEP]
exact False.elim (CharP.char_ne_one R 1 rfl)
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hq : ExpChar R 1
⊢ CharZero R
[PROOFSTEP]
cases hq
[GOAL]
case zero
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : CharZero R
⊢ CharZero R
[PROOFSTEP]
assumption
[GOAL]
case prime
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R
[PROOFSTEP]
exact False.elim (CharP.char_ne_one R 1 rfl)
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 ↔ p = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 → p = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
p : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R 1
⊢ p = 0
[PROOFSTEP]
exact char_zero_of_expChar_one R p
[GOAL]
case mpr
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
q : ℕ
inst✝¹ : ExpChar R q
inst✝ : CharP R 0
⊢ q = 1
[PROOFSTEP]
exact expChar_one_of_char_zero R q
[GOAL]
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
[PROOFSTEP]
cases' CharP.char_is_prime_or_zero R p with h h
[GOAL]
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
[PROOFSTEP]
exact h
[GOAL]
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
[PROOFSTEP]
contradiction
[GOAL]
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hq : ExpChar R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
cases hq
[GOAL]
case zero
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
⊢ Nat.Prime 1 ∨ 1 = 1
case prime
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hprime✝ : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
case zero => exact .inr rfl
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
⊢ Nat.Prime 1 ∨ 1 = 1
[PROOFSTEP]
case zero => exact .inr rfl
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
⊢ Nat.Prime 1 ∨ 1 = 1
[PROOFSTEP]
exact .inr rfl
[GOAL]
case prime
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hprime✝ : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
case prime hp _ => exact .inl hp
[GOAL]
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hp : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
case prime hp _ => exact .inl hp
[GOAL]
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
q : ℕ
hp : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1
[PROOFSTEP]
exact .inl hp
