no goals
R : Type u
ι : Type ?u.339982
inst✝ : CommSemiring R
I J K L : Ideal R
n : ℕ
H : n > 0
⊢ ¬Nat.zero > 0
decide
R : Type u
ι : Type ?u.339982
inst✝ : CommSemiring R
I J K L : Ideal R
n✝ : ℕ
H✝¹ : n✝ > 0
n : ℕ
ih : n > 0 → radical (I ^ n) = radical I
H✝ : Nat.succ n > 0
H : 0 < n
⊢ radical (I * I ^ n) = radical I ⊓ radical (I ^ n)
R : Type u
ι : Type ?u.339982
inst✝ : CommSemiring R
I J K L : Ideal R
n✝ : ℕ
H✝¹ : n✝ > 0
n : ℕ
ih : n > 0 → radical (I ^ n) = radical I
H✝ : Nat.succ n > 0
H : 0 < n
⊢ radical (I ^ (n + 1)) = radical I ⊓ radical (I ^ n)
rw [pow_succ]
no goals
R : Type u
ι : Type ?u.339982
inst✝ : CommSemiring R
I J K L : Ideal R
n✝ : ℕ
H✝¹ : n✝ > 0
n : ℕ
ih : n > 0 → radical (I ^ n) = radical I
H✝ : Nat.succ n > 0
H : 0 < n
⊢ radical (I * I ^ n) = radical I ⊓ radical (I ^ n)
exact radical_mul _ _
no goals
R : Type u
ι : Type ?u.339982
inst✝ : CommSemiring R
I J K L : Ideal R
n✝ : ℕ
H✝¹ : n✝ > 0
n : ℕ
ih : n > 0 → radical (I ^ n) = radical I
H✝ : Nat.succ n > 0
H : 0 < n
⊢ radical I ⊓ radical (I ^ n) = radical I ⊓ radical I
rw [ih H]