Library mathcomp.algebra.poly

This file provides a library for univariate polynomials over ring structures; it also provides an extended theory for polynomials whose coefficients range over commutative rings and integral domains. {poly R} == the type of polynomials with coefficients of type R, represented as lists with a non zero last element (big endian representation); the coefficient type R must have a canonical ringType structure cR. In fact {poly R} denotes the concrete type polynomial cR; R is just a phantom argument that lets type inference reconstruct the (hidden) ringType structure cR. p : seq R == the big-endian sequence of coefficients of p, via the coercion polyseq : polynomial >-> seq. Poly s == the polynomial with coefficient sequence s (ignoring trailing zeroes). \poly(i < n) E(i) == the polynomial of degree at most n - 1 whose coefficients are given by the general term E(i) 0, 1, - p, p + q, == the usual ring operations: {poly R} has a canonical p * q, p ^+ n, ... ringType structure, which is commutative / integral when R is commutative / integral, respectively. polyC c, c%:P == the constant polynomial c 'X == the (unique) variable 'X^n == a power of 'X; 'X^0 is 1, 'X^1 is convertible to 'X p`_i == the coefficient of 'X^i in p; this is in fact just the ring_scope notation generic seq-indexing using nth 0%R, combined with the polyseq coercion. coefp i == the linear function p |-> p`_i (self-exapanding). size p == 1 + the degree of p, or 0 if p = 0 (this is the generic seq function combined with polyseq). lead_coef p == the coefficient of the highest monomial in p, or 0 if p = 0 (hence lead_coef p = 0 iff p = 0) p \is monic <=> lead_coef p == 1 (0 is not monic). p \is a polyOver S <=> the coefficients of p satisfy S; S should have a key that should be (at least) an addrPred. p. [x] == the evaluation of a polynomial p at a point x using the Horner scheme

The multi-rule hornerE (resp., hornerE_comm) unwinds

horner evaluation of a polynomial expression (resp., in a non commutative ring, with side conditions). p^` == formal derivative of p p^`(n) == formal n-derivative of p p^`N(n) == formal n-derivative of p divided by n! p \Po q == polynomial composition; because this is naturally a a linear morphism in the first argument, this notation is transposed (q comes before p for redex selection, etc). := \sum(i < size p) p`_i *: q ^+ i comm_poly p x == x and p. [x] commute; this is a sufficient condition for evaluating (q * p). [x] as q. [x] * p. [x] when R is not commutative. comm_coef p x == x commutes with all the coefficients of p (clearly, this implies comm_poly p x). root p x == x is a root of p, i.e., p. [x] = 0 n.-unity_root x == x is an nth root of unity, i.e., a root of 'X^n - 1 n.-primitive_root x == x is a primitive nth root of unity, i.e., n is the least positive integer m > 0 such that x ^+ m = 1.

The submodule poly.UnityRootTheory can be used to

import selectively the part of the theory of roots of unity that doesn't mention polynomials explicitly map_poly f p == the image of the polynomial by the function f (which (locally, p^f) is usually a ring morphism). p^:P == p lifted to {poly {poly R}} (:= map_poly polyC p). commr_rmorph f u == u commutes with the image of f (i.e., with all f x). horner_morph cfu == given cfu : commr_rmorph f u, the function mapping p to the value of map_poly f p at u; this is a ring morphism from {poly R} to the codomain of f when f is a ring morphism. horner_eval u == the function mapping p to p. [u]; this function can only be used for u in a commutative ring, so it is always a linear ring morphism from {poly R} to R. horner_alg a == given a in some R-algebra A, the function evaluating a polynomial p at a; it is always a linear ring morphism from {poly R} to A. diff_roots x y == x and y are distinct roots; if R is a field, this just means x != y, but this concept is generalized to the case where R is only a ring with units (i.e., a unitRingType); in which case it means that x and y commute, and that the difference x - y is a unit (i.e., has a multiplicative inverse) in R. to just x != y). uniq_roots s == s is a sequence or pairwise distinct roots, in the sense of diff_roots p above.

We only show that these operations and properties are transferred by

morphisms whose domain is a field (thus ensuring injectivity). We prove the factor_theorem, and the max_poly_roots inequality relating the number of distinct roots of a polynomial and its size. The some polynomial lemmas use following suffix interpretation : C - constant polynomial (as in polyseqC : a%:P = nseq (a != 0) a). X - the polynomial variable 'X (as in coefX : 'X`_i = (i == 1%N)). Xn - power of 'X (as in monicXn : monic 'X^n).

Defines a polynomial as a sequence with <> 0 last element

We need to break off the section here to let the Bind Scope directives take effect.

Remember the boolean (c != 0) is coerced to 1 if true and 0 if false

Extensional interpretation (poly <=> nat -> R)

Builds a polynomial by extension.

Build a polynomial directly from a list of coefficients.

Build a polynomial from an infinite sequence of coefficients and a bound.

Zmodule structure for polynomial

Properties of the zero polynomial

Size, leading coef, morphism properties of coef

Polynomial ring structure.

Algebra structure of polynomials.

The indeterminate, at last!

Expansion of a polynomial as an indexed sum

Monic predicate

Some facts about regular elements.

Horner evaluation of polynomials