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