An additional lemma about coprime ideals

This lemma generalises exists_sum_eq_one_iff_pairwise_coprime to the case of non-principal ideals. It is on a separate file due to import requirements.

theorem Ideal.iSup_iInf_eq_top_iff_pairwise {ι : Type u_1} {R : Type u_2} [CommSemiring R] {t : Finset ι} (h : t.Nonempty) (I : ι → Ideal R) : ⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j = ⊤ ↔ (↑t).Pairwise fun (i j : ι) => I i ⊔ I j = ⊤

A finite family of ideals is pairwise coprime (that is, any two of them generate the whole ring) iff when taking all the possible intersections of all but one of these ideals, the resulting family of ideals still generate the whole ring.

For example with three ideals : I ⊔ J = I ⊔ K = J ⊔ K = ⊤ ↔ (I ⊓ J) ⊔ (I ⊓ K) ⊔ (J ⊓ K) = ⊤.

When ideals are all of the form I i = R ∙ s i, this is equivalent to the exists_sum_eq_one_iff_pairwise_coprime lemma.