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.
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