mathlib

797c7133 - feat(ring_theory/coprime/lemmas): alternative characterisations of pairwise coprimeness (#12911)

feat(ring_theory/coprime/lemmas): alternative characterisations of pairwise coprimeness (#12911) This provides two condtions equivalent to pairwise coprimeness : * each term is coprime to the product of all others * 1 can be obtained as a linear combination of all products with one term missing.