Numbering the roots of a polynomial #
This file relates an explicit numbering of a polynomial's root set to its multiset of roots.
Main results #
Polynomial.Separable.roots_map_eq_map_numbering: for a separable polynomial, a numbering of its root set enumerates its full root multiset after base change.
The numbering lemma lets root-product formulas be expressed as finite products indexed by
Fin f.natDegree, without choosing a global order on the root set.
theorem
Polynomial.Separable.roots_map_eq_map_numbering
{F : Type u_1}
[CommRing F]
{E : Type u_2}
[CommRing E]
[IsDomain E]
[Algebra F E]
{f : Polynomial F}
(hsep : f.Separable)
(e : Fin f.natDegree ≃ ↑(f.rootSet E))
:
(Polynomial.map (algebraMap F E) f).roots = Multiset.map (fun (i : Fin f.natDegree) => ↑(e i)) Finset.univ.val
A numbering of the root set of a separable polynomial enumerates the whole root multiset: separability makes the roots simple, so the multiset is the image of the numbering.