feat(data/polynomial/ring_division): add multiplicity of sum of polyn…

…omials is at least minimum of multiplicities (#4442)

I've added the lemma `root_multiplicity_add` inside `data/polynomial/ring_division` that says that the multiplicity of a root in a sum of two polynomials is at least the minimum of the multiplicities.

Co-authored-by: riccardobrasca <32490532+riccardobrasca@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/group_power/basic.lean

@@ -467,6 +467,19 @@ end
 
 end cancel_add_monoid
 
+section comm_semiring
+
+variables [comm_semiring R]
+
+lemma min_pow_dvd_add {n m : ℕ} {a b c : R} (ha : c ^ n ∣ a) (hb : c ^ m ∣ b) : c ^ (min n m) ∣ a + b :=
+begin
+  replace ha := dvd.trans (pow_dvd_pow c (min_le_left n m)) ha,
+  replace hb := dvd.trans (pow_dvd_pow c (min_le_right n m)) hb,
+  exact dvd_add ha hb
+end
+
+end comm_semiring
+
 namespace canonically_ordered_semiring
 variable [canonically_ordered_comm_semiring R]
 

src/data/polynomial/ring_division.lean

@@ -185,6 +185,38 @@ begin
   exact root_multiplicity_eq_zero (mt root_X_sub_C.mp (ne.symm hxy))
 end
 
+/-- The multiplicity of `a` as root of `(X - a) ^ n` is `n`. -/
+lemma root_multiplicity_X_sub_C_pow (a : R) (n : ℕ) : root_multiplicity a ((X - C a) ^ n) = n :=
+begin
+  induction n with n hn,
+  { refine root_multiplicity_eq_zero _,
+    simp only [eval_one, is_root.def, not_false_iff, one_ne_zero, pow_zero] },
+  have hzero :=  (ne_zero_of_monic (monic_pow (monic_X_sub_C a) n.succ)),
+  rw pow_succ (X - C a) n at hzero ⊢,
+  simp only [root_multiplicity_mul hzero, root_multiplicity_X_sub_C_self, hn, nat.one_add]
+end
+
+/-- If `(X - a) ^ n` divides a polynomial `p` then the multiplicity of `a` as root of `p` is at
+least `n`. -/
+lemma root_multiplicity_of_dvd {p : polynomial R} {a : R} {n : ℕ}
+  (hzero : p ≠ 0) (h : (X - C a) ^ n ∣ p) : n ≤ root_multiplicity a p :=
+begin
+  obtain ⟨q, hq⟩ := exists_eq_mul_right_of_dvd h,
+  rw hq at hzero,
+  simp only [hq, root_multiplicity_mul hzero, root_multiplicity_X_sub_C_pow,
+             ge_iff_le, _root_.zero_le, le_add_iff_nonneg_right],
+end
+
+/-- The multiplicity of `p + q` is at least the minimum of the multiplicities. -/
+lemma root_multiplicity_add {p q : polynomial R} (a : R) (hzero : p + q ≠ 0) :
+  min (root_multiplicity a p) (root_multiplicity a q) ≤ root_multiplicity a (p + q) :=
+begin
+  refine root_multiplicity_of_dvd hzero _,
+  have hdivp : (X - C a) ^ root_multiplicity a p ∣ p := pow_root_multiplicity_dvd p a,
+  have hdivq : (X - C a) ^ root_multiplicity a q ∣ q := pow_root_multiplicity_dvd q a,
+  exact min_pow_dvd_add hdivp hdivq
+end
+
 lemma exists_multiset_roots : ∀ {p : polynomial R} (hp : p ≠ 0),
   ∃ s : multiset R, (s.card : with_bot ℕ) ≤ degree p ∧ ∀ a, s.count a = root_multiplicity a p
 | p := λ hp, by haveI := classical.prop_decidable (∃ x, is_root p x); exact