# 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)
:

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.