case zero
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n : ℕ
H✝ : r ^ n ∈ I
H : r ^ Nat.zero ∈ I
⊢ r ∈ I

case succ
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n✝ : ℕ
H✝ : r ^ n✝ ∈ I
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ Nat.succ n ∈ I
⊢ r ∈ I
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n : ℕ
H : r ^ n ∈ I
⊢ r ∈ I
induction' n with n ih
case zero
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n : ℕ
H✝ : r ^ n ∈ I
H : 1 ∈ I
⊢ r ∈ I
case zero
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n : ℕ
H✝ : r ^ n ∈ I
H : r ^ Nat.zero ∈ I
⊢ r ∈ I
rw [pow_zero] at H
no goals
case zero
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n : ℕ
H✝ : r ^ n ∈ I
H : 1 ∈ I
⊢ r ∈ I
exact (mt (eq_top_iff_one _).2 hI.1).elim H
case succ
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n✝ : ℕ
H✝ : r ^ n✝ ∈ I
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r * r ^ n ∈ I
⊢ r ∈ I
case succ
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n✝ : ℕ
H✝ : r ^ n✝ ∈ I
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ Nat.succ n ∈ I
⊢ r ∈ I
rw [pow_succ] at H
no goals
case succ
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n✝ : ℕ
H✝ : r ^ n✝ ∈ I
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r * r ^ n ∈ I
⊢ r ∈ I
exact Or.casesOn (hI.mem_or_mem H) id ih