# Zulip Chat Archive

## 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 :=
⟨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 (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