Polynomial divisible by Π(x - μ_i)

Stream: Is there code for X?

[giacomo gallina]

I have a polynomial p, and I want to write it as

$$p = q \cdot r$$

where

$$q(x) = \prod_{μ \in S} (x - μ) \qquad S \subseteq roots(p)$$

Is there already some theorem in mathlib that says this? I searched but didn't find it.
And if this isn't in mathlib, how could I prove it? I found Polynomial.mul_div_eq_iff_isRoot, which is similar to what I want, but I'm not sure of how i could use it

[Kevin Buzzard]

You can just let $S$ be empty and let $q$ be 1.

I think it's better to ask your actual question as a #mwe rather than in informal language.

[giacomo gallina]

Sorry, I didn't explain myself properly, I already have S fixed, and would like to get the decomposition. Basically I would like a theorem with this signature:

theorem my_factorization (p : ℝ[X]) (S : Multiset ℝ) (hs : S ≤ p.roots) : ∃ r : ℝ[X], p = r * Multiset.prod (Multiset.map (fun μ => X - Polynomial.C μ) S)

[giacomo gallina]

It would be enough to be able to do a proof by induction on the cardinality of S, but I don't really know how to do that

[giacomo gallina]

Ok, I found Multiset.induction, I think I can do it

[Jireh Loreaux]

How about docs#Multiset.prod_X_sub_C_dvd_iff_le_roots ?

[Jireh Loreaux]

In fact, just:

[Jireh Loreaux]

@loogle Multiset.prod, Multiset.map, Polynomial.roots, Polynomial.C

[loogle]

:search: Polynomial.roots_multiset_prod_X_sub_C, Polynomial.monic_prod_multiset_X_sub_C, and 10 more

[Jireh Loreaux]

It's the 5th hit here.

[giacomo gallina]

Thank you so much, I need to learn to use loogle better!

[Jireh Loreaux]

Adding one more bit gets the exact hit:

@loogle Multiset.prod, Multiset.map, Polynomial.roots, Polynomial.C, LE.le

[loogle]

:search: Multiset.prod_X_sub_C_dvd_iff_le_roots