Polynomial that splits is product of linear factors

Stream: Is there code for X?

[Violeta Hernández]

I'm looking for something like this:

import Mathlib.Algebra.Polynomial.Splits

open Polynomial

theorem Polynomial.Splits.eq_prod {F : Type*} [Field F] {p : F[X]} (hp : p.Splits (.id _)) :
    ∃ f : Fin p.natDegree → F, p = C p.leadingCoeff * ∏ i, (X + C (f i)) :=
  sorry

[Violeta Hernández]

There might be a better way to write down the assumptions or the result, I don't know

[Violeta Hernández]

Immediately found docs#Polynomial.eq_prod_roots_of_splits right after this, whoops