+ +

Library mathcomp.algebra.poly

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+

+ +

+ 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. + 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. + 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). +

+
+ +
+Set Implicit Arguments.
+ +
+Import GRing.Theory.
+Local Open Scope ring_scope.
+ +
+Reserved Notation "{ 'poly' T }" (at level 0, format "{ 'poly' T }").
+Reserved Notation "c %:P" (at level 2, format "c %:P").
+Reserved Notation "p ^:P" (at level 2, format "p ^:P").
+Reserved Notation "'X" (at level 0).
+Reserved Notation "''X^' n" (at level 3, n at level 2, format "''X^' n").
+Reserved Notation "\poly_ ( i < n ) E"
+  (at level 36, E at level 36, i, n at level 50,
+   format "\poly_ ( i < n ) E").
+Reserved Notation "p \Po q" (at level 50).
+Reserved Notation "p ^`N ( n )" (at level 8, format "p ^`N ( n )").
+Reserved Notation "n .-unity_root" (at level 2, format "n .-unity_root").
+Reserved Notation "n .-primitive_root"
+  (at level 2, format "n .-primitive_root").
+ +
+ +
+Section Polynomial.
+ +
+Variable R : ringType.
+ +
+
+ +
+ Defines a polynomial as a sequence with <> 0 last element +
+
+Record polynomial := Polynomial {polyseq :> seq R; _ : last 1 polyseq != 0}.
+ +
+Canonical polynomial_subType := Eval hnf in [subType for polyseq ].
+Definition polynomial_eqMixin := Eval hnf in [eqMixin of polynomial by <:].
+Canonical polynomial_eqType := Eval hnf in EqType polynomial polynomial_eqMixin.
+Definition polynomial_choiceMixin := [choiceMixin of polynomial by <:].
+Canonical polynomial_choiceType :=
+  Eval hnf in ChoiceType polynomial polynomial_choiceMixin.
+ +
+Lemma poly_inj : injective polyseq.
+ +
+Definition poly_of of phant R := polynomial.
+Identity Coercion type_poly_of : poly_of >-> polynomial.
+ +
+Definition coefp_head h i (p : poly_of (Phant R)) := let: tt := h in p `_i.
+ +
+End Polynomial.
+ +
+
+ +
+ We need to break off the section here to let the argument scope + directives take effect. +
+
+Notation "{ 'poly' T }" := (poly_of (Phant T)).
+Notation coefp i := (coefp_head tt i).
+ +
+Section PolynomialTheory.
+ +
+Variable R : ringType.
+Implicit Types (a b c x y z : R) (p q r d : {poly R }).
+ +
+Canonical poly_subType := Eval hnf in [subType of {poly R }].
+Canonical poly_eqType := Eval hnf in [eqType of {poly R }].
+Canonical poly_choiceType := Eval hnf in [choiceType of {poly R }].
+ +
+Definition lead_coef p := p `_(size p ).-1.
+Lemma lead_coefE p : lead_coef p = p `_(size p ).-1.
+ +
+Definition poly_nil := @Polynomial R [::] (oner_neq0 R).
+Definition polyC c : {poly R } := insubd poly_nil [:: c ].
+ +
+ +
+
+ +
+ Remember the boolean (c != 0) is coerced to 1 if true and 0 if false +
+
+Lemma polyseqC c : c %:P = nseq (c != 0) c :> seq R.
+ +
+Lemma size_polyC c : size c %:P = (c != 0).
+ +
+Lemma coefC c i : c %:P `_i = if i == 0%N then c else 0.
+ +
+Lemma polyCK : cancel polyC (coefp 0).
+ +
+Lemma polyC_inj : injective polyC.
+ +
+Lemma lead_coefC c : lead_coef c %:P = c.
+ +
+
+ +
+ Extensional interpretation (poly <=> nat -> R) +
+
+Lemma polyP p q : nth 0 p =1 nth 0 q ↔ p = q.
+ +
+Lemma size1_polyC p : size p ≤ 1 → p = (p `_0 )%:P.
+ +
+
+ +
+ Builds a polynomial by extension. +
+
+Definition cons_poly c p : {poly R } :=
+  if p is Polynomial ((_ :: _) as s) ns then
+    @Polynomial R (c :: s) ns
+  else c %:P.
+ +
+Lemma polyseq_cons c p :
+  cons_poly c p = (if ~~ nilp p then c :: p else c %:P ) :> seq R.
+ +
+Lemma size_cons_poly c p :
+  size (cons_poly c p) = (if nilp p && (c == 0) then 0%N else (size p ).+1 ).
+ +
+Lemma coef_cons c p i : (cons_poly c p )`_i = if i == 0%N then c else p `_i .-1.
+ +
+
+ +
+ Build a polynomial directly from a list of coefficients. +
+
+Definition Poly := foldr cons_poly 0%:P.
+ +
+Lemma PolyK c s : last c s != 0 → Poly s = s :> seq R.
+ +
+Lemma polyseqK p : Poly p = p.
+ +
+Lemma size_Poly s : size (Poly s) ≤ size s.
+ +
+Lemma coef_Poly s i : (Poly s )`_i = s `_i.
+ +
+
+ +
+ Build a polynomial from an infinite sequence of coefficients and a bound. +
+
+Definition poly_expanded_def n E := Poly (mkseq E n).
+Fact poly_key : unit.
+Definition poly := locked_with poly_key poly_expanded_def.
+Canonical poly_unlockable := [unlockable fun poly ].
+ +
+Lemma polyseq_poly n E :
+  E n .-1 != 0 → \poly_(i < n ) E i = mkseq [eta E ] n :> seq R.
+ +
+Lemma size_poly n E : size (\poly_(i < n ) E i) ≤ n.
+ +
+Lemma size_poly_eq n E : E n .-1 != 0 → size (\poly_(i < n ) E i) = n.
+ +
+Lemma coef_poly n E k : (\poly_(i < n ) E i )`_k = (if k < n then E k else 0).
+ +
+Lemma lead_coef_poly n E :
+  n > 0 → E n .-1 != 0 → lead_coef (\poly_(i < n ) E i) = E n .-1.
+ +
+Lemma coefK p : \poly_(i < size p ) p `_i = p.
+ +
+
+ +
+ Zmodule structure for polynomial +
+
+Definition add_poly_def p q := \poly_(i < maxn (size p) (size q)) (p `_i + q `_i ).
+Fact add_poly_key : unit.
+Definition add_poly := locked_with add_poly_key add_poly_def.
+Canonical add_poly_unlockable := [unlockable fun add_poly ].
+ +
+Definition opp_poly_def p := \poly_(i < size p ) - p `_i.
+Fact opp_poly_key : unit.
+Definition opp_poly := locked_with opp_poly_key opp_poly_def.
+Canonical opp_poly_unlockable := [unlockable fun opp_poly ].
+ +
+Fact coef_add_poly p q i : (add_poly p q )`_i = p `_i + q `_i.
+ +
+Fact coef_opp_poly p i : (opp_poly p )`_i = - p `_i.
+ +
+Fact add_polyA : associative add_poly.
+ +
+Fact add_polyC : commutative add_poly.
+ +
+Fact add_poly0 : left_id 0%:P add_poly.
+ +
+Fact add_polyN : left_inverse 0%:P opp_poly add_poly.
+ +
+Definition poly_zmodMixin :=
+  ZmodMixin add_polyA add_polyC add_poly0 add_polyN.
+ +
+Canonical poly_zmodType := Eval hnf in ZmodType {poly R } poly_zmodMixin.
+Canonical polynomial_zmodType :=
+  Eval hnf in ZmodType (polynomial R) poly_zmodMixin.
+ +
+
+ +
+ Properties of the zero polynomial +
+
+Lemma polyC0 : 0%:P = 0 :> {poly R }.
+ +
+Lemma polyseq0 : (0 : {poly R }) = [::] :> seq R.
+ +
+Lemma size_poly0 : size (0 : {poly R }) = 0%N.
+ +
+Lemma coef0 i : (0 : {poly R })`_i = 0.
+ +
+Lemma lead_coef0 : lead_coef 0 = 0 :> R.
+ +
+Lemma size_poly_eq0 p : (size p == 0%N) = (p == 0).
+ +
+Lemma size_poly_leq0 p : (size p ≤ 0) = (p == 0).
+ +
+Lemma size_poly_leq0P p : reflect (p = 0) (size p ≤ 0%N).
+ +
+Lemma size_poly_gt0 p : (0 < size p ) = (p != 0).
+ +
+Lemma nil_poly p : nilp p = (p == 0).
+ +
+Lemma poly0Vpos p : {p = 0} + {size p > 0}.
+ +
+Lemma polySpred p : p != 0 → size p = (size p ).-1 .+1.
+ +
+Lemma lead_coef_eq0 p : (lead_coef p == 0) = (p == 0).
+ +
+Lemma polyC_eq0 (c : R) : (c %:P == 0) = (c == 0).
+ +
+Lemma size_poly1P p : reflect (exists2 c, c != 0 & p = c %:P) (size p == 1%N).
+ +
+Lemma leq_sizeP p i : reflect (∀ j, i ≤ j → p `_j = 0) (size p ≤ i).
+ +
+
+ +
+ Size, leading coef, morphism properties of coef +
+
+ +
+Lemma coefD p q i : (p + q )`_i = p `_i + q `_i.
+ +
+Lemma coefN p i : (- p )`_i = - p `_i.
+ +
+Lemma coefB p q i : (p - q )`_i = p `_i - q `_i.
+ +
+Canonical coefp_additive i :=
+  Additive ((fun p ⇒ (coefB p )^~ i ) : additive (coefp i)).
+ +
+Lemma coefMn p n i : (p *+ n )`_i = p `_i *+ n.
+ +
+Lemma coefMNn p n i : (p *- n )`_i = p `_i *- n.
+ +
+Lemma coef_sum I (r : seq I) (P : pred I) (F : I → {poly R }) k :
+  (\sum_(i <- r | P i ) F i )`_k = \sum_(i <- r | P i ) (F i )`_k.
+ +
+Lemma polyC_add : {morph polyC : a b / a + b }.
+ +
+Lemma polyC_opp : {morph polyC : c / - c }.
+ +
+Lemma polyC_sub : {morph polyC : a b / a - b }.
+ +
+Canonical polyC_additive := Additive polyC_sub.
+ +
+Lemma polyC_muln n : {morph polyC : c / c *+ n }.
+ +
+Lemma size_opp p : size (- p) = size p.
+ +
+Lemma lead_coef_opp p : lead_coef (- p) = - lead_coef p.
+ +
+Lemma size_add p q : size (p + q) ≤ maxn (size p) (size q).
+ +
+Lemma size_addl p q : size p > size q → size (p + q) = size p.
+ +
+Lemma size_sum I (r : seq I) (P : pred I) (F : I → {poly R }) :
+  size (\sum_(i <- r | P i ) F i) ≤ \max_(i <- r | P i ) size (F i).
+ +
+Lemma lead_coefDl p q : size p > size q → lead_coef (p + q) = lead_coef p.
+ +
+
+ +
+ Polynomial ring structure. +
+
+ +
+Definition mul_poly_def p q :=
+  \poly_(i < (size p + size q ).-1 ) (\sum_(j < i .+1 ) p `_j × q `_(i - j )).
+Fact mul_poly_key : unit.
+Definition mul_poly := locked_with mul_poly_key mul_poly_def.
+Canonical mul_poly_unlockable := [unlockable fun mul_poly ].
+ +
+Fact coef_mul_poly p q i :
+  (mul_poly p q )`_i = \sum_(j < i .+1 ) p `_j × q `_(i - j)%N.
+ +
+Fact coef_mul_poly_rev p q i :
+  (mul_poly p q )`_i = \sum_(j < i .+1 ) p `_(i - j)%N × q `_j.
+ +
+Fact mul_polyA : associative mul_poly.
+ +
+Fact mul_1poly : left_id 1%:P mul_poly.
+ +
+Fact mul_poly1 : right_id 1%:P mul_poly.
+ +
+Fact mul_polyDl : left_distributive mul_poly +%R.
+ +
+Fact mul_polyDr : right_distributive mul_poly +%R.
+ +
+Fact poly1_neq0 : 1%:P != 0 :> {poly R }.
+ +
+Definition poly_ringMixin :=
+  RingMixin mul_polyA mul_1poly mul_poly1 mul_polyDl mul_polyDr poly1_neq0.
+ +
+Canonical poly_ringType := Eval hnf in RingType {poly R } poly_ringMixin.
+Canonical polynomial_ringType :=
+  Eval hnf in RingType (polynomial R) poly_ringMixin.
+ +
+Lemma polyC1 : 1%:P = 1 :> {poly R }.
+ +
+Lemma polyseq1 : (1 : {poly R }) = [:: 1] :> seq R.
+ +
+Lemma size_poly1 : size (1 : {poly R }) = 1%N.
+ +
+Lemma coef1 i : (1 : {poly R })`_i = (i == 0%N)%:R.
+ +
+Lemma lead_coef1 : lead_coef 1 = 1 :> R.
+ +
+Lemma coefM p q i : (p × q )`_i = \sum_(j < i .+1 ) p `_j × q `_(i - j)%N.
+ +
+Lemma coefMr p q i : (p × q )`_i = \sum_(j < i .+1 ) p `_(i - j)%N × q `_j.
+ +
+Lemma size_mul_leq p q : size (p × q) ≤ (size p + size q ).-1.
+ +
+Lemma mul_lead_coef p q :
+  lead_coef p × lead_coef q = (p × q )`_(size p + size q ).-2.
+ +
+Lemma size_proper_mul p q :
+  lead_coef p × lead_coef q != 0 → size (p × q) = (size p + size q ).-1.
+ +
+Lemma lead_coef_proper_mul p q :
+  let c := lead_coef p × lead_coef q in c != 0 → lead_coef (p × q) = c.
+ +
+Lemma size_prod_leq (I : finType) (P : pred I) (F : I → {poly R }) :
+  size (\prod_(i | P i ) F i) ≤ (\sum_(i | P i ) size (F i)).+1 - #|P |.
+ +
+Lemma coefCM c p i : (c %:P × p )`_i = c × p `_i.
+ +
+Lemma coefMC c p i : (p × c %:P )`_i = p `_i × c.
+ +
+Lemma polyC_mul : {morph polyC : a b / a × b }.
+ +
+Fact polyC_multiplicative : multiplicative polyC.
+ Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative.
+ +
+Lemma polyC_exp n : {morph polyC : c / c ^+ n }.
+ +
+Lemma size_exp_leq p n : size (p ^+ n) ≤ ((size p ).-1 × n ).+1.
+ +
+Lemma size_Msign p n : size ((-1) ^+ n × p) = size p.
+ +
+Fact coefp0_multiplicative : multiplicative (coefp 0 : {poly R } → R).
+ +
+Canonical coefp0_rmorphism := AddRMorphism coefp0_multiplicative.
+ +
+
+ +
+ Algebra structure of polynomials. +
+
+Definition scale_poly_def a (p : {poly R }) := \poly_(i < size p ) (a × p `_i ).
+Fact scale_poly_key : unit.
+Definition scale_poly := locked_with scale_poly_key scale_poly_def.
+Canonical scale_poly_unlockable := [unlockable fun scale_poly ].
+ +
+Fact scale_polyE a p : scale_poly a p = a %:P × p.
+ +
+Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a × b) p.
+ +
+Fact scale_1poly : left_id 1 scale_poly.
+ +
+Fact scale_polyDr a : {morph scale_poly a : p q / p + q }.
+ +
+Fact scale_polyDl p : {morph scale_poly ^~ p : a b / a + b }.
+ +
+Fact scale_polyAl a p q : scale_poly a (p × q) = scale_poly a p × q.
+ +
+Definition poly_lmodMixin :=
+  LmodMixin scale_polyA scale_1poly scale_polyDr scale_polyDl.
+ +
+Canonical poly_lmodType :=
+  Eval hnf in LmodType R {poly R } poly_lmodMixin.
+Canonical polynomial_lmodType :=
+  Eval hnf in LmodType R (polynomial R) poly_lmodMixin.
+Canonical poly_lalgType :=
+  Eval hnf in LalgType R {poly R } scale_polyAl.
+Canonical polynomial_lalgType :=
+  Eval hnf in LalgType R (polynomial R) scale_polyAl.
+ +
+Lemma mul_polyC a p : a %:P × p = a *: p.
+ +
+Lemma alg_polyC a : a %:A = a %:P :> {poly R }.
+ +
+Lemma coefZ a p i : (a *: p )`_i = a × p `_i.
+ +
+Lemma size_scale_leq a p : size (a *: p) ≤ size p.
+ +
+Canonical coefp_linear i : {scalar {poly R }} :=
+  AddLinear ((fun a ⇒ (coefZ a ) ^~ i ) : scalable_for *%R (coefp i)).
+Canonical coefp0_lrmorphism := [lrmorphism of coefp 0].
+ +
+
+ +
+ The indeterminate, at last! +
+
+Definition polyX_def := Poly [:: 0; 1].
+Fact polyX_key : unit.
+Definition polyX : {poly R } := locked_with polyX_key polyX_def.
+Canonical polyX_unlockable := [unlockable of polyX ].
+ +
+Lemma polyseqX : 'X = [:: 0; 1] :> seq R.
+ +
+Lemma size_polyX : size 'X = 2.
+ +
+Lemma polyX_eq0 : ('X == 0) = false.
+ +
+Lemma coefX i : 'X `_i = (i == 1%N)%:R.
+ +
+Lemma lead_coefX : lead_coef 'X = 1.
+ +
+Lemma commr_polyX p : GRing.comm p 'X.
+ +
+Lemma coefMX p i : (p × 'X )`_i = (if (i == 0)%N then 0 else p `_i .-1 ).
+ +
+Lemma coefXM p i : ('X × p )`_i = (if (i == 0)%N then 0 else p `_i .-1 ).
+ +
+Lemma cons_poly_def p a : cons_poly a p = p × 'X + a %:P.
+ +
+Lemma poly_ind (K : {poly R } → Type) :
+  K 0 → (∀ p c, K p → K (p × 'X + c %:P)) → (∀ p, K p ).
+ +
+Lemma polyseqXsubC a : 'X - a %:P = [:: - a ; 1] :> seq R.
+ +
+Lemma size_XsubC a : size ('X - a %:P) = 2%N.
+ +
+Lemma size_XaddC b : size ('X + b %:P) = 2.
+ +
+Lemma lead_coefXsubC a : lead_coef ('X - a %:P) = 1.
+ +
+Lemma polyXsubC_eq0 a : ('X - a %:P == 0) = false.
+ +
+Lemma size_MXaddC p c :
+  size (p × 'X + c %:P) = (if (p == 0) && (c == 0) then 0%N else (size p ).+1 ).
+ +
+Lemma polyseqMX p : p != 0 → p × 'X = 0 :: p :> seq R.
+ +
+Lemma size_mulX p : p != 0 → size (p × 'X) = (size p ).+1.
+ +
+Lemma lead_coefMX p : lead_coef (p × 'X) = lead_coef p.
+ +
+Lemma size_XmulC a : a != 0 → size ('X × a %:P) = 2.
+ +
+ +
+Lemma coefXn n i : 'X ^n `_i = (i == n )%:R.
+ +
+Lemma polyseqXn n : 'X ^n = rcons (nseq n 0) 1 :> seq R.
+ +
+Lemma size_polyXn n : size 'X ^n = n .+1.
+ +
+Lemma commr_polyXn p n : GRing.comm p 'X ^n.
+ +
+Lemma lead_coefXn n : lead_coef 'X ^n = 1.
+ +
+Lemma polyseqMXn n p : p != 0 → p × 'X ^n = ncons n 0 p :> seq R.
+ +
+Lemma coefMXn n p i : (p × 'X ^n )`_i = if i < n then 0 else p `_(i - n ).
+ +
+Lemma coefXnM n p i : ('X ^n × p )`_i = if i < n then 0 else p `_(i - n ).
+ +
+
+ +
+ Expansion of a polynomial as an indexed sum +
+
+Lemma poly_def n E : \poly_(i < n ) E i = \sum_(i < n ) E i *: 'X ^i.
+ +
+
+ +
+ Monic predicate +
+
+Definition monic := [qualify p | lead_coef p == 1].
+Fact monic_key : pred_key monic.
+Canonical monic_keyed := KeyedQualifier monic_key.
+ +
+Lemma monicE p : (p \is monic ) = (lead_coef p == 1).
+Lemma monicP p : reflect (lead_coef p = 1) (p \is monic).
+ +
+Lemma monic1 : 1 \is monic.
+Lemma monicX : 'X \is monic.
+Lemma monicXn n : 'X ^n \is monic.
+ +
+Lemma monic_neq0 p : p \is monic → p != 0.
+ +
+Lemma lead_coef_monicM p q : p \is monic → lead_coef (p × q) = lead_coef q.
+ +
+Lemma lead_coef_Mmonic p q : q \is monic → lead_coef (p × q) = lead_coef p.
+ +
+Lemma size_monicM p q :
+  p \is monic → q != 0 → size (p × q) = (size p + size q ).-1.
+ +
+Lemma size_Mmonic p q :
+  p != 0 → q \is monic → size (p × q) = (size p + size q ).-1.
+ +
+Lemma monicMl p q : p \is monic → (p × q \is monic ) = (q \is monic ).
+ +
+Lemma monicMr p q : q \is monic → (p × q \is monic ) = (p \is monic ).
+ +
+Fact monic_mulr_closed : mulr_closed monic.
+ Canonical monic_mulrPred := MulrPred monic_mulr_closed.
+ +
+Lemma monic_exp p n : p \is monic → p ^+ n \is monic.
+ +
+Lemma monic_prod I rI (P : pred I) (F : I → {poly R }):
+  (∀ i, P i → F i \is monic ) → \prod_(i <- rI | P i ) F i \is monic.
+ +
+Lemma monicXsubC c : 'X - c %:P \is monic.
+ +
+Lemma monic_prod_XsubC I rI (P : pred I) (F : I → R) :
+  \prod_(i <- rI | P i ) ('X - (F i )%:P ) \is monic.
+ +
+Lemma size_prod_XsubC I rI (F : I → R) :
+  size (\prod_(i <- rI ) ('X - (F i )%:P )) = (size rI ).+1.
+ +
+Lemma size_exp_XsubC n a : size (('X - a %:P ) ^+ n) = n .+1.
+ +
+
+ +
+ Some facts about regular elements. +
+
+ +
+Lemma lreg_lead p : GRing.lreg (lead_coef p) → GRing.lreg p.
+ +
+Lemma rreg_lead p : GRing.rreg (lead_coef p) → GRing.rreg p.
+ +
+Lemma lreg_lead0 p : GRing.lreg (lead_coef p) → p != 0.
+ +
+Lemma rreg_lead0 p : GRing.rreg (lead_coef p) → p != 0.
+ +
+Lemma lreg_size c p : GRing.lreg c → size (c *: p) = size p.
+ +
+Lemma lreg_polyZ_eq0 c p : GRing.lreg c → (c *: p == 0) = (p == 0).
+ +
+Lemma lead_coef_lreg c p :
+  GRing.lreg c → lead_coef (c *: p) = c × lead_coef p.
+ +
+Lemma rreg_size c p : GRing.rreg c → size (p × c %:P) = size p.
+ +
+Lemma rreg_polyMC_eq0 c p : GRing.rreg c → (p × c %:P == 0) = (p == 0).
+ +
+Lemma rreg_div0 q r d :
+    GRing.rreg (lead_coef d) → size r < size d →
+  (q × d + r == 0) = (q == 0) && (r == 0).
+ +
+Lemma monic_comreg p :
+  p \is monic → GRing.comm p (lead_coef p )%:P ∧ GRing.rreg (lead_coef p).
+ +
+
+ +
+ Horner evaluation of polynomials +
+
+Implicit Types s rs : seq R.
+Fixpoint horner_rec s x := if s is a :: s' then horner_rec s' x × x + a else 0.
+Definition horner p := horner_rec p.
+ +
+ +
+Lemma horner0 x : (0 : {poly R }).[x ] = 0.
+ +
+Lemma hornerC c x : (c %:P ).[x ] = c.
+ +
+Lemma hornerX x : 'X .[x ] = x.
+ +
+Lemma horner_cons p c x : (cons_poly c p ).[x ] = p .[x ] × x + c.
+ +
+Lemma horner_coef0 p : p .[0] = p `_0.
+ +
+Lemma hornerMXaddC p c x : (p × 'X + c %:P ).[x ] = p .[x ] × x + c.
+ +
+Lemma hornerMX p x : (p × 'X ).[x ] = p .[x ] × x.
+ +
+Lemma horner_Poly s x : (Poly s ).[x ] = horner_rec s x.
+ +
+Lemma horner_coef p x : p .[x ] = \sum_(i < size p ) p `_i × x ^+ i.
+ +
+Lemma horner_coef_wide n p x :
+  size p ≤ n → p .[x ] = \sum_(i < n ) p `_i × x ^+ i.
+ +
+Lemma horner_poly n E x : (\poly_(i < n ) E i ).[x ] = \sum_(i < n ) E i × x ^+ i.
+ +
+Lemma hornerN p x : (- p ).[x ] = - p .[x ].
+ +
+Lemma hornerD p q x : (p + q ).[x ] = p .[x ] + q .[x ].
+ +
+Lemma hornerXsubC a x : ('X - a %:P ).[x ] = x - a.
+ +
+Lemma horner_sum I (r : seq I) (P : pred I) F x :
+  (\sum_(i <- r | P i ) F i ).[x ] = \sum_(i <- r | P i ) (F i ).[x ].
+ +
+Lemma hornerCM a p x : (a %:P × p ).[x ] = a × p .[x ].
+ +
+Lemma hornerZ c p x : (c *: p ).[x ] = c × p .[x ].
+ +
+Lemma hornerMn n p x : (p *+ n ).[x ] = p .[x ] *+ n.
+ +
+Definition comm_coef p x := ∀ i, p `_i × x = x × p `_i.
+ +
+Definition comm_poly p x := x × p .[x ] = p .[x ] × x.
+ +
+Lemma comm_coef_poly p x : comm_coef p x → comm_poly p x.
+ +
+Lemma comm_poly0 x : comm_poly 0 x.
+ +
+Lemma comm_poly1 x : comm_poly 1 x.
+ +
+Lemma comm_polyX x : comm_poly 'X x.
+ +
+Lemma hornerM_comm p q x : comm_poly q x → (p × q ).[x ] = p .[x ] × q .[x ].
+ +
+Lemma horner_exp_comm p x n : comm_poly p x → (p ^+ n ).[x ] = p .[x ] ^+ n.
+ +
+Lemma hornerXn x n : ('X ^n ).[x ] = x ^+ n.
+ +
+Definition hornerE_comm :=
+  (hornerD , hornerN , hornerX , hornerC , horner_cons ,
+   simp , hornerCM , hornerZ ,
+   (fun p x ⇒ hornerM_comm p (comm_polyX x))).
+ +
+Definition root p : pred R := fun x ⇒ p .[x ] == 0.
+ +
+Lemma mem_root p x : x \in root p = (p .[x ] == 0).
+ +
+Lemma rootE p x : (root p x = (p .[x ] == 0)) × ((x \in root p ) = (p .[x ] == 0)).
+ +
+Lemma rootP p x : reflect (p .[x ] = 0) (root p x).
+ +
+Lemma rootPt p x : reflect (p .[x ] == 0) (root p x).
+ +
+Lemma rootPf p x : reflect ((p .[x ] == 0) = false) (~~ root p x).
+ +
+Lemma rootC a x : root a %:P x = (a == 0).
+ +
+Lemma root0 x : root 0 x.
+ +
+Lemma root1 x : ~~ root 1 x.
+ +
+Lemma rootX x : root 'X x = (x == 0).
+ +
+Lemma rootN p x : root (- p) x = root p x.
+ +
+Lemma root_size_gt1 a p : p != 0 → root p a → 1 < size p.
+ +
+Lemma root_XsubC a x : root ('X - a %:P) x = (x == a ).
+ +
+Lemma root_XaddC a x : root ('X + a %:P) x = (x == - a ).
+ +
+Theorem factor_theorem p a : reflect (∃ q, p = q × ('X - a %:P )) (root p a).
+ +
+Lemma multiplicity_XsubC p a :
+  {m | exists2 q, (p != 0) ==> ~~ root q a & p = q × ('X - a %:P ) ^+ m }.
+ +
+
+ +
+ Roots of unity. +
+
+ +
+Lemma size_Xn_sub_1 n : n > 0 → size ('X ^n - 1 : {poly R }) = n .+1.
+ +
+Lemma monic_Xn_sub_1 n : n > 0 → 'X ^n - 1 \is monic.
+ +
+Definition root_of_unity n : pred R := root ('X ^n - 1).
+ +
+Lemma unity_rootE n z : n .-unity_root z = (z ^+ n == 1).
+ +
+Lemma unity_rootP n z : reflect (z ^+ n = 1) (n .-unity_root z).
+ +
+Definition primitive_root_of_unity n z :=
+  (n > 0) && [∀ i : 'I_n , i .+1 .-unity_root z == (i .+1 == n )].
+ +
+Lemma prim_order_exists n z :
+  n > 0 → z ^+ n = 1 → {m | m .-primitive_root z & (m %| n )}.
+ +
+Section OnePrimitive.
+ +
+Variables (n : nat) (z : R).
+Hypothesis prim_z : n .-primitive_root z.
+ +
+Lemma prim_order_gt0 : n > 0.
+Let n_gt0 := prim_order_gt0.
+ +
+Lemma prim_expr_order : z ^+ n = 1.
+ +
+Lemma prim_expr_mod i : z ^+ (i %% n ) = z ^+ i.
+ +
+Lemma prim_order_dvd i : (n %| i ) = (z ^+ i == 1).
+ +
+Lemma eq_prim_root_expr i j : (z ^+ i == z ^+ j ) = (i == j %[mod n ]).
+ +
+Lemma exp_prim_root k : (n %/ gcdn k n ).-primitive_root (z ^+ k).
+ +
+Lemma dvdn_prim_root m : (m %| n)%N → m .-primitive_root (z ^+ (n %/ m )).
+ +
+End OnePrimitive.
+ +
+Lemma prim_root_exp_coprime n z k :
+  n .-primitive_root z → n .-primitive_root (z ^+ k) = coprime k n.
+ +
+
+ +
+ Lifting a ring predicate to polynomials. +
+
+ +
+Definition polyOver (S : pred_class) :=
+  [qualify a p : {poly R } | all (mem S) p ].
+ +
+Fact polyOver_key S : pred_key (polyOver S).
+Canonical polyOver_keyed S := KeyedQualifier (polyOver_key S).
+ +
+Lemma polyOverS (S1 S2 : pred_class) :
+  {subset S1 ≤ S2 } → {subset polyOver S1 ≤ polyOver S2 }.
+ +
+Lemma polyOver0 S : 0 \is a polyOver S.
+ +
+Lemma polyOver_poly (S : pred_class) n E :
+  (∀ i, i < n → E i \in S ) → \poly_(i < n ) E i \is a polyOver S.
+ +
+Section PolyOverAdd.
+ +
+Variables (S : predPredType R) (addS : addrPred S) (kS : keyed_pred addS).
+ +
+Lemma polyOverP {p} : reflect (∀ i, p `_i \in kS) (p \in polyOver kS).
+ +
+Lemma polyOverC c : (c %:P \in polyOver kS ) = (c \in kS ).
+ +
+Fact polyOver_addr_closed : addr_closed (polyOver kS).
+Canonical polyOver_addrPred := AddrPred polyOver_addr_closed.
+ +
+End PolyOverAdd.
+ +
+Fact polyOverNr S (addS : zmodPred S) (kS : keyed_pred addS) :
+  oppr_closed (polyOver kS).
+Canonical polyOver_opprPred S addS kS := OpprPred (@polyOverNr S addS kS).
+Canonical polyOver_zmodPred S addS kS := ZmodPred (@polyOverNr S addS kS).
+ +
+Section PolyOverSemiring.
+ +
+Context (S : pred_class) (ringS : @semiringPred R S) (kS : keyed_pred ringS).
+ +
+Fact polyOver_mulr_closed : mulr_closed (polyOver kS).
+Canonical polyOver_mulrPred := MulrPred polyOver_mulr_closed.
+Canonical polyOver_semiringPred := SemiringPred polyOver_mulr_closed.
+ +
+Lemma polyOverZ : {in kS & polyOver kS , ∀ c p, c *: p \is a polyOver kS }.
+ +
+Lemma polyOverX : 'X \in polyOver kS.
+ +
+Lemma rpred_horner : {in polyOver kS & kS , ∀ p x, p .[x ] \in kS }.
+ +
+End PolyOverSemiring.
+ +
+Section PolyOverRing.
+ +
+Context (S : pred_class) (ringS : @subringPred R S) (kS : keyed_pred ringS).
+Canonical polyOver_smulrPred := SmulrPred (polyOver_mulr_closed kS).
+Canonical polyOver_subringPred := SubringPred (polyOver_mulr_closed kS).
+ +
+Lemma polyOverXsubC c : ('X - c %:P \in polyOver kS ) = (c \in kS ).
+ +
+End PolyOverRing.
+ +
+
+ +
+ Single derivative. +
+
+ +
+Definition deriv p := \poly_(i < (size p ).-1 ) (p `_i .+1 *+ i .+1 ).
+ +
+ +
+Lemma coef_deriv p i : p ^``_i = p `_i .+1 *+ i .+1.
+ +
+Lemma polyOver_deriv S (ringS : semiringPred S) (kS : keyed_pred ringS) :
+  {in polyOver kS , ∀ p, p ^` \is a polyOver kS }.
+ +
+Lemma derivC c : c %:P ^` = 0.
+ +
+Lemma derivX : ('X )^` = 1.
+ +
+Lemma derivXn n : 'X ^n ^` = 'X ^n .-1 *+ n.
+ +
+Fact deriv_is_linear : linear deriv.
+Canonical deriv_additive := Additive deriv_is_linear.
+Canonical deriv_linear := Linear deriv_is_linear.
+ +
+Lemma deriv0 : 0^` = 0.
+ +
+Lemma derivD : {morph deriv : p q / p + q }.
+ +
+Lemma derivN : {morph deriv : p / - p }.
+ +
+Lemma derivB : {morph deriv : p q / p - q }.
+ +
+Lemma derivXsubC (a : R) : ('X - a %:P )^` = 1.
+ +
+Lemma derivMn n p : (p *+ n )^` = p ^` *+ n.
+ +
+Lemma derivMNn n p : (p *- n )^` = p ^` *- n.
+ +
+Lemma derivZ c p : (c *: p )^` = c *: p ^`.
+ +
+Lemma deriv_mulC c p : (c %:P × p )^` = c %:P × p ^`.
+ +
+Lemma derivMXaddC p c : (p × 'X + c %:P )^` = p + p ^` × 'X.
+ +
+Lemma derivM p q : (p × q )^` = p ^` × q + p × q ^`.
+ +
+Definition derivE := Eval lazy beta delta [morphism_2 morphism_1] in
+  (derivZ , deriv_mulC , derivC , derivX , derivMXaddC , derivXsubC , derivM , derivB ,
+   derivD , derivN , derivXn , derivM , derivMn ).
+ +
+
+ +
+ Iterated derivative. +
+
+Definition derivn n p := iter n deriv p.
+ +
+ +
+Lemma derivn0 p : p ^`(0) = p.
+ +
+Lemma derivn1 p : p ^`(1) = p ^`.
+ +
+Lemma derivnS p n : p ^`(n .+1 ) = p ^`(n )^`.
+ +
+Lemma derivSn p n : p ^`(n .+1 ) = p ^`^`(n ).
+ +
+Lemma coef_derivn n p i : p ^`(n )`_i = p `_(n + i ) *+ (n + i ) ^_ n.
+ +
+Lemma polyOver_derivn S (ringS : semiringPred S) (kS : keyed_pred ringS) :
+  {in polyOver kS , ∀ p n, p ^`(n ) \is a polyOver kS }.
+ +
+Fact derivn_is_linear n : linear (derivn n).
+ Canonical derivn_additive n := Additive (derivn_is_linear n).
+Canonical derivn_linear n := Linear (derivn_is_linear n).
+ +
+Lemma derivnC c n : c %:P ^`(n ) = if n == 0%N then c %:P else 0.
+ +
+Lemma derivnD n : {morph derivn n : p q / p + q }.
+ +
+Lemma derivn_sub n : {morph derivn n : p q / p - q }.
+ +
+Lemma derivnMn n m p : (p *+ m )^`(n ) = p ^`(n ) *+ m.
+ +
+Lemma derivnMNn n m p : (p *- m )^`(n ) = p ^`(n ) *- m.
+ +
+Lemma derivnN n : {morph derivn n : p / - p }.
+ +
+Lemma derivnZ n : scalable (derivn n).
+ +
+Lemma derivnXn m n : 'X ^m ^`(n ) = 'X ^(m - n ) *+ m ^_ n.
+ +
+Lemma derivnMXaddC n p c :
+  (p × 'X + c %:P )^`(n .+1 ) = p ^`(n ) *+ n .+1 + p ^`(n .+1 ) × 'X.
+ +
+Lemma derivn_poly0 p n : size p ≤ n → p ^`(n ) = 0.
+ +
+Lemma lt_size_deriv (p : {poly R }) : p != 0 → size p ^` < size p.
+ +
+
+ +
+ A normalising version of derivation to get the division by n! in Taylor +
+
+ +
+Definition nderivn n p := \poly_(i < size p - n ) (p `_(n + i ) *+ 'C (n + i , n )).
+ +
+ +
+Lemma coef_nderivn n p i : p ^`N (n )`_i = p `_(n + i ) *+ 'C (n + i , n ).
+ +
+
+ +
+ Here is the division by n! +
+
+Lemma nderivn_def n p : p ^`(n ) = p ^`N (n ) *+ n `!.
+ +
+Lemma polyOver_nderivn S (ringS : semiringPred S) (kS : keyed_pred ringS) :
+  {in polyOver kS , ∀ p n, p ^`N (n ) \in polyOver kS }.
+ +
+Lemma nderivn0 p : p ^`N (0) = p.
+ +
+Lemma nderivn1 p : p ^`N (1) = p ^`.
+ +
+Lemma nderivnC c n : (c %:P )^`N (n ) = if n == 0%N then c %:P else 0.
+ +
+Lemma nderivnXn m n : 'X ^m ^`N (n ) = 'X ^(m - n ) *+ 'C (m , n ).
+ +
+Fact nderivn_is_linear n : linear (nderivn n).
+Canonical nderivn_additive n := Additive(nderivn_is_linear n).
+Canonical nderivn_linear n := Linear (nderivn_is_linear n).
+ +
+Lemma nderivnD n : {morph nderivn n : p q / p + q }.
+ +
+Lemma nderivnB n : {morph nderivn n : p q / p - q }.
+ +
+Lemma nderivnMn n m p : (p *+ m )^`N (n ) = p ^`N (n ) *+ m.
+ +
+Lemma nderivnMNn n m p : (p *- m )^`N (n ) = p ^`N (n ) *- m.
+ +
+Lemma nderivnN n : {morph nderivn n : p / - p }.
+ +
+Lemma nderivnZ n : scalable (nderivn n).
+ +
+Lemma nderivnMXaddC n p c :
+  (p × 'X + c %:P )^`N (n .+1 ) = p ^`N (n ) + p ^`N (n .+1 ) × 'X.
+ +
+Lemma nderivn_poly0 p n : size p ≤ n → p ^`N (n ) = 0.
+ +
+Lemma nderiv_taylor p x h :
+  GRing.comm x h → p .[x + h ] = \sum_(i < size p ) p ^`N (i ).[x ] × h ^+ i.
+ +
+Lemma nderiv_taylor_wide n p x h :
+    GRing.comm x h → size p ≤ n →
+  p .[x + h ] = \sum_(i < n ) p ^`N (i ).[x ] × h ^+ i.
+ +
+End PolynomialTheory.
+ +
+Notation "\poly_ ( i < n ) E" := (poly n (fun i ⇒ E)) : ring_scope.
+Notation "c %:P" := (polyC c) : ring_scope.
+Notation "'X" := (polyX _) : ring_scope.
+Notation "''X^' n" := ('X ^+ n) : ring_scope.
+Notation "p .[ x ]" := (horner p x) : ring_scope.
+Notation "n .-unity_root" := (root_of_unity n) : ring_scope.
+Notation "n .-primitive_root" := (primitive_root_of_unity n) : ring_scope.
+Notation "a ^` " := (deriv a) : ring_scope.
+Notation "a ^` ( n )" := (derivn n a) : ring_scope.
+Notation "a ^`N ( n )" := (nderivn n a) : ring_scope.
+ +
+ +
+
+ +
+ Container morphism. +
+
+Section MapPoly.
+ +
+Section Definitions.
+ +
+Variables (aR rR : ringType) (f : aR → rR).
+ +
+Definition map_poly (p : {poly aR }) := \poly_(i < size p ) f p `_i.
+ +
+
+ +
+ 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. +
+
+Lemma map_polyE p : map_poly p = Poly (map f p).
+ +
+Definition commr_rmorph u := ∀ x, GRing.comm u (f x).
+ +
+Definition horner_morph u of commr_rmorph u := fun p ⇒ (map_poly p ).[u ].
+ +
+End Definitions.
+ +
+Variables aR rR : ringType.
+ +
+Section Combinatorial.
+ +
+Variables (iR : ringType) (f : aR → rR).
+ +
+Lemma map_poly0 : 0^f = 0.
+ +
+Lemma eq_map_poly (g : aR → rR) : f =1 g → map_poly f =1 map_poly g.
+ +
+Lemma map_poly_id g (p : {poly iR }) :
+  {in (p : seq iR ), g =1 id } → map_poly g p = p.
+ +
+Lemma coef_map_id0 p i : f 0 = 0 → (p ^f )`_i = f p `_i.
+ +
+Lemma map_Poly_id0 s : f 0 = 0 → (Poly s )^f = Poly (map f s).
+ +
+Lemma map_poly_comp_id0 (g : iR → aR) p :
+  f 0 = 0 → map_poly (f \o g) p = (map_poly g p )^f.
+ +
+Lemma size_map_poly_id0 p : f (lead_coef p) != 0 → size p ^f = size p.
+ +
+Lemma map_poly_eq0_id0 p : f (lead_coef p) != 0 → (p ^f == 0) = (p == 0).
+ +
+Lemma lead_coef_map_id0 p :
+  f 0 = 0 → f (lead_coef p) != 0 → lead_coef p ^f = f (lead_coef p).
+ +
+Hypotheses (inj_f : injective f) (f_0 : f 0 = 0).
+ +
+Lemma size_map_inj_poly p : size p ^f = size p.
+ +
+Lemma map_inj_poly : injective (map_poly f).
+ +
+Lemma lead_coef_map_inj p : lead_coef p ^f = f (lead_coef p).
+ +
+End Combinatorial.
+ +
+Lemma map_polyK (f : aR → rR) g :
+  cancel g f → f 0 = 0 → cancel (map_poly g) (map_poly f).
+ +
+Section Additive.
+ +
+Variables (iR : ringType) (f : {additive aR → rR }).
+ +
+ +
+Lemma coef_map p i : p ^f `_i = f p `_i.
+ +
+Lemma map_Poly s : (Poly s )^f = Poly (map f s).
+ +
+Lemma map_poly_comp (g : iR → aR) p :
+  map_poly (f \o g) p = map_poly f (map_poly g p).
+ +
+Fact map_poly_is_additive : additive (map_poly f).
+ Canonical map_poly_additive := Additive map_poly_is_additive.
+ +
+Lemma map_polyC a : (a %:P )^f = (f a )%:P.
+ +
+Lemma lead_coef_map_eq p :
+  f (lead_coef p) != 0 → lead_coef p ^f = f (lead_coef p).
+ +
+End Additive.
+ +
+Variable f : {rmorphism aR → rR }.
+Implicit Types p : {poly aR }.
+ +
+ +
+Fact map_poly_is_rmorphism : rmorphism (map_poly f).
+Canonical map_poly_rmorphism := RMorphism map_poly_is_rmorphism.
+ +
+Lemma map_polyZ c p : (c *: p )^f = f c *: p ^f.
+ Canonical map_poly_linear :=
+  AddLinear (map_polyZ : scalable_for (f \; *:%R) (map_poly f)).
+Canonical map_poly_lrmorphism := [lrmorphism of map_poly f ].
+ +
+Lemma map_polyX : ('X )^f = 'X.
+ +
+Lemma map_polyXn n : ('X ^n )^f = 'X ^n.
+ +
+Lemma monic_map p : p \is monic → p ^f \is monic.
+ +
+Lemma horner_map p x : p ^f .[f x ] = f p .[x ].
+ +
+Lemma map_comm_poly p x : comm_poly p x → comm_poly p ^f (f x).
+ +
+Lemma map_comm_coef p x : comm_coef p x → comm_coef p ^f (f x).
+ +
+Lemma rmorph_root p x : root p x → root p ^f (f x).
+ +
+Lemma rmorph_unity_root n z : n .-unity_root z → n .-unity_root (f z).
+ +
+Section HornerMorph.
+ +
+Variable u : rR.
+Hypothesis cfu : commr_rmorph f u.
+ +
+Lemma horner_morphC a : horner_morph cfu a %:P = f a.
+ +
+Lemma horner_morphX : horner_morph cfu 'X = u.
+ +
+Fact horner_is_lrmorphism : lrmorphism_for (f \; *%R) (horner_morph cfu).
+Canonical horner_additive := Additive horner_is_lrmorphism.
+Canonical horner_rmorphism := RMorphism horner_is_lrmorphism.
+Canonical horner_linear := AddLinear horner_is_lrmorphism.
+Canonical horner_lrmorphism := [lrmorphism of horner_morph cfu ].
+ +
+End HornerMorph.
+ +
+Lemma deriv_map p : p ^f ^` = (p ^`)^f.
+ +
+Lemma derivn_map p n : p ^f ^`(n ) = (p ^`(n ))^f.
+ +
+Lemma nderivn_map p n : p ^f ^`N (n ) = (p ^`N (n ))^f.
+ +
+End MapPoly.
+ +
+
+ +
+ Morphisms from the polynomial ring, and the initiality of polynomials + with respect to these. +
+
+Section MorphPoly.
+ +
+Variable (aR rR : ringType) (pf : {rmorphism {poly aR } → rR }).
+ +
+Lemma poly_morphX_comm : commr_rmorph (pf \o polyC) (pf 'X).
+ +
+Lemma poly_initial : pf =1 horner_morph poly_morphX_comm.
+ +
+End MorphPoly.
+ +
+Notation "p ^:P" := (map_poly polyC p) : ring_scope.
+ +
+Section PolyCompose.
+ +
+Variable R : ringType.
+Implicit Types p q : {poly R }.
+ +
+Definition comp_poly q p := p ^:P .[q ].
+ +
+ +
+Lemma size_map_polyC p : size p ^:P = size p.
+ +
+Lemma map_polyC_eq0 p : (p ^:P == 0) = (p == 0).
+ +
+Lemma root_polyC p x : root p ^:P x %:P = root p x.
+ +
+Lemma comp_polyE p q : p \Po q = \sum_(i < size p ) p `_i *: q ^+i.
+ +
+Lemma polyOver_comp S (ringS : semiringPred S) (kS : keyed_pred ringS) :
+  {in polyOver kS &, ∀ p q, p \Po q \in polyOver kS }.
+ +
+Lemma comp_polyCr p c : p \Po c %:P = p .[c ]%:P.
+ +
+Lemma comp_poly0r p : p \Po 0 = (p `_0 )%:P.
+ +
+Lemma comp_polyC c p : c %:P \Po p = c %:P.
+ +
+Fact comp_poly_is_linear p : linear (comp_poly p).
+Canonical comp_poly_additive p := Additive (comp_poly_is_linear p).
+Canonical comp_poly_linear p := Linear (comp_poly_is_linear p).
+ +
+Lemma comp_poly0 p : 0 \Po p = 0.
+ +
+Lemma comp_polyD p q r : (p + q ) \Po r = (p \Po r ) + (q \Po r ).
+ +
+Lemma comp_polyB p q r : (p - q ) \Po r = (p \Po r ) - (q \Po r ).
+ +
+Lemma comp_polyZ c p q : (c *: p ) \Po q = c *: (p \Po q ).
+ +
+Lemma comp_polyXr p : p \Po 'X = p.
+ +
+Lemma comp_polyX p : 'X \Po p = p.
+ +
+Lemma comp_poly_MXaddC c p q : (p × 'X + c %:P ) \Po q = (p \Po q ) × q + c %:P.
+ +
+Lemma comp_polyXaddC_K p z : (p \Po ('X + z %:P )) \Po ('X - z %:P ) = p.
+ +
+Lemma size_comp_poly_leq p q :
+  size (p \Po q) ≤ ((size p ).-1 × (size q ).-1 ).+1.
+ +
+End PolyCompose.
+ +
+Notation "p \Po q" := (comp_poly q p) : ring_scope.
+ +
+Lemma map_comp_poly (aR rR : ringType) (f : {rmorphism aR → rR }) p q :
+  map_poly f (p \Po q) = map_poly f p \Po map_poly f q.
+ +
+Section PolynomialComRing.
+ +
+Variable R : comRingType.
+Implicit Types p q : {poly R }.
+ +
+Fact poly_mul_comm p q : p × q = q × p.
+ +
+Canonical poly_comRingType := Eval hnf in ComRingType {poly R } poly_mul_comm.
+Canonical polynomial_comRingType :=
+  Eval hnf in ComRingType (polynomial R) poly_mul_comm.
+Canonical poly_algType := Eval hnf in CommAlgType R {poly R }.
+Canonical polynomial_algType :=
+  Eval hnf in [algType R of polynomial R for poly_algType ].
+ +
+Lemma hornerM p q x : (p × q ).[x ] = p .[x ] × q .[x ].
+ +
+Lemma horner_exp p x n : (p ^+ n ).[x ] = p .[x ] ^+ n.
+ +
+Lemma horner_prod I r (P : pred I) (F : I → {poly R }) x :
+  (\prod_(i <- r | P i ) F i ).[x ] = \prod_(i <- r | P i ) (F i ).[x ].
+ +
+Definition hornerE :=
+  (hornerD , hornerN , hornerX , hornerC , horner_cons ,
+   simp , hornerCM , hornerZ , hornerM ).
+ +
+Definition horner_eval (x : R) := horner ^~ x.
+Lemma horner_evalE x p : horner_eval x p = p .[x ].
+ +
+Fact horner_eval_is_lrmorphism x : lrmorphism_for *%R (horner_eval x).
+Canonical horner_eval_additive x := Additive (horner_eval_is_lrmorphism x).
+Canonical horner_eval_rmorphism x := RMorphism (horner_eval_is_lrmorphism x).
+Canonical horner_eval_linear x := AddLinear (horner_eval_is_lrmorphism x).
+Canonical horner_eval_lrmorphism x := [lrmorphism of horner_eval x ].
+ +
+Fact comp_poly_multiplicative q : multiplicative (comp_poly q).
+Canonical comp_poly_rmorphism q := AddRMorphism (comp_poly_multiplicative q).
+Canonical comp_poly_lrmorphism q := [lrmorphism of comp_poly q ].
+ +
+Lemma comp_polyM p q r : (p × q ) \Po r = (p \Po r ) × (q \Po r ).
+ +
+Lemma comp_polyA p q r : p \Po (q \Po r ) = (p \Po q ) \Po r.
+ +
+Lemma horner_comp p q x : (p \Po q ).[x ] = p .[q .[x ]].
+ +
+Lemma root_comp p q x : root (p \Po q) x = root p (q .[x ]).
+ +
+Lemma deriv_comp p q : (p \Po q ) ^` = (p ^` \Po q ) × q ^`.
+ +
+Lemma deriv_exp p n : (p ^+ n )^` = p ^` × p ^+ n .-1 *+ n.
+ +
+Definition derivCE := (derivE , deriv_exp ).
+ +
+End PolynomialComRing.
+ +
+Section PolynomialIdomain.
+ +
+
+ +
+ Integral domain structure on poly +
+
+Variable R : idomainType.
+ +
+Implicit Types (a b x y : R) (p q r m : {poly R }).
+ +
+Lemma size_mul p q : p != 0 → q != 0 → size (p × q) = (size p + size q ).-1.
+ +
+Fact poly_idomainAxiom p q : p × q = 0 → (p == 0) || (q == 0).
+ +
+Definition poly_unit : pred {poly R } :=
+  fun p ⇒ (size p == 1%N) && (p `_0 \in GRing.unit ).
+ +
+Definition poly_inv p := if p \in poly_unit then (p `_0 )^-1 %:P else p.
+ +
+Fact poly_mulVp : {in poly_unit , left_inverse 1 poly_inv *%R }.
+ +
+Fact poly_intro_unit p q : q × p = 1 → p \in poly_unit.
+ +
+Fact poly_inv_out : {in [predC poly_unit ], poly_inv =1 id }.
+ +
+Definition poly_comUnitMixin :=
+  ComUnitRingMixin poly_mulVp poly_intro_unit poly_inv_out.
+ +
+Canonical poly_unitRingType :=
+  Eval hnf in UnitRingType {poly R } poly_comUnitMixin.
+Canonical polynomial_unitRingType :=
+  Eval hnf in [unitRingType of polynomial R for poly_unitRingType ].
+ +
+Canonical poly_unitAlgType := Eval hnf in [unitAlgType R of {poly R }].
+Canonical polynomial_unitAlgType := Eval hnf in [unitAlgType R of polynomial R ].
+ +
+Canonical poly_comUnitRingType := Eval hnf in [comUnitRingType of {poly R }].
+Canonical polynomial_comUnitRingType :=
+  Eval hnf in [comUnitRingType of polynomial R ].
+ +
+Canonical poly_idomainType :=
+  Eval hnf in IdomainType {poly R } poly_idomainAxiom.
+Canonical polynomial_idomainType :=
+  Eval hnf in [idomainType of polynomial R for poly_idomainType ].
+ +
+Lemma poly_unitE p :
+  (p \in GRing.unit ) = (size p == 1%N) && (p `_0 \in GRing.unit ).
+ +
+Lemma poly_invE p : p ^-1 = if p \in GRing.unit then (p `_0 )^-1 %:P else p.
+ +
+Lemma polyC_inv c : c %:P ^-1 = (c ^-1 )%:P.
+ +
+Lemma rootM p q x : root (p × q) x = root p x || root q x.
+ +
+Lemma rootZ x a p : a != 0 → root (a *: p) x = root p x.
+ +
+Lemma size_scale a p : a != 0 → size (a *: p) = size p.
+ +
+Lemma size_Cmul a p : a != 0 → size (a %:P × p) = size p.
+ +
+Lemma lead_coefM p q : lead_coef (p × q) = lead_coef p × lead_coef q.
+ +
+Lemma lead_coefZ a p : lead_coef (a *: p) = a × lead_coef p.
+ +
+Lemma scale_poly_eq0 a p : (a *: p == 0) = (a == 0) || (p == 0).
+ +
+Lemma size_prod (I : finType) (P : pred I) (F : I → {poly R }) :
+    (∀ i, P i → F i != 0) →
+  size (\prod_(i | P i ) F i) = ((\sum_(i | P i ) size (F i)).+1 - #|P |)%N.
+ +
+Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p ).-1 × n)%N.
+ +
+Lemma lead_coef_exp p n : lead_coef (p ^+ n) = lead_coef p ^+ n.
+ +
+Lemma root_prod_XsubC rs x :
+  root (\prod_(a <- rs ) ('X - a %:P )) x = (x \in rs ).
+ +
+Lemma root_exp_XsubC n a x : root (('X - a %:P ) ^+ n .+1) x = (x == a ).
+ +
+Lemma size_comp_poly p q :
+  (size (p \Po q)).-1 = ((size p ).-1 × (size q ).-1)%N.
+ +
+Lemma size_comp_poly2 p q : size q = 2 → size (p \Po q) = size p.
+ +
+Lemma comp_poly2_eq0 p q : size q = 2 → (p \Po q == 0) = (p == 0).
+ +
+Lemma lead_coef_comp p q :
+  size q > 1 → lead_coef (p \Po q) = lead_coef p × lead_coef q ^+ (size p ).-1.
+ +
+Theorem max_poly_roots p rs :
+  p != 0 → all (root p) rs → uniq rs → size rs < size p.
+ +
+End PolynomialIdomain.
+ +
+Section MapFieldPoly.
+ +
+Variables (F : fieldType) (R : ringType) (f : {rmorphism F → R }).
+ +
+ +
+Lemma size_map_poly p : size p ^f = size p.
+ +
+Lemma lead_coef_map p : lead_coef p ^f = f (lead_coef p).
+ +
+Lemma map_poly_eq0 p : (p ^f == 0) = (p == 0).
+ +
+Lemma map_poly_inj : injective (map_poly f).
+ +
+Lemma map_monic p : (p ^f \is monic ) = (p \is monic ).
+ +
+Lemma map_poly_com p x : comm_poly p ^f (f x).
+ +
+Lemma fmorph_root p x : root p ^f (f x) = root p x.
+ +
+Lemma fmorph_unity_root n z : n .-unity_root (f z) = n .-unity_root z.
+ +
+Lemma fmorph_primitive_root n z :
+  n .-primitive_root (f z) = n .-primitive_root z.
+ +
+End MapFieldPoly.
+ +
+ +
+Section MaxRoots.
+ +
+Variable R : unitRingType.
+Implicit Types (x y : R) (rs : seq R) (p : {poly R }).
+ +
+Definition diff_roots (x y : R) := (x × y == y × x ) && (y - x \in GRing.unit ).
+ +
+Fixpoint uniq_roots rs :=
+  if rs is x :: rs' then all (diff_roots x) rs' && uniq_roots rs' else true.
+ +
+Lemma uniq_roots_prod_XsubC p rs :
+    all (root p) rs → uniq_roots rs →
+  ∃ q, p = q × \prod_(z <- rs ) ('X - z %:P ).
+ +
+Theorem max_ring_poly_roots p rs :
+  p != 0 → all (root p) rs → uniq_roots rs → size rs < size p.
+ +
+Lemma all_roots_prod_XsubC p rs :
+    size p = (size rs ).+1 → all (root p) rs → uniq_roots rs →
+  p = lead_coef p *: \prod_(z <- rs ) ('X - z %:P ).
+ +
+End MaxRoots.
+ +
+Section FieldRoots.
+ +
+Variable F : fieldType.
+Implicit Types (p : {poly F }) (rs : seq F).
+ +
+Lemma poly2_root p : size p = 2 → {r | root p r }.
+ +
+Lemma uniq_rootsE rs : uniq_roots rs = uniq rs.
+ +
+Section UnityRoots.
+ +
+Variable n : nat.
+ +
+Lemma max_unity_roots rs :
+  n > 0 → all n .-unity_root rs → uniq rs → size rs ≤ n.
+ +
+Lemma mem_unity_roots rs :
+    n > 0 → all n .-unity_root rs → uniq rs → size rs = n →
+  n .-unity_root =i rs.
+ +
+
+ +
+ Showing the existence of a primitive root requires the theory in cyclic. +
+
+ +
+Variable z : F.
+Hypothesis prim_z : n .-primitive_root z.
+ +
+Let zn := [seq z ^+ i | i <- index_iota 0 n ].
+ +
+Lemma factor_Xn_sub_1 : \prod_(0 ≤ i < n ) ('X - (z ^+ i )%:P ) = 'X ^n - 1.
+ +
+Lemma prim_rootP x : x ^+ n = 1 → {i : 'I_n | x = z ^+ i }.
+ +
+End UnityRoots.
+ +
+End FieldRoots.
+ +
+Section MapPolyRoots.
+ +
+Variables (F : fieldType) (R : unitRingType) (f : {rmorphism F → R }).
+ +
+Lemma map_diff_roots x y : diff_roots (f x) (f y) = (x != y ).
+ +
+Lemma map_uniq_roots s : uniq_roots (map f s) = uniq s.
+ +
+End MapPolyRoots.
+ +
+Section AutPolyRoot.
+
+ +
+ The action of automorphisms on roots of unity. +
+
+ +
+Variable F : fieldType.
+Implicit Types u v : {rmorphism F → F }.
+ +
+Lemma aut_prim_rootP u z n :
+  n .-primitive_root z → {k | coprime k n & u z = z ^+ k }.
+ +
+Lemma aut_unity_rootP u z n : n > 0 → z ^+ n = 1 → {k | u z = z ^+ k }.
+ +
+Lemma aut_unity_rootC u v z n : n > 0 → z ^+ n = 1 → u (v z) = v (u z).
+ +
+End AutPolyRoot.
+ +
+Module UnityRootTheory.
+ +
+Notation "n .-unity_root" := (root_of_unity n) : unity_root_scope.
+Notation "n .-primitive_root" := (primitive_root_of_unity n) : unity_root_scope.
+Open Scope unity_root_scope.
+ +
+Definition unity_rootE := unity_rootE.
+Definition unity_rootP := @unity_rootP.
+ +
+Definition prim_order_exists := prim_order_exists.
+Notation prim_order_gt0 := prim_order_gt0.
+Notation prim_expr_order := prim_expr_order.
+Definition prim_expr_mod := prim_expr_mod.
+Definition prim_order_dvd := prim_order_dvd.
+Definition eq_prim_root_expr := eq_prim_root_expr.
+ +
+Definition rmorph_unity_root := rmorph_unity_root.
+Definition fmorph_unity_root := fmorph_unity_root.
+Definition fmorph_primitive_root := fmorph_primitive_root.
+Definition max_unity_roots := max_unity_roots.
+Definition mem_unity_roots := mem_unity_roots.
+Definition prim_rootP := prim_rootP.
+ +
+End UnityRootTheory.
+ +
+Section DecField.
+ +
+Variable F : decFieldType.
+ +
+Lemma dec_factor_theorem (p : {poly F }) :
+  {s : seq F & {q : {poly F } | p = q × \prod_(x <- s ) ('X - x %:P )
+                             ∧ (q != 0 → ∀ x, ~~ root q x )}}.
+ +
+End DecField.
+ +
+Module PreClosedField.
+Section UseAxiom.
+ +
+Variable F : fieldType.
+Hypothesis closedF : GRing.ClosedField.axiom F.
+Implicit Type p : {poly F }.
+ +
+Lemma closed_rootP p : reflect (∃ x, root p x) (size p != 1%N).
+ +
+Lemma closed_nonrootP p : reflect (∃ x, ~~ root p x) (p != 0).
+ +
+End UseAxiom.
+End PreClosedField.
+ +
+Section ClosedField.
+ +
+Variable F : closedFieldType.
+Implicit Type p : {poly F }.
+ +
+Let closedF := @solve_monicpoly F.
+ +
+Lemma closed_rootP p : reflect (∃ x, root p x) (size p != 1%N).
+ +
+Lemma closed_nonrootP p : reflect (∃ x, ~~ root p x) (p != 0).
+ +
+Lemma closed_field_poly_normal p :
+  {r : seq F | p = lead_coef p *: \prod_(z <- r ) ('X - z %:P )}.
+ +
+End ClosedField.
+
+