Counting roots of a monic polynomial by its factorizations

A monic polynomial p of degree n over a domain has at least k roots, counted with multiplicity, exactly when it factors as ∏ j, (X - x j) * q with q monic of degree n - k. Writing q through its lower coefficients b : Fin (n - k) → R as TauCeti.Polynomial.monicOfCoeff b turns the condition into the solvability of a polynomial system in the finitely many unknowns x and b. This is how the root count is related to the coefficients when one studies its dependence on them, for instance its measurability over a local field (TauCeti.isCompact_setOf_le_card_aroots).

Main results

• Polynomial.Monic.le_card_roots_iff_exists_prod_mul_monicOfCoeff_eq: a monic polynomial of degree n has at least k roots exactly when it is ∏ j, (X - x j) times a monic polynomial of degree n - k.

theorem Polynomial.Monic.le_card_roots_iff_exists_prod_mul_monicOfCoeff_eq {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p.Monic) {n k : ℕ} (hdeg : p.natDegree = n) : k ≤ p.roots.card ↔ ∃ (x : Fin k → R) (b : Fin (n - k) → R), (∏ j : Fin k, (X - C (x j))) * TauCeti.Polynomial.monicOfCoeff b = p

A monic polynomial p of degree n over a domain has at least k roots, counted with multiplicity, exactly when p = ∏ j, (X - x j) * monicOfCoeff b for some x : Fin k → R and b : Fin (n - k) → R, that is, with a monic cofactor of degree n - k.