polynomial α is the type of univariate polynomials over α.

Polynomials should be seen as (semi-)rings with the additional constructor X. The embedding from α is called C.

C a is the constant polynomial a.

X is the polynomial variable (aka indeterminant).

coeff p n is the coefficient of X^n in p

degree p is the degree of the polynomial p, i.e. the largest X-exponent in p. degree p = some n when p ≠ 0 and n is the highest power of X that appears in p, otherwise degree 0 = ⊥.

nat_degree p forces degree p to ℕ, by defining nat_degree 0 = 0.

Evaluate a polynomial p given a ring hom f from the scalar ring to the target and a value x for the variable in the target

eval x p is the evaluation of the polynomial p at x

is_root p x implies x is a root of p. The evaluation of p at x is zero

leading_coeff p gives the coefficient of the highest power of X in p

a polynomial is monic if its leading coefficient is 1

map f p maps a polynomial p across a ring hom f

dix_X p return a polynomial q such that q * X + C (p.coeff 0) = p. It can be used in a semiring where the usual division algorithm is not possible

div_by_monic gives the quotient of p by a monic polynomial q.

mod_by_monic gives the remainder of p by a monic polynomial q.

roots p noncomputably gives a finset containing all the roots of p

nth_roots n a noncomputably returns the solutions to x ^ n = a

derivative p formal derivative of the polynomial p