R : Type u
ι : Type ?u.281942
inst✝ : CommSemiring R
I J K L : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ (∏ _x in Finset.range n, I) ⊔ J = ⊤
R : Type u
ι : Type ?u.281942
inst✝ : CommSemiring R
I J K L : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ I ^ n ⊔ J = ⊤
rw [← Finset.card_range n, ← Finset.prod_const]
no goals
R : Type u
ι : Type ?u.281942
inst✝ : CommSemiring R
I J K L : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ (∏ _x in Finset.range n, I) ⊔ J = ⊤
exact prod_sup_eq_top fun _ _ => h