Commit 2022-04-11 16:38 797c7133

View on Github →

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.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.pairwise_cons'

added theorem finset.pairwise_cons

added theorem finset.pairwise_subtype_iff_pairwise_finset'

added theorem finset.pairwise_subtype_iff_pairwise_finset

Modified src/ring_theory/coprime/lemmas.lean

added theorem exists_sum_eq_one_iff_pairwise_coprime'

added theorem exists_sum_eq_one_iff_pairwise_coprime

added theorem pairwise_coprime_iff_coprime_prod