Library 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 coeficient 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.      
               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.         
             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)           
            monic p == p is monic, i.e., lead_coef p = 1 (0 is not monic)   
             p.[x]  == the evaluation of a polynomial p at a point x using  
                       the Horner scheme                                    
The multi-rule horner_lin (resp. horner_lin_com)

                       unwinds horner evaluation of a polynomial expression 
                       (resp. in a non commutative ring, under appropriate  
                       assumptions).                                        
             p^`()  == formal derivative of p                               
             p^`(n) == formal n-derivative of p                             
            p^`N(n) == formal n-derivative of p divided by n!               
       com_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.                                  
       com_coef p x == x commutes with all the coefficients of p (clearly,  
                       this implies com_poly p x).                          
           root p x == x is a root of p, i.e., p.[x] = 0                    
       map_poly f p == the image of the polynomial by the function f (which 
                       should be a ring morphism).                          
     comm_ringM f u == u commutes with the image of f (i.e., with all f x)  
   horner_morph f u == the function mapping p to the value of map_poly f p  
                       at u; this is a morphism from {poly R} to the image  
                       ring of f when f is a morphism and comm_ringM f u.   
  We define pseudo division on polynomials over an integral domain :        
             m %/ d == the pseudo-quotient                                  
             m %% d == the pseudo remainder                                 
          scalp m d == the scaling coefficient of the pseudo-division       
             p %| q <=> q is a pseudo-divisor of p                          
             p %= q <=> p and q are equal up to a non-zero scalar factor    
                    := (p %| q) && (q %| p)                                 
If R is a field, this means p and q are associate.

           gcdp p q == pseudo-gcd of p and q. This is defined for p and q   
                       with coefficients in an arbitrary ring; however gcdp 
                       is only known to be idempotent and  associative when 
                       R has an integral domain (idomainType) structure.    
     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.                 

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

We need to break off the section here to let the argument 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. 

Builds a polynomial from a bare list of coefficients 

Builds a polynomial from an infinite seq of coef and a bound 

Zmodule structure for polynomial 

Properties of the zero polynomial 

Size, leading coef, morphism properties of coef 

And now the Ring structure. 

Indeterminate, at last! 

Expansion of a polynomial as an indexed sum 

Monic predicate 

Pseudo division, defined on an arbitrary ring 

Equality up to a constant factor; this is only used when R is integral 

Pseudo gcd 

Horner evaluation of polynomials 

Container morphism. 

Alternative definition; the one above is more convenient because it lets 
 us use the lemmas on \poly, e.g., size (map_poly p) <= size p is an      
 instance of size_poly.                                                   

Morphisms from the polynomial ring, and the initiality of polynomials  
 with respect to these.                                                 

Pseudo-division in a commutative setting 

idomain structure on poly 

Equality modulo constant factors 

Now we can state that gcd is commutative modulo a factor 

A normalising version of derivation to get the division by n! in Taylor 

Here is the division by n!