feat(ring_theory/coprime/lemmas): alternative characterisations of pa…

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

src/data/finset/basic.lean

@@ -2532,6 +2532,36 @@ lemma choose_mem (hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l := (choose
 lemma choose_property (hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp) := (choose_spec _ _ _).2
 
 end choose
+
+section pairwise
+variables {s : finset α}
+
+lemma pairwise_subtype_iff_pairwise_finset' (r : β → β → Prop) (f : α → β) :
+  pairwise (r on λ x : s, f x) ↔ (s : set α).pairwise (r on f) :=
+begin
+  refine ⟨λ h x hx y hy hxy, h ⟨x, hx⟩ ⟨y, hy⟩ (by simpa only [subtype.mk_eq_mk, ne.def]), _⟩,
+  rintros h ⟨x, hx⟩ ⟨y, hy⟩ hxy,
+  exact h hx hy (subtype.mk_eq_mk.not.mp hxy)
+end
+
+lemma pairwise_subtype_iff_pairwise_finset (r : α → α → Prop) :
+  pairwise (r on λ x : s, x) ↔ (s : set α).pairwise r :=
+pairwise_subtype_iff_pairwise_finset' r id
+
+lemma pairwise_cons' {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) :
+  pairwise (r on λ a : s.cons a ha, f a) ↔
+  pairwise (r on λ a : s, f a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a) :=
+begin
+  simp only [pairwise_subtype_iff_pairwise_finset', finset.coe_cons, set.pairwise_insert,
+             finset.mem_coe, and.congr_right_iff],
+  exact λ hsr, ⟨λ h b hb, h b hb $ by { rintro rfl, contradiction }, λ h b hb _, h b hb⟩,
+end
+
+lemma pairwise_cons {a : α} (ha : a ∉ s) (r : α → α → Prop) :
+  pairwise (r on λ a : s.cons a ha, a) ↔ pairwise (r on λ a : s, a) ∧ ∀ b ∈ s, r a b ∧ r b a :=
+pairwise_cons' ha r id
+
+end pairwise
 end finset
 
 namespace equiv

src/ring_theory/coprime/lemmas.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Ken Lee, Chris Hughes
 -/
-import algebra.big_operators.basic
+import algebra.big_operators.ring
 import data.fintype.basic
 import data.int.gcd
 import ring_theory.coprime.basic
@@ -71,6 +71,73 @@ theorem fintype.prod_dvd_of_coprime [fintype I] (Hs : pairwise (is_coprime on s)
   (Hs1 : ∀ i, s i ∣ z) : ∏ x, s x ∣ z :=
 finset.prod_dvd_of_coprime (Hs.set_pairwise _) (λ i _, Hs1 i)
 
+open finset
+
+lemma exists_sum_eq_one_iff_pairwise_coprime (h : t.nonempty) :
+  (∃ μ : I → R, ∑ i in t, μ i * ∏ j in t \ {i}, s j = 1) ↔ pairwise (is_coprime on λ i : t, s i) :=
+begin
+  refine h.cons_induction _ _; clear' t h,
+  { simp only [pairwise, sum_singleton, finset.sdiff_self, prod_empty, mul_one,
+      exists_apply_eq_apply, ne.def, true_iff],
+    rintro a ⟨i, hi⟩ ⟨j, hj⟩ h,
+    rw finset.mem_singleton at hi hj,
+    simpa [hi, hj] using h },
+  intros a t hat h ih,
+  rw pairwise_cons',
+  have mem : ∀ x ∈ t, a ∈ insert a t \ {x} := λ x hx, by
+    { rw [mem_sdiff, mem_singleton], exact ⟨mem_insert_self _ _, λ ha, hat (ha.symm.cases_on hx)⟩ },
+  split,
+  { rintro ⟨μ, hμ⟩,
+    rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ,
+    refine ⟨ih.mp ⟨pi.single h.some (μ a * s h.some) + μ * λ _, s a, _⟩, λ b hb, _⟩,
+    { rw [prod_eq_mul_prod_diff_singleton h.some_spec, ← mul_assoc,
+        ← @if_pos _ _ h.some_spec R (_ * _) 0, ← sum_pi_single', ← sum_add_distrib] at hμ,
+      rw [← hμ, sum_congr rfl], intros x hx, convert add_mul _ _ _ using 2,
+      { by_cases hx : x = h.some,
+        { rw [hx, pi.single_eq_same, pi.single_eq_same] },
+        { rw [pi.single_eq_of_ne hx, pi.single_eq_of_ne hx, zero_mul] } },
+      { convert (mul_assoc _ _ _).symm,
+        convert prod_eq_mul_prod_diff_singleton (mem x hx) _ using 3,
+        convert sdiff_sdiff_comm, rw [sdiff_singleton_eq_erase, erase_insert hat] } },
+    { have : is_coprime (s b) (s a) :=
+        ⟨μ a * ∏ i in t \ {b}, s i, ∑ i in t, μ i * ∏ j in t \ {i}, s j, _⟩,
+      { exact ⟨this.symm, this⟩ },
+      rw [mul_assoc, ← prod_eq_prod_diff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl],
+      intros x hx, convert mul_assoc _ _ _,
+      convert prod_eq_prod_diff_singleton_mul (mem x hx) _ using 3,
+      convert sdiff_sdiff_comm, rw [sdiff_singleton_eq_erase, erase_insert hat] } },
+  { rintro ⟨hs, Hb⟩, obtain ⟨μ, hμ⟩ := ih.mpr hs,
+    obtain ⟨u, v, huv⟩ := is_coprime.prod_left (λ b hb, (Hb b hb).right),
+    use λ i, if i = a then u else v * μ i,
+    have hμ' : ∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a) = v * s a := by
+      rw [← mul_sum, ← sum_mul, hμ, one_mul],
+    rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat, if_pos rfl,
+      ← huv, ← hμ', sum_congr rfl], intros x hx,
+    rw [mul_assoc, if_neg (λ ha : x = a, hat (ha.cases_on hx))],
+    convert mul_assoc _ _ _, convert (prod_eq_prod_diff_singleton_mul (mem x hx) _).symm using 3,
+    convert sdiff_sdiff_comm, rw [sdiff_singleton_eq_erase, erase_insert hat] }
+end
+
+lemma exists_sum_eq_one_iff_pairwise_coprime' [fintype I] [nonempty I] :
+  (∃ μ : I → R, ∑ (i : I), μ i * ∏ j in {i}ᶜ, s j = 1) ↔ pairwise (is_coprime on s) :=
+begin
+  convert exists_sum_eq_one_iff_pairwise_coprime finset.univ_nonempty using 1,
+  simp only [function.on_fun, pairwise_subtype_iff_pairwise_finset', coe_univ, set.pairwise_univ],
+  assumption
+end
+
+lemma pairwise_coprime_iff_coprime_prod :
+  pairwise (is_coprime on λ i : t, s i) ↔ ∀ i ∈ t, is_coprime (s i) (∏ j in t \ {i}, (s j)) :=
+begin
+  refine ⟨λ hp i hi, is_coprime.prod_right_iff.mpr (λ j hj, _), λ hp, _⟩,
+  { rw [finset.mem_sdiff, finset.mem_singleton] at hj,
+    obtain ⟨hj, ji⟩ := hj,
+    exact hp ⟨i, hi⟩ ⟨j, hj⟩ (λ h, ji (congr_arg coe h).symm) },
+  { rintro ⟨i, hi⟩ ⟨j, hj⟩ h,
+    apply is_coprime.prod_right_iff.mp (hp i hi),
+    exact finset.mem_sdiff.mpr ⟨hj, λ f, h $ subtype.ext (finset.mem_singleton.mp f).symm⟩ }
+end
+
 variables {m n : ℕ}
 
 theorem is_coprime.pow_left (H : is_coprime x y) : is_coprime (x ^ m) y :=