feat(data/polynomial): more API for roots (#11081)

`leading_coeff_monic_mul`
`leading_coeff_X_sub_C`
`root_multiplicity_C`
`not_is_root_C`
`roots_smul_nonzero`
`leading_coeff_div_by_monic_X_sub_C`
`roots_eq_zero_iff`

also generalized various statements about `X - C a` to `X + C a` over semirings.



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/data/polynomial/degree/definitions.lean

@@ -388,10 +388,7 @@ lemma next_coeff_of_pos_nat_degree (p : polynomial R) (hp : 0 < p.nat_degree) :
   next_coeff p = p.coeff (p.nat_degree - 1) :=
 by { rw [next_coeff, if_neg], contrapose! hp, simpa }
 
-end semiring
-
-section semiring
-variables [semiring R] {p q : polynomial R} {ι : Type*}
+variables {p q : polynomial R} {ι : Type*}
 
 lemma coeff_nat_degree_eq_zero_of_degree_lt (h : degree p < degree q) :
   coeff p (nat_degree q) = 0 :=
@@ -913,41 +910,92 @@ end ring
 section nonzero_ring
 variables [nontrivial R]
 
-@[simp] lemma degree_X_add_C [semiring R] (a : R) : degree (X + C a) = 1 :=
+section semiring
+variable [semiring R]
+
+@[simp] lemma degree_X_add_C (a : R) : degree (X + C a) = 1 :=
 have degree (C a) < degree (X : polynomial R),
 from calc degree (C a) ≤ 0 : degree_C_le
                    ... < 1 : with_bot.some_lt_some.mpr zero_lt_one
                    ... = degree X : degree_X.symm,
 by rw [degree_add_eq_left_of_degree_lt this, degree_X]
 
+@[simp] lemma nat_degree_X_add_C (x : R) : (X + C x).nat_degree = 1 :=
+nat_degree_eq_of_degree_eq_some $ degree_X_add_C x
+
+@[simp]
+lemma next_coeff_X_add_C [semiring S] (c : S) : next_coeff (X + C c) = c :=
+begin
+  nontriviality S,
+  simp [next_coeff_of_pos_nat_degree]
+end
+
+lemma degree_X_pow_add_C {n : ℕ} (hn : 0 < n) (a : R) :
+  degree ((X : polynomial R) ^ n + C a) = n :=
+have degree (C a) < degree ((X : polynomial R) ^ n),
+  from calc degree (C a) ≤ 0 : degree_C_le
+  ... < degree ((X : polynomial R) ^ n) : by rwa [degree_X_pow];
+    exact with_bot.coe_lt_coe.2 hn,
+by rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]
+
+lemma X_pow_add_C_ne_zero {n : ℕ} (hn : 0 < n) (a : R) :
+  (X : polynomial R) ^ n + C a ≠ 0 :=
+mt degree_eq_bot.2 (show degree ((X : polynomial R) ^ n + C a) ≠ ⊥,
+  by rw degree_X_pow_add_C hn a; exact dec_trivial)
+
+theorem X_add_C_ne_zero (r : R) : X + C r ≠ 0 :=
+pow_one (X : polynomial R) ▸ X_pow_add_C_ne_zero zero_lt_one r
+
+theorem zero_nmem_multiset_map_X_add_C {α : Type*} (m : multiset α) (f : α → R) :
+  (0 : polynomial R) ∉ m.map (λ a, X + C (f a)) :=
+λ mem, let ⟨a, _, ha⟩ := multiset.mem_map.mp mem in X_add_C_ne_zero _ ha
+
+lemma nat_degree_X_pow_add_C {n : ℕ} {r : R} :
+  (X ^ n + C r).nat_degree = n :=
+begin
+  by_cases hn : n = 0,
+  { rw [hn, pow_zero, ←C_1, ←ring_hom.map_add, nat_degree_C] },
+  { exact nat_degree_eq_of_degree_eq_some (degree_X_pow_add_C (pos_iff_ne_zero.mpr hn) r) },
+end
+
+@[simp] lemma leading_coeff_X_pow_add_C {n : ℕ} (hn : 0 < n) {r : R} :
+  (X ^ n + C r).leading_coeff = 1 :=
+by rw [leading_coeff, nat_degree_X_pow_add_C, coeff_add, coeff_X_pow_self,
+  coeff_C, if_neg (pos_iff_ne_zero.mp hn), add_zero]
+
+@[simp] lemma leading_coeff_X_add_C [semiring S] (r : S) :
+  (X + C r).leading_coeff = 1 :=
+begin
+  nontriviality,
+  rw [←pow_one (X : polynomial S), leading_coeff_X_pow_add_C zero_lt_one],
+  apply_instance
+end
+
+@[simp] lemma leading_coeff_X_pow_add_one {n : ℕ} (hn : 0 < n) :
+  (X ^ n + 1 : polynomial R).leading_coeff = 1 :=
+leading_coeff_X_pow_add_C hn
+
+end semiring
+
 variables [ring R]
 
 @[simp] lemma degree_X_sub_C (a : R) : degree (X - C a) = 1 :=
-have degree (C a) < degree (X : polynomial R),
-from calc degree (C a) ≤ 0 : degree_C_le
-                   ... < 1 : with_bot.some_lt_some.mpr zero_lt_one
-                   ... = degree X : degree_X.symm,
-by rw [degree_sub_eq_left_of_degree_lt this, degree_X]
+by rw [sub_eq_add_neg, ←map_neg C a, degree_X_add_C]
 
 @[simp] lemma nat_degree_X_sub_C (x : R) : (X - C x).nat_degree = 1 :=
 nat_degree_eq_of_degree_eq_some $ degree_X_sub_C x
 
 @[simp]
-lemma next_coeff_X_sub_C (c : R) : next_coeff (X - C c) = - c :=
-by simp [next_coeff_of_pos_nat_degree]
+lemma next_coeff_X_sub_C [ring S] (c : S) : next_coeff (X - C c) = - c :=
+by rw [sub_eq_add_neg, ←map_neg C c, next_coeff_X_add_C]
 
 lemma degree_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) :
   degree ((X : polynomial R) ^ n - C a) = n :=
-have degree (C a) < degree ((X : polynomial R) ^ n),
-  from calc degree (C a) ≤ 0 : degree_C_le
-  ... < degree ((X : polynomial R) ^ n) : by rwa [degree_X_pow];
-    exact with_bot.coe_lt_coe.2 hn,
-by rw [degree_sub_eq_left_of_degree_lt this, degree_X_pow]
+by rw [sub_eq_add_neg, ←map_neg C a, degree_X_pow_add_C hn]; apply_instance
 
 lemma X_pow_sub_C_ne_zero {n : ℕ} (hn : 0 < n) (a : R) :
   (X : polynomial R) ^ n - C a ≠ 0 :=
-mt degree_eq_bot.2 (show degree ((X : polynomial R) ^ n - C a) ≠ ⊥,
-  by rw degree_X_pow_sub_C hn a; exact dec_trivial)
+by { rw [sub_eq_add_neg, ←map_neg C a], exact X_pow_add_C_ne_zero hn _ }
 
 theorem X_sub_C_ne_zero (r : R) : X - C r ≠ 0 :=
 pow_one (X : polynomial R) ▸ X_pow_sub_C_ne_zero zero_lt_one r
@@ -958,16 +1006,15 @@ theorem zero_nmem_multiset_map_X_sub_C {α : Type*} (m : multiset α) (f : α 
 
 lemma nat_degree_X_pow_sub_C {n : ℕ} {r : R} :
   (X ^ n - C r).nat_degree = n :=
-begin
-  by_cases hn : n = 0,
-  { rw [hn, pow_zero, ←C_1, ←ring_hom.map_sub, nat_degree_C] },
-  { exact nat_degree_eq_of_degree_eq_some (degree_X_pow_sub_C (pos_iff_ne_zero.mpr hn) r) },
-end
+by rw [sub_eq_add_neg, ←map_neg C r, nat_degree_X_pow_add_C]
 
 @[simp] lemma leading_coeff_X_pow_sub_C {n : ℕ} (hn : 0 < n) {r : R} :
   (X ^ n - C r).leading_coeff = 1 :=
-by rw [leading_coeff, nat_degree_X_pow_sub_C, coeff_sub, coeff_X_pow_self,
-  coeff_C, if_neg (pos_iff_ne_zero.mp hn), sub_zero]
+by rw [sub_eq_add_neg, ←map_neg C r, leading_coeff_X_pow_add_C hn]; apply_instance
+
+@[simp] lemma leading_coeff_X_sub_C [ring S] (r : S) :
+  (X - C r).leading_coeff = 1 :=
+by rw [sub_eq_add_neg, ←map_neg C r, leading_coeff_X_add_C]
 
 @[simp] lemma leading_coeff_X_pow_sub_one {n : ℕ} (hn : 0 < n) :
   (X ^ n - 1 : polynomial R).leading_coeff = 1 :=
@@ -1000,7 +1047,7 @@ begin
       exact mul_ne_zero (mt leading_coeff_eq_zero.1 hp) (mt leading_coeff_eq_zero.1 hq) } }
 end
 
-@[simp] lemma leading_coeff_X_add_C [nontrivial R] (a b : R) (ha : a ≠ 0):
+@[simp] lemma leading_coeff_C_mul_X_add_C [nontrivial R] (a b : R) (ha : a ≠ 0):
   leading_coeff (C a * X + C b) = a :=
 begin
   rw [add_comm, leading_coeff_add_of_degree_lt],

src/data/polynomial/div.lean

@@ -467,6 +467,13 @@ begin
   exact multiplicity.dvd_iff_multiplicity_pos
 end
 
+@[simp] lemma root_multiplicity_C (r a : R) : root_multiplicity a (C r) = 0 :=
+begin
+  rcases eq_or_ne r 0 with rfl|hr,
+  { simp },
+  { exact root_multiplicity_eq_zero (not_is_root_C _ _ hr) }
+end
+
 lemma pow_root_multiplicity_dvd (p : polynomial R) (a : R) :
   (X - C a) ^ root_multiplicity a p ∣ p :=
 if h : p = 0 then by simp [h]

src/data/polynomial/eval.lean

@@ -362,6 +362,9 @@ lemma is_root.dvd {R : Type*} [comm_semiring R] {p q : polynomial R} {x : R}
   (h : p.is_root x) (hpq : p ∣ q) : q.is_root x :=
 by rwa [is_root, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]
 
+lemma not_is_root_C (r a : R) (hr : r ≠ 0) : ¬ is_root (C r) a :=
+by simpa using hr
+
 end eval
 
 section comp

src/data/polynomial/ring_division.lean

@@ -402,12 +402,18 @@ end
 
 @[simp] lemma roots_C (x : R) : (C x).roots = 0 :=
 if H : x = 0 then by rw [H, C_0, roots_zero] else multiset.ext.mpr $ λ r,
-have not_root : ¬ is_root (C x) r := mt (λ (h : eval r (C x) = 0), trans eval_C.symm h) H,
-by rw [count_roots, count_zero, root_multiplicity_eq_zero not_root]
+by rw [count_roots, count_zero, root_multiplicity_eq_zero (not_is_root_C _ _ H)]
 
 @[simp] lemma roots_one : (1 : polynomial R).roots = ∅ :=
 roots_C 1
 
+lemma roots_smul_nonzero (p : polynomial R) {r : R} (hr : r ≠ 0) :
+  (r • p).roots = p.roots :=
+begin
+  by_cases hp : p = 0;
+  simp [smul_eq_C_mul, roots_mul, hr, hp]
+end
+
 lemma roots_list_prod (L : list (polynomial R)) :
   ((0 : polynomial R) ∉ L) → L.prod.roots = (L : multiset (polynomial R)).bind roots :=
 list.rec_on L (λ _, roots_one) $ λ hd tl ih H,
@@ -681,6 +687,16 @@ begin
   exact hrew.symm
 end
 
+lemma leading_coeff_div_by_monic_X_sub_C (p : polynomial R) (hp : degree p ≠ 0) (a : R) :
+  leading_coeff (p /ₘ (X - C a)) = leading_coeff p :=
+begin
+  nontriviality,
+  cases hp.lt_or_lt with hd hd,
+  { rw [degree_eq_bot.mp $ (nat.with_bot.lt_zero_iff _).mp hd, zero_div_by_monic] },
+  refine leading_coeff_div_by_monic_of_monic (monic_X_sub_C a) _,
+  rwa [degree_X_sub_C, nat.with_bot.one_le_iff_zero_lt]
+end
+
 lemma eq_of_monic_of_dvd_of_nat_degree_le (hp : p.monic) (hq : q.monic) (hdiv : p ∣ q)
   (hdeg : q.nat_degree ≤ p.nat_degree) : q = p :=
 begin

src/field_theory/is_alg_closed/basic.lean

@@ -86,6 +86,17 @@ begin
   exact ⟨z, sq z⟩
 end
 
+lemma roots_eq_zero_iff [is_alg_closed k] {p : polynomial k} :
+  p.roots = 0 ↔ p = polynomial.C (p.coeff 0) :=
+begin
+  refine ⟨λ h, _, λ hp, by rw [hp, roots_C]⟩,
+  cases (le_or_lt (degree p) 0) with hd hd,
+  { exact eq_C_of_degree_le_zero hd },
+  { obtain ⟨z, hz⟩ := is_alg_closed.exists_root p hd.ne',
+    rw [←mem_roots (ne_zero_of_degree_gt hd), h] at hz,
+    simpa using hz }
+end
+
 theorem exists_eval₂_eq_zero_of_injective {R : Type*} [ring R] [is_alg_closed k] (f : R →+* k)
   (hf : function.injective f) (p : polynomial R) (hp : p.degree ≠ 0) : ∃ x, p.eval₂ f x = 0 :=
 let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective hf]) in