The Polynomials Library :

poly.v

• A library for univariate polynomials over ring structures
• with extensions for polynomials whose coefficients range over
• commutative rings
• integral domains

The Polynomials

• Definitions
• Ring Structure
• Evaluation
• Derivative
• Roots

Definition

• P = a_n X^n + ... + a_2 X^2 + a_1 X + a_0
• list of coefficients (decreasing/increasing degrees)
• list of pairs (degree, coef)

Math Components library choice:

• P = a_0 + a_1 X + a_2 X^2 + ... + a_n X^n
• A normalized (i.e. no trailing 0) sequence of coefficients

First properties

Polynomials are coercible to sequences:

• one can directly take the k_th element of a polynomial
• P'_k i.e. retrieve the coefficient of X^k in P.

• size of a polynomial
• the degree of a polynomial is its size minus 1

Notations

• {poly R}: polynomials over R (a Ring)
• Poly s : the polynomial built from sequence s
• 'X : monomial
• 'X^n : monomial to the power of n
• a:%P : constant polynomial
• standard notations of ssralg (+, -, *, *:, ^+)

A polynomial can be defined by extension:

• poly(i < n) E i is the polynomial:
• (E 0) + (E 1) *: 'X + ... + E (n - 1) *: 'X^(n-1)

Ring Structure

• The type of polynomials has been equipped with a (commutative / integral) ring structure.

• All related lemmas of ssralg can be used.

Evaluation

• (Right-)evaluation of polynomials
• Warning: type of x

Properties of coefficients

• Lifting a ring predicate to polynomials.

polyOver's lemmas:

• predicate associate to S: at least an addrPred
• polyOver0
• polyOverC
• polyOverX
• rpred* (from ssralg)

• definition
• notation
• properties

Roots

• root p x == x is a root of p

polydiv.v