## Stream: Is there code for X?

### Topic: A polynomial splits if it has enough roots

#### Riccardo Brasca (Oct 02 2020 at 09:31):

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 (Oct 02 2020 at 09:51):

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

#### Anne Baanen (Oct 02 2020 at 10:04):

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 :=
rw [ ring_hom.id_comp i,  splits_map_iff],
exact splits_of_splits_of_dvd _ hzero hsplit hdvd
end

#### Riccardo Brasca (Oct 02 2020 at 10:16):

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

#### Riccardo Brasca (Oct 03 2020 at 14:45):

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 (Oct 03 2020 at 14:53):

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

#### Riccardo Brasca (Oct 03 2020 at 14:57):

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 (Oct 03 2020 at 15:03):

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

#### Johan Commelin (Oct 03 2020 at 15:03):

Then we can try to help filling in the proof

#### Riccardo Brasca (Oct 03 2020 at 15:44):

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 (Oct 04 2020 at 10:41):

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

Last updated: May 16 2021 at 05:21 UTC