roots p <= roots q -> p | q

Stream: Is there code for X?

[Tomaz Mascarenhas]

We do have docs#Polynomial.roots.le_of_dvd. Do we have the converse? I.e. if the roots of p form a subset of the roots of q then p divides q?

[Kevin Buzzard]

Trick question: can you formalize the statement of what you want to prove?

[Tomaz Mascarenhas]

hm, doesn't

theorem roots.dvd_of_le (h : q ≠ 0) (hp : p ≠ 0) :  roots p ≤ roots q  -> p ∣ q

work? (in my case I don't care about 0s)

[Aaron Liu]

You should add some typeclasses and the types of p and q

[Kevin Buzzard]

Can you make a #mwe?

[Yury G. Kudryashov]

See docs#Polynomial.Splits.dvd_of_roots_le_roots

[Tomaz Mascarenhas]

import Mathlib

universe u

variable {R : Type u}

variable [CommRing R] [IsDomain R] {p q : Polynomial R}

open Polynomial

theorem roots.dvd_of_le (h : q ≠ 0) (hp : p ≠ 0) :  roots p ≤ roots q  -> p ∣ q := sorry

[Tomaz Mascarenhas]

Yury G. Kudryashov said:

See docs#Polynomial.Splits.dvd_of_roots_le_roots

hm, let me see

[Tomaz Mascarenhas]

That works for me! Thanks @Yury G. Kudryashov!

[Yury G. Kudryashov]

Found by @loogle Polynomial.roots, _ ≤ _, _ ∣ _

[loogle]

:search: Polynomial.roots.le_of_dvd, Multiset.prod_X_sub_C_dvd_iff_le_roots, and 2 more

[Kevin Buzzard]

Tomaz Mascarenhas said:

import Mathlib

universe u

variable {R : Type u}

variable [CommRing R] [IsDomain R] {p q : Polynomial R}

open Polynomial

theorem roots.dvd_of_le (h : q ≠ 0) (hp : p ≠ 0) :  roots p ≤ roots q  -> p ∣ q := sorry

This isn't true, e.g. roots (X^2+1) is empty if R is the real numbers (this was why it was a trick question) as is roots (X^2+2) so both inclusions are valid but neither polynomial divides the other.

[Kevin Buzzard]

This is why (hp : Polynomial.Splits (RingHom.id K) p) is essential in Yury's answer (i.e. "all the roots are in the base ring")

[Yury G. Kudryashov]

BTW, should we add versions of Polynomial.Splits lemmas in the Polynomial namespace assuming that the field is algebraically closed?