R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharZero (R ⧸ I)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
intro I hI_ne_top
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
h_charP : CharP (R ⧸ I) 0
⊢ CharZero (R ⧸ I)

case h_charP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharP (R ⧸ I) 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharZero (R ⧸ I)
suffices h_charP : CharP (R ⧸ I) 0
no goals
case h_charP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharP (R ⧸ I) 0
cases CharP.exists (R ⧸ I) with
| intro p hp =>
  cases p with
  | zero => exact hp
  | succ p =>
    have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
    exact absurd h_mixed (h p.succ p.succ_pos)
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
h_charP : CharP (R ⧸ I) 0
⊢ CharZero (R ⧸ I)
apply CharP.charP_to_charZero
no goals
case h_charP.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) p
⊢ CharP (R ⧸ I) 0
cases p with
| zero => exact hp
| succ p =>
  have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
  exact absurd h_mixed (h p.succ p.succ_pos)
no goals
case h_charP.intro.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hp : CharP (R ⧸ I) Nat.zero
⊢ CharP (R ⧸ I) 0
exact hp
case h_charP.intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (Nat.succ p)
h_mixed : MixedCharZero R (Nat.succ p)
⊢ CharP (R ⧸ I) 0
case h_charP.intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (Nat.succ p)
⊢ CharP (R ⧸ I) 0
have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
no goals
case h_charP.intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (Nat.succ p)
h_mixed : MixedCharZero R (Nat.succ p)
⊢ CharP (R ⧸ I) 0
exact absurd h_mixed (h p.succ p.succ_pos)