A polynomial splits if it has enough roots

Stream: Is there code for X?

[Riccardo Brasca]

Hi all, do we have a lemma that says that if a polynomial has as many roots as his degree (in a field extension) than it splits (in the extension)? The definition of polynomial.splits that I am using is in field_theory.splitting_field, where I do not see this result. Thank you!

[Anne Baanen]

I think we only have the converse, that the number of roots of a polynomial that splits is equal to the degree.

[Anne Baanen]

This might be a nice starting point (in field_theory.splitting_field):

lemma splits_of_card_roots {p : polynomial α} {i : α →+* β}
  (hroots : p.nat_degree = (p.map i).roots.card) : splits i p :=
begin
  have hzero : ((p.map i).roots.map (λ a, X - C a)).prod ≠ 0 := sorry,
  have hsplit : splits (ring_hom.id _) ((p.map i).roots.map (λ a, X - C a)).prod := sorry,
  have hdvd : p.map i ∣ ((p.map i).roots.map (λ a, X - C a)).prod :=
    ⟨C (leading_coeff (p.map i))⁻¹, sorry⟩,
  rw [← ring_hom.id_comp i, ← splits_map_iff],
  exact splits_of_splits_of_dvd _ hzero hsplit hdvd
end

[Riccardo Brasca]

@Anne Baanen Thank you! I will try to prove it, it seems to me we already have all the relevant ingredients.

[Riccardo Brasca]

When trying to prove this I realize that there is no lemma that says that the multiplicity of $\alpha$ in $P+Q$ is at least the minimum of the multiplicities. This should be easy (and I think it should be added to mathlib), since the multiplicity is defined as the largest $n$ such that $(X-\alpha)^n$ divides the polynomial, but I do no understand the way the definition of polynomial.root_multiplicity is written, so I am not able to prove it. Can someone help me? Thank you!

[Reid Barton]

If you need to look at the definition to prove this, then there is already a missing lemma.

[Riccardo Brasca]

Yes, I agree. I think that what is missing is that if $(X-\alpha)^n$ divides $P$ then the multiplicity is at least $n$. Of course mathematically there is nothing to prove, but to write this in Lean I am stuck.

[Johan Commelin]

@Riccardo Brasca Can you write the lean statement that you think is missing?

[Johan Commelin]

Then we can try to help filling in the proof

[Riccardo Brasca]

Yes, sure. Here it is

import data.polynomial.div

variables (R : Type*) [comm_ring R]

namespace polynomial

lemma multiplicity_ge_ of_dvd (p : polynomial R) (a : R) (n : ℕ) :
(X - C a)^n ∣ p → root_multiplicity a p ≥ n :=
begin
sorry
end

lemma root_multiplicity_add (p q : polynomial R) (a : R) :
root_multiplicity a (p + q) ≥
min (root_multiplicity a p) (root_multiplicity a q)
begin
sorry
end

end polynomial

Now I do not have time to write the proof down, but I can prove the second one (that is the one is more interesting in my opinion) from the first one, that mathematically is true by definition. Thank you very much!

[Riccardo Brasca]

There was a := missing in what I wrote yesterday, I am sorry. Now it is correct.