feat(data/polynomial/monic): monic.not_zero_divisor_iff (#8417)

We prove that a monic polynomial is not a zero divisor. A helper lemma is proven that the product of a monic polynomial is of lesser degree iff it is nontrivial and the multiplicand is zero.

src/data/polynomial/degree/definitions.lean

@@ -637,7 +637,7 @@ begin
   rwa coeff_mul_degree_add_degree
 end
 
-lemma degree_mul_monic (hq : monic q) : degree (p * q) = degree p + degree q :=
+lemma monic.degree_mul (hq : monic q) : degree (p * q) = degree p + degree q :=
 if hp : p = 0 then by simp [hp]
 else degree_mul' $ by rwa [hq.leading_coeff, mul_one, ne.def, leading_coeff_eq_zero]
 
@@ -811,10 +811,10 @@ theorem not_is_unit_X : ¬ is_unit (X : polynomial R) :=
 λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $
 by { change g * monomial 1 1 = 1 at hgf, rw [← coeff_one_zero, ← hgf], simp }
 
-@[simp] lemma degree_mul_X : degree (p * X) = degree p + 1 := by simp [degree_mul_monic monic_X]
+@[simp] lemma degree_mul_X : degree (p * X) = degree p + 1 := by simp [monic_X.degree_mul]
 
 @[simp] lemma degree_mul_X_pow : degree (p * X ^ n) = degree p + n :=
-by simp [degree_mul_monic (monic_X_pow n)]
+by simp [(monic_X_pow n).degree_mul]
 
 end nontrivial_semiring
 

src/data/polynomial/div.lean

@@ -78,7 +78,7 @@ else
     (by rw [← degree_eq_nat_degree h.2, ← degree_eq_nat_degree hq0];
     exact h.1),
   degree_sub_lt
-  (by rw [degree_mul_monic hq, degree_C_mul_X_pow _ hp, degree_eq_nat_degree h.2,
+  (by rw [hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_nat_degree h.2,
       degree_eq_nat_degree hq0, ← with_bot.coe_add, nat.sub_add_cancel hlt])
   h.2
   (by rw [leading_coeff_mul_monic hq, leading_coeff_mul_X_pow, leading_coeff_C])

src/data/polynomial/monic.lean

@@ -59,6 +59,10 @@ begin
   rwa nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f _)
 end
 
+lemma monic_C_mul_of_mul_leading_coeff_eq_one [nontrivial R] {b : R}
+  (hp : b * p.leading_coeff = 1) : monic (C b * p) :=
+by rw [monic, leading_coeff_mul' _]; simp [leading_coeff_C b, hp]
+
 lemma monic_mul_C_of_leading_coeff_mul_eq_one [nontrivial R] {b : R}
   (hp : p.leading_coeff * b = 1) : monic (p * C b) :=
 by rw [monic, leading_coeff_mul' _]; simp [leading_coeff_C b, hp]
@@ -101,7 +105,7 @@ by rwa [monic, leading_coeff_add_of_degree_lt hpq]
 namespace monic
 
 @[simp]
-lemma degree_eq_zero_iff_eq_one {p : polynomial R} (hp : p.monic) :
+lemma nat_degree_eq_zero_iff_eq_one {p : polynomial R} (hp : p.monic) :
   p.nat_degree = 0 ↔ p = 1 :=
 begin
   split; intro h,
@@ -112,6 +116,11 @@ begin
   rw this, convert C_1, rw ← h, apply hp,
 end
 
+@[simp]
+lemma degree_le_zero_iff_eq_one {p : polynomial R} (hp : p.monic) :
+  p.degree ≤ 0 ↔ p = 1 :=
+by rw [←hp.nat_degree_eq_zero_iff_eq_one, nat_degree_eq_zero_iff_degree_le_zero]
+
 lemma nat_degree_mul {p q : polynomial R} (hp : p.monic) (hq : q.monic) :
   (p * q).nat_degree = p.nat_degree + q.nat_degree :=
 begin
@@ -120,6 +129,32 @@ begin
   simp [hp.leading_coeff, hq.leading_coeff]
 end
 
+lemma degree_mul_comm {p : polynomial R} (hp : p.monic) (q : polynomial R) :
+  (p * q).degree = (q * p).degree :=
+begin
+  by_cases h : q = 0,
+  { simp [h] },
+  rw [degree_mul', hp.degree_mul],
+  { exact add_comm _ _ },
+  { rwa [hp.leading_coeff, one_mul, leading_coeff_ne_zero] }
+end
+
+lemma nat_degree_mul' {p q : polynomial R} (hp : p.monic) (hq : q ≠ 0) :
+  (p * q).nat_degree = p.nat_degree + q.nat_degree :=
+begin
+  rw [nat_degree_mul', add_comm],
+  simpa [hp.leading_coeff, leading_coeff_ne_zero]
+end
+
+lemma nat_degree_mul_comm {p : polynomial R} (hp : p.monic) (q : polynomial R) :
+  (p * q).nat_degree = (q * p).nat_degree :=
+begin
+  by_cases h : q = 0,
+  { simp [h] },
+  rw [hp.nat_degree_mul' h, polynomial.nat_degree_mul', add_comm],
+  simpa [hp.leading_coeff, leading_coeff_ne_zero]
+end
+
 lemma next_coeff_mul {p q : polynomial R} (hp : monic p) (hq : monic q) :
   next_coeff (p * q) = next_coeff p + next_coeff q :=
 begin
@@ -294,5 +329,140 @@ lemma ne_zero_of_monic (h : monic p) : p ≠ 0 :=
 
 end nonzero_semiring
 
+section not_zero_divisor
+
+-- TODO: using gh-8537, rephrase lemmas that involve commutation around `*` using the op-ring
+-- TODO: using gh-8561, rephrase using regular elements
+
+variables [semiring R] {p : polynomial R}
+
+lemma monic.mul_left_ne_zero (hp : monic p) {q : polynomial R} (hq : q ≠ 0) :
+  q * p ≠ 0 :=
+begin
+  by_cases h : p = 1,
+  { simpa [h] },
+  rw [ne.def, ←degree_eq_bot, hp.degree_mul, with_bot.add_eq_bot, not_or_distrib, degree_eq_bot],
+  refine ⟨hq, _⟩,
+  rw [←hp.degree_le_zero_iff_eq_one, not_le] at h,
+  refine (lt_trans _ h).ne',
+  simp
+end
+
+lemma monic.mul_right_ne_zero (hp : monic p) {q : polynomial R} (hq : q ≠ 0) :
+  p * q ≠ 0 :=
+begin
+  by_cases h : p = 1,
+  { simpa [h] },
+  rw [ne.def, ←degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, with_bot.add_eq_bot,
+      not_or_distrib, degree_eq_bot],
+  refine ⟨hq, _⟩,
+  rw [←hp.degree_le_zero_iff_eq_one, not_le] at h,
+  refine (lt_trans _ h).ne',
+  simp
+end
+
+lemma monic.mul_nat_degree_lt_iff (h : monic p) {q : polynomial R} :
+  (p * q).nat_degree < p.nat_degree ↔ p ≠ 1 ∧ q = 0 :=
+begin
+  by_cases hq : q = 0,
+  { suffices : 0 < p.nat_degree ↔ p.nat_degree ≠ 0,
+    { simpa [hq, ←h.nat_degree_eq_zero_iff_eq_one] },
+    exact ⟨λ h, h.ne', λ h, lt_of_le_of_ne (nat.zero_le _) h.symm ⟩ },
+  { simp [h.nat_degree_mul', hq] }
+end
+
+lemma monic.mul_right_eq_zero_iff (h : monic p) {q : polynomial R} :
+  p * q = 0 ↔ q = 0 :=
+begin
+  by_cases hq : q = 0;
+  simp [h.mul_right_ne_zero, hq]
+end
+
+lemma monic.mul_left_eq_zero_iff (h : monic p) {q : polynomial R} :
+  q * p = 0 ↔ q = 0 :=
+begin
+  by_cases hq : q = 0;
+  simp [h.mul_left_ne_zero, hq]
+end
+
+lemma degree_smul_of_non_zero_divisor {S : Type*} [monoid S] [distrib_mul_action S R]
+  (p : polynomial R) (k : S) (h : ∀ (x : R), k • x = 0 → x = 0) :
+  (k • p).degree = p.degree :=
+begin
+  refine le_antisymm _ _,
+  { rw degree_le_iff_coeff_zero,
+    intros m hm,
+    rw degree_lt_iff_coeff_zero at hm,
+    simp [hm m le_rfl] },
+  { rw degree_le_iff_coeff_zero,
+    intros m hm,
+    rw degree_lt_iff_coeff_zero at hm,
+    refine h _ _,
+    simpa using hm m le_rfl },
+end
+
+lemma nat_degree_smul_of_non_zero_divisor {S : Type*} [monoid S] [distrib_mul_action S R]
+  (p : polynomial R) (k : S) (h : ∀ (x : R), k • x = 0 → x = 0) :
+  (k • p).nat_degree = p.nat_degree :=
+begin
+  by_cases hp : p = 0,
+  { simp [hp] },
+  rw [←with_bot.coe_eq_coe, ←degree_eq_nat_degree hp, ←degree_eq_nat_degree,
+      degree_smul_of_non_zero_divisor _ _ h],
+  contrapose! hp,
+  rw polynomial.ext_iff at hp ⊢,
+  simp only [coeff_smul, coeff_zero] at hp,
+  intro n,
+  simp [h _ (hp n)]
+end
+
+lemma leading_coeff_smul_of_non_zero_divisor {S : Type*} [monoid S] [distrib_mul_action S R]
+  (p : polynomial R) (k : S) (h : ∀ (x : R), k • x = 0 → x = 0) :
+  (k • p).leading_coeff = k • p.leading_coeff :=
+by rw [leading_coeff, leading_coeff, coeff_smul, nat_degree_smul_of_non_zero_divisor _ _ h]
+
+lemma monic_of_is_unit_leading_coeff_inv_smul (h : is_unit p.leading_coeff) :
+  monic (h.unit⁻¹ • p) :=
+begin
+  rw [monic.def, leading_coeff_smul_of_non_zero_divisor, units.smul_def],
+  { obtain ⟨k, hk⟩ := h,
+    simp only [←hk, smul_eq_mul, ←units.coe_mul, units.coe_eq_one, inv_mul_eq_iff_eq_mul],
+    simp [units.ext_iff, is_unit.unit_spec] },
+  { simp [smul_eq_zero_iff_eq] }
+end
+
+lemma is_unit_leading_coeff_mul_right_eq_zero_iff (h : is_unit p.leading_coeff) {q : polynomial R} :
+  p * q = 0 ↔ q = 0 :=
+begin
+  split,
+  { intro hp,
+    rw ←smul_eq_zero_iff_eq (h.unit)⁻¹ at hp,
+    { have : (h.unit)⁻¹ • (p * q) = ((h.unit)⁻¹ • p) * q,
+      { ext,
+        simp only [units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum],
+        refine sum_congr rfl (λ x hx, _),
+        rw ←mul_assoc },
+      rwa [this, monic.mul_right_eq_zero_iff] at hp,
+      exact monic_of_is_unit_leading_coeff_inv_smul _ } },
+  { rintro rfl,
+    simp }
+end
+
+lemma is_unit_leading_coeff_mul_left_eq_zero_iff (h : is_unit p.leading_coeff) {q : polynomial R} :
+  q * p = 0 ↔ q = 0 :=
+begin
+  split,
+  { intro hp,
+    replace hp := congr_arg (* C ↑(h.unit)⁻¹) hp,
+    simp only [zero_mul] at hp,
+    rwa [mul_assoc, monic.mul_left_eq_zero_iff] at hp,
+    nontriviality,
+    refine monic_mul_C_of_leading_coeff_mul_eq_one _,
+    simp [units.mul_inv_eq_iff_eq_mul, is_unit.unit_spec] },
+  { rintro rfl,
+    rw zero_mul }
+end
+
+end not_zero_divisor
 
 end polynomial