(edits are also saved when you close the window). Finally you can
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
(notes)
- 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
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
(notes)
Look theorems ans definitions about size, lead_coef in poly.v
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 (+, -, *, *:, ^+)
Definition by extension
- \poly_(i < n) E i
is the polynomial:
- (E 0) + (E 1) *: 'X + ... + E (n - 1) *: 'X^(n-1)
The ring of polynomials
- The type of polynomials has been equipped
with a (commutative / integral) ring structure.
- All related lemmas of ssralg can be used.
Evaluation of polynomials
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
Division
- division and its theory are in the polydiv.v file