Zulip Chat Archive

Stream: Is there code for X?

Topic: A polynomial splits if it has enough roots


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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 :=
    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

view this post on Zulip 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.

view this post on Zulip 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+QP+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 nn such that (Xα)n(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!

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Oct 03 2020 at 14:57):

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

view this post on Zulip Johan Commelin (Oct 03 2020 at 15:03):

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

view this post on Zulip Johan Commelin (Oct 03 2020 at 15:03):

Then we can try to help filling in the proof

view this post on Zulip 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!

view this post on Zulip 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