Splitting from the degrees of irreducible factors, and evaluating split polynomials

A polynomial over a field splits as soon as each of its irreducible factors has degree at most one. This is the converse of Mathlib's Polynomial.Splits.natDegree_le_one_of_irreducible, read through divisibility; it is the form in which splitting is detected when only the irreducible factors of a polynomial are under control, as in Kummer's theorem on the places above a place of a function field.

Main results

• Polynomial.Splits.of_forall_irreducible_dvd_natDegree_le_one: a polynomial whose irreducible factors all have degree at most one splits.
• Polynomial.Splits.eval₂_eq_prod_roots: evaluated along any ring homomorphism, a split polynomial is its leading coefficient times the product of the linear factors over its roots.
• Polynomial.Splits.eq_prod_roots_of_coeff_zero_eq_one: a split polynomial with constant coefficient 1 is the product of the factors 1 - α⁻¹ X over its roots α.

theorem Polynomial.Splits.of_forall_irreducible_dvd_natDegree_le_one {K : Type u_1} [Field K] {f : Polynomial K} (h : ∀ (g : Polynomial K), Irreducible g → g ∣ f → g.natDegree ≤ 1) : f.Splits

A polynomial whose irreducible factors are linear splits.

theorem Polynomial.Splits.eval₂_eq_prod_roots {R : Type u_2} {S : Type u_3} [CommRing R] [IsDomain R] [CommRing S] {f : Polynomial R} (hf : f.Splits) (φ : R →+* S) (x : S) : eval₂ φ x f = φ f.leadingCoeff * (Multiset.map (fun (a : R) => x - φ a) f.roots).prod

Evaluating a split polynomial along a ring homomorphism: the value at x is the image of the leading coefficient times the product of x - φ a over the roots a. This is Polynomial.Splits.eval_eq_prod_roots with the evaluation taking place in another ring.

theorem Polynomial.Splits.eq_prod_roots_of_coeff_zero_eq_one {K : Type u_1} [Field K] {f : Polynomial K} (hf : f.Splits) (h0 : f.coeff 0 = 1) : f = (Multiset.map (fun (α : K) => 1 - C α⁻¹ * X) f.roots).prod

A split polynomial with constant coefficient 1 is the product of the factors 1 - α⁻¹ X over its roots α, counted with multiplicity. This is the normalisation of Polynomial.Splits.eq_prod_roots at 0 rather than at the leading coefficient.