mathlibdocumentation

ring_theory.coprime.ideal

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