case hI
R : Type u
ι✝ : Type ?u.255689
inst✝¹ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ Set.Pairwise (↑Finset.univ) (IsCoprime on fun i => I i)
R : Type u
ι✝ : Type ?u.255689
inst✝¹ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ (⨅ (i : ι), span {I i}) = span {∏ i : ι, I i}
rw [← Finset.inf_univ_eq_iInf, finset_inf_span_singleton]
no goals
case hI
R : Type u
ι✝ : Type ?u.255689
inst✝¹ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ Set.Pairwise (↑Finset.univ) (IsCoprime on fun i => I i)
rwa [Finset.coe_univ, Set.pairwise_univ]