feat(ring_theory/ideals): prod_dvd_of_coprime (#2815)

Co-authored-by: kckennylau <kc_kennylau@yahoo.com.hk>

src/data/polynomial.lean

@@ -2371,6 +2371,14 @@ prime_of_associated normalize_associated this
 lemma irreducible_of_degree_eq_one (hp1 : degree p = 1) : irreducible p :=
 irreducible_of_prime (prime_of_degree_eq_one hp1)
 
+theorem pairwise_coprime_X_sub {α : Type u} [field α] {I : Type v}
+  {s : I → α} (H : function.injective s) :
+  pairwise (is_coprime on (λ i : I, polynomial.X - polynomial.C (s i))) :=
+λ i j hij, have h : s j - s i ≠ 0, from sub_ne_zero_of_ne $ function.injective.ne H hij.symm,
+⟨polynomial.C (s j - s i)⁻¹, -polynomial.C (s j - s i)⁻¹,
+by rw [neg_mul_eq_neg_mul_symm, ← sub_eq_add_neg, ← mul_sub, sub_sub_sub_cancel_left,
+    ← polynomial.C_sub, ← polynomial.C_mul, inv_mul_cancel h, polynomial.C_1]⟩
+
 end field
 
 section derivative
@@ -2482,7 +2490,7 @@ then `f / (X - a)` is coprime with `X - a`.
 Note that we do not assume `f a = 0`, because `f / (X - a) = (f - f a) / (X - a)`. -/
 lemma is_coprime_of_is_root_of_eval_derivative_ne_zero {K : Type*} [field K]
   (f : polynomial K) (a : K) (hf' : f.derivative.eval a ≠ 0) :
-  ideal.is_coprime (X - C a : polynomial K) (f /ₘ (X - C a)) :=
+  is_coprime (X - C a : polynomial K) (f /ₘ (X - C a)) :=
 begin
   refine or.resolve_left (dvd_or_coprime (X - C a) (f /ₘ (X - C a))
     (irreducible_of_degree_eq_one (polynomial.degree_X_sub_C a))) _,

src/ring_theory/coprime.lean

@@ -0,0 +1,164 @@
+/-
+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
+import data.fintype.basic
+import data.int.gcd
+import data.set.disjointed
+
+/-!
+# Coprime elements of a ring
+
+## Main definitions
+
+* `is_coprime x y`: that `x` and `y` are coprime, defined to be the existence of `a` and `b` such
+that `a * x + b * y = 1`. Note that elements with no common divisors are not necessarily coprime,
+e.g., the multivariate polynomials `x₁` and `x₂` are not coprime.
+
+-/
+
+open_locale classical big_operators
+
+universes u v
+
+variables {R : Type u} [comm_semiring R] (x y z : R)
+
+/-- The proposition that `x` and `y` are coprime, defined to be the existence of `a` and `b` such
+that `a * x + b * y = 1`. Note that elements with no common divisors are not necessarily coprime,
+e.g., the multivariate polynomials `x₁` and `x₂` are not coprime. -/
+@[simp] def is_coprime : Prop :=
+∃ a b, a * x + b * y = 1
+
+theorem nat.is_coprime_iff_coprime {m n : ℕ} : is_coprime (m : ℤ) n ↔ nat.coprime m n :=
+⟨λ ⟨a, b, H⟩, nat.eq_one_of_dvd_one $ int.coe_nat_dvd.1 $ by { rw [int.coe_nat_one, ← H],
+  exact dvd_add (dvd_mul_of_dvd_right (int.coe_nat_dvd.2 $ nat.gcd_dvd_left m n) _)
+    (dvd_mul_of_dvd_right (int.coe_nat_dvd.2 $ nat.gcd_dvd_right m n) _) },
+λ H, ⟨nat.gcd_a m n, nat.gcd_b m n, by rw [mul_comm _ (m : ℤ), mul_comm _ (n : ℤ),
+    ← nat.gcd_eq_gcd_ab, show _ = _, from H, int.coe_nat_one]⟩⟩
+
+variables {x y z}
+
+theorem is_coprime.symm (H : is_coprime x y) : is_coprime y x :=
+let ⟨a, b, H⟩ := H in ⟨b, a, by rw [add_comm, H]⟩
+
+theorem is_coprime_comm : is_coprime x y ↔ is_coprime y x :=
+⟨is_coprime.symm, is_coprime.symm⟩
+
+theorem is_coprime_self : is_coprime x x ↔ is_unit x :=
+⟨λ ⟨a, b, h⟩, is_unit_of_mul_eq_one x (a + b) $ by rwa [mul_comm, add_mul],
+λ h, let ⟨b, hb⟩ := is_unit_iff_exists_inv'.1 h in ⟨b, 0, by rwa [zero_mul, add_zero]⟩⟩
+
+theorem is_coprime_zero_left : is_coprime 0 x ↔ is_unit x :=
+⟨λ ⟨a, b, H⟩, is_unit_of_mul_eq_one x b $ by rwa [mul_zero, zero_add, mul_comm] at H,
+λ H, let ⟨b, hb⟩ := is_unit_iff_exists_inv'.1 H in ⟨1, b, by rwa [one_mul, zero_add]⟩⟩
+
+theorem is_coprime_zero_right : is_coprime x 0 ↔ is_unit x :=
+is_coprime_comm.trans is_coprime_zero_left
+
+theorem is_coprime_one_left : is_coprime 1 x :=
+⟨1, 0, by rw [one_mul, zero_mul, add_zero]⟩
+
+theorem is_coprime_one_right : is_coprime x 1 :=
+⟨0, 1, by rw [one_mul, zero_mul, zero_add]⟩
+
+theorem is_coprime.dvd_of_dvd_mul_right (H1 : is_coprime x z) (H2 : x ∣ y * z) : x ∣ y :=
+let ⟨a, b, H⟩ := H1 in by { rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm],
+exact dvd_add (dvd_mul_left _ _) (dvd_mul_of_dvd_right H2 _) }
+
+theorem is_coprime.dvd_of_dvd_mul_left (H1 : is_coprime x y) (H2 : x ∣ y * z) : x ∣ z :=
+let ⟨a, b, H⟩ := H1 in by { rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b],
+exact dvd_add (dvd_mul_left _ _) (dvd_mul_of_dvd_right H2 _) }
+
+theorem is_coprime.mul_left (H1 : is_coprime x z) (H2 : is_coprime y z) : is_coprime (x * y) z :=
+let ⟨a, b, h1⟩ := H1, ⟨c, d, h2⟩ := H2 in
+⟨a * c, a * x * d + b * c * y + b * d * z,
+calc  a * c * (x * y) + (a * x * d + b * c * y + b * d * z) * z
+    = (a * x + b * z) * (c * y + d * z) : by ring
+... = 1 : by rw [h1, h2, mul_one]⟩
+
+theorem is_coprime.mul_right (H1 : is_coprime x y) (H2 : is_coprime x z) : is_coprime x (y * z) :=
+by { rw is_coprime_comm at H1 H2 ⊢, exact H1.mul_left H2 }
+
+variables {I : Type v} {s : I → R} {t : finset I}
+
+theorem is_coprime.prod_left : (∀ i ∈ t, is_coprime (s i) x) → is_coprime (∏ i in t, s i) x :=
+finset.induction_on t (λ _, is_coprime_one_left) $ λ b t hbt ih H,
+by { rw finset.prod_insert hbt, rw finset.forall_mem_insert at H, exact H.1.mul_left (ih H.2) }
+
+theorem is_coprime.prod_right : (∀ i ∈ t, is_coprime x (s i)) → is_coprime x (∏ i in t, s i) :=
+by simpa only [is_coprime_comm] using is_coprime.prod_left
+
+theorem is_coprime.mul_dvd (H : is_coprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z :=
+begin
+  obtain ⟨a, b, h⟩ := H,
+  rw [← mul_one z, ← h, mul_add],
+  apply dvd_add,
+  { rw [mul_comm z, mul_assoc],
+    exact dvd_mul_of_dvd_right (mul_dvd_mul_left _ H2) _ },
+  { rw [mul_comm b, ← mul_assoc],
+    exact dvd_mul_of_dvd_left (mul_dvd_mul_right H1 _) _ }
+end
+
+theorem finset.prod_dvd_of_coprime (Hs : pairwise (is_coprime on s)) (Hs1 : ∀ i, s i ∣ z) :
+  ∏ x in t, s x ∣ z :=
+finset.induction_on t (one_dvd z) (λ a r har ih, by { rw finset.prod_insert har,
+exact (is_coprime.prod_right $ λ i hir, Hs a i $ λ hai, har $ hai.symm ▸ hir).mul_dvd (Hs1 a) ih })
+
+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 Hs1
+
+theorem is_coprime.of_mul_left_left (H : is_coprime (x * y) z) : is_coprime x z :=
+let ⟨a, b, h⟩ := H in ⟨a * y, b, by rwa [mul_right_comm, mul_assoc]⟩
+
+theorem is_coprime.of_mul_left_right (H : is_coprime (x * y) z) : is_coprime y z :=
+by { rw mul_comm at H, exact H.of_mul_left_left }
+
+theorem is_coprime.of_mul_right_left (H : is_coprime x (y * z)) : is_coprime x y :=
+by { rw is_coprime_comm at H ⊢, exact H.of_mul_left_left }
+
+theorem is_coprime.of_mul_right_right (H : is_coprime x (y * z)) : is_coprime x z :=
+by { rw mul_comm at H, exact H.of_mul_right_left }
+
+theorem is_coprime.mul_left_iff : is_coprime (x * y) z ↔ is_coprime x z ∧ is_coprime y z :=
+⟨λ H, ⟨H.of_mul_left_left, H.of_mul_left_right⟩, λ ⟨H1, H2⟩, H1.mul_left H2⟩
+
+theorem is_coprime.mul_right_iff : is_coprime x (y * z) ↔ is_coprime x y ∧ is_coprime x z :=
+by rw [is_coprime_comm, is_coprime.mul_left_iff, is_coprime_comm, @is_coprime_comm _ _ z]
+
+theorem is_coprime.prod_left_iff : is_coprime (∏ i in t, s i) x ↔ ∀ i ∈ t, is_coprime (s i) x :=
+finset.induction_on t (iff_of_true is_coprime_one_left $ λ _, false.elim) $ λ b t hbt ih,
+by rw [finset.prod_insert hbt, is_coprime.mul_left_iff, ih, finset.forall_mem_insert]
+
+theorem is_coprime.prod_right_iff : is_coprime x (∏ i in t, s i) ↔ ∀ i ∈ t, is_coprime x (s i) :=
+by simpa only [is_coprime_comm] using is_coprime.prod_left_iff
+
+theorem is_coprime.of_prod_left (H1 : is_coprime (∏ i in t, s i) x) (i : I) (hit : i ∈ t) :
+  is_coprime (s i) x :=
+is_coprime.prod_left_iff.1 H1 i hit
+
+theorem is_coprime.of_prod_right (H1 : is_coprime x (∏ i in t, s i)) (i : I) (hit : i ∈ t) :
+  is_coprime x (s i) :=
+is_coprime.prod_right_iff.1 H1 i hit
+
+variables {m n : ℕ}
+
+theorem is_coprime.pow_left (H : is_coprime x y) : is_coprime (x ^ m) y :=
+by { rw [← finset.card_range m, ← finset.prod_const], exact is_coprime.prod_left (λ _ _, H) }
+
+theorem is_coprime.pow_right (H : is_coprime x y) : is_coprime x (y ^ n) :=
+by { rw [← finset.card_range n, ← finset.prod_const], exact is_coprime.prod_right (λ _ _, H) }
+
+theorem is_coprime.pow (H : is_coprime x y) : is_coprime (x ^ m) (y ^ n) :=
+H.pow_left.pow_right
+
+theorem is_coprime.is_unit_of_dvd (H : is_coprime x y) (d : x ∣ y) : is_unit x :=
+let ⟨k, hk⟩ := d in is_coprime_self.1 $ is_coprime.of_mul_right_left $
+show is_coprime x (x * k), from hk ▸ H
+
+theorem is_coprime.map (H : is_coprime x y) {S : Type v} [comm_semiring S] (f : R →+* S) :
+  is_coprime (f x) (f y) :=
+let ⟨a, b, h⟩ := H in ⟨f a, f b, by rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]⟩

src/ring_theory/euclidean_domain.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Chris Hughes
 -/
+import ring_theory.coprime
 import ring_theory.ideals
 noncomputable theory
 open_locale classical
@@ -26,7 +27,10 @@ end
 
 theorem gcd_is_unit_iff {α} [euclidean_domain α] {x y : α} :
   is_unit (gcd x y) ↔ is_coprime x y :=
-by rw [← span_singleton_eq_top, span_gcd, is_coprime]
+⟨λ h, let ⟨b, hb⟩ := is_unit_iff_exists_inv'.1 h in ⟨b * gcd_a x y, b * gcd_b x y,
+  by rw [← hb, gcd_eq_gcd_ab, mul_comm x, mul_comm y, mul_add, mul_assoc, mul_assoc]⟩,
+λ ⟨a, b, h⟩, is_unit_iff_dvd_one.2 $ h ▸ dvd_add (dvd_mul_of_dvd_right (gcd_dvd_left x y) _)
+  (dvd_mul_of_dvd_right (gcd_dvd_right x y) _)⟩
 
 theorem is_coprime_of_dvd {α} [euclidean_domain α] {x y : α}
   (z : ¬ (x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬ z ∣ y) :

src/ring_theory/ideals.lean

@@ -149,21 +149,10 @@ begin
     exact SC JS ((eq_top_iff_one _).2 J0) }
 end
 
-def is_coprime (x y : α) : Prop :=
-span ({x, y} : set α) = ⊤
-
 theorem mem_span_pair {x y z : α} :
   z ∈ span ({x, y} : set α) ↔ ∃ a b, a * x + b * y = z :=
 by simp [mem_span_insert, mem_span_singleton', @eq_comm _ _ z]
 
-theorem is_coprime_def {x y : α} :
-  is_coprime x y ↔ ∀ z, ∃ a b, a * x + b * y = z :=
-by simp [is_coprime, submodule.eq_top_iff', mem_span_pair]
-
-theorem is_coprime_self {x : α} :
-  is_coprime x x ↔ is_unit x :=
-by rw [← span_singleton_eq_top]; simp [is_coprime]
-
 lemma span_singleton_lt_span_singleton [integral_domain β] {x y : β} :
   span ({x} : set β) < span ({y} : set β) ↔ y ≠ 0 ∧ ∃ d : β, ¬ is_unit d ∧ x = y * d :=
 by rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton,