[Merged by Bors] - feat(field_theory/ratfunc): The numerator and denominator of a rational function are coprime

src/algebra/euclidean_domain/basic.lean

@@ -84,6 +84,9 @@ begin
   rw [mul_div_cancel_left _ hz, mul_left_comm, mul_div_cancel_left _ hz]
 end
 
+protected lemma mul_div_cancel' {a b : R} (hb : b ≠ 0) (hab : b ∣ a) : b * (a / b) = a :=
+by rw [←mul_div_assoc _ hab, mul_div_cancel_left _ hb]
+
 @[simp, priority 900] -- This generalizes `int.div_one`, see note [simp-normal form]
 lemma div_one (p : R) : p / 1 = p :=
 (euclidean_domain.eq_div_of_mul_eq_left (one_ne_zero' R) (mul_one p)).symm

src/field_theory/ratfunc.lean

@@ -1020,6 +1020,14 @@ x.induction_on (λ p q hq, begin
     exact inv_ne_zero (polynomial.leading_coeff_ne_zero.mpr q_div_ne_zero) },
 end)
 
+lemma is_coprime_num_denom (x : ratfunc K) : is_coprime x.num x.denom :=
+begin
+  induction x using ratfunc.induction_on with p q hq,
+  rw [num_div, denom_div _ hq],
+  exact (is_coprime_mul_unit_left ((leading_coeff_ne_zero.2 $ right_div_gcd_ne_zero
+    hq).is_unit.inv.map C) _ _).2 (is_coprime_div_gcd_div_gcd hq),
+end
+
 @[simp] lemma num_eq_zero_iff {x : ratfunc K} : num x = 0 ↔ x = 0 :=
 ⟨λ h, by rw [← num_div_denom x, h, ring_hom.map_zero, zero_div],
  λ h, h.symm ▸ num_zero⟩

src/ring_theory/euclidean_domain.lean

@@ -29,14 +29,12 @@ open euclidean_domain set ideal
 
 section gcd_monoid
 
-variables {R : Type*} [euclidean_domain R] [gcd_monoid R]
+variables {R : Type*} [euclidean_domain R] [gcd_monoid R] {p q : R}
 
-lemma gcd_ne_zero_of_left (p q : R) (hp : p ≠ 0) :
-  gcd_monoid.gcd p q ≠ 0 :=
+lemma gcd_ne_zero_of_left (hp : p ≠ 0) : gcd_monoid.gcd p q ≠ 0 :=
 λ h, hp $ eq_zero_of_zero_dvd (h ▸ gcd_dvd_left p q)
 
-lemma gcd_ne_zero_of_right (p q : R) (hp : q ≠ 0) :
-  gcd_monoid.gcd p q ≠ 0 :=
+lemma gcd_ne_zero_of_right (hp : q ≠ 0) : gcd_monoid.gcd p q ≠ 0 :=
 λ h, hp $ eq_zero_of_zero_dvd (h ▸ gcd_dvd_right p q)
 
 lemma left_div_gcd_ne_zero {p q : R} (hp : p ≠ 0) :
@@ -57,6 +55,13 @@ begin
   exact r0,
 end
 
+lemma is_coprime_div_gcd_div_gcd (hq : q ≠ 0) :
+  is_coprime (p / gcd_monoid.gcd p q) (q / gcd_monoid.gcd p q) :=
+(gcd_is_unit_iff _ _).1 $ is_unit_gcd_of_eq_mul_gcd
+    (euclidean_domain.mul_div_cancel' (gcd_ne_zero_of_right hq) $ gcd_dvd_left _ _).symm
+    (euclidean_domain.mul_div_cancel' (gcd_ne_zero_of_right hq) $ gcd_dvd_right _ _).symm $
+    gcd_ne_zero_of_right hq
+
 end gcd_monoid
 
 namespace euclidean_domain