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
Roadmap of the lesson:
- Definitions
- Ring Structure
- Evaluation
- Derivative
- Roots
Definition
- P = a_n X^n + ... + a_2 X^2 + a_1 X + a_0
- 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)
- 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)
Derivative
- definition
- notation
- properties
Roots
- root p x == x is a root of p