- -

Library mathcomp.algebra.poly

- -

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

- -

- 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 Bind Scope directives - take effect. -
-
-Notation "{ 'poly' T }" := (poly_of (Phant T)).
-Notation coefp i := (coefp_head tt i).
- -
-Definition poly_countMixin (R : countRingType) :=
-  [countMixin of polynomial R by <:].
-Canonical polynomial_countType R := CountType _ (poly_countMixin R).
-Canonical poly_countType (R : countRingType) := [countType of {poly R }].
- -
-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 gt_size_poly_neq0 p n : (size p > n)%N → 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 size_polyC_leq1 (c : R) : (size c %: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.
- -
-Lemma lead_coefDr p q : size q > size p → lead_coef (p + q) = lead_coef q.
- -
-
- -
- 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. -
-
- -
-Implicit Type S : {pred R }.
- -
-Definition polyOver S := [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 R }) :
-  {subset S1 ≤ S2 } → {subset polyOver S1 ≤ polyOver S2 }.
- -
-Lemma polyOver0 S : 0 \is a polyOver S.
- -
-Lemma polyOver_poly S n E :
-  (∀ i, i < n → E i \in S ) → \poly_(i < n ) E i \is a polyOver S.
- -
-Section PolyOverAdd.
- -
-Variables (S : {pred 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.
- -
-Variables (S : {pred R }) (ringS : semiringPred 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.
- -
-Variables (S : {pred R }) (ringS : subringPred 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.
- -
-Lemma eq_poly n E1 E2 : E1 =1 E2 → poly n E1 = poly n E2.
- -
-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.
- -
- -
-Canonical polynomial_countZmodType (R : countRingType) :=
-  [countZmodType of polynomial R ].
-Canonical poly_countZmodType (R : countRingType) := [countZmodType of {poly R }].
-Canonical polynomial_countRingType (R : countRingType) :=
-  [countRingType of polynomial R ].
-Canonical poly_countRingType (R : countRingType) := [countRingType of {poly R }].
- -
-
- -
- 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 coef_comp_poly p q n :
-  (p \Po q )`_n = \sum_(i < size p ) p `_i × (q ^+ i )`_n.
- -
-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.
- -
-Canonical polynomial_countComRingType (R : countComRingType) :=
-  [countComRingType of polynomial R ].
-Canonical poly_countComRingType (R : countComRingType) :=
-  [countComRingType of {poly R }].
- -
-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_prod_seq (I : eqType) (s : seq I) (F : I → {poly R }) :
-    (∀ i, i \in s → F i != 0) →
-  size (\prod_(i <- s ) F i) = ((\sum_(i <- s ) size (F i)).+1 - size s)%N.
- -
-Lemma size_mul_eq1 p q :
-  (size (p × q) == 1%N) = ((size p == 1%N) && (size q == 1%N)).
- -
-Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I → {poly R }) :
-  reflect (∀ i, P i && (i \in s ) → size (F i) = 1%N)
-          (size (\prod_(i <- s | P i ) F i) == 1%N).
- -
-Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I → {poly R }) :
-  reflect (∀ i, P i → size (F i) = 1%N)
-          (size (\prod_(i | P i ) F i) == 1%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 lead_coef_comp p q : size q > 1 →
-  lead_coef (p \Po q) = (lead_coef p ) × lead_coef q ^+ (size p ).-1.
- -
-Lemma comp_poly_eq0 p q : size q > 1 → (p \Po q == 0) = (p == 0).
- -
-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).
- -
-Theorem max_poly_roots p rs :
-  p != 0 → all (root p) rs → uniq rs → size rs < size p.
- -
-Lemma roots_geq_poly_eq0 p (rs : seq R) : all (root p) rs → uniq rs →
-  (size rs ≥ size p)%N → p = 0.
- -
-End PolynomialIdomain.
- -
-Canonical polynomial_countUnitRingType (R : countIdomainType) :=
-  [countUnitRingType of polynomial R ].
-Canonical poly_countUnitRingType (R : countIdomainType) :=
-  [countUnitRingType of {poly R }].
-Canonical polynomial_countComUnitRingType (R : countIdomainType) :=
-  [countComUnitRingType of polynomial R ].
-Canonical poly_countComUnitRingType (R : countIdomainType) :=
-  [countComUnitRingType of {poly R }].
-Canonical polynomial_countIdomainType (R : countIdomainType) :=
-  [countIdomainType of polynomial R ].
-Canonical poly_countIdomainType (R : countIdomainType) :=
-  [countIdomainType of {poly R }].
- -
-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.
-
-