# Library mathcomp.algebra.poly

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

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

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

### The submodule poly.UnityRootTheory can be used to

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

### We only show that these operations and properties are transferred by

morphisms whose domain is a field (thus ensuring injectivity). We prove the factor_theorem, and the max_poly_roots inequality relating the number of distinct roots of a polynomial and its size. The some polynomial lemmas use following suffix interpretation : C - constant polynomial (as in polyseqC : a%:P = nseq (a != 0) a). X - the polynomial variable 'X (as in coefX : 'X`_i = (i == 1%N)). Xn - power of 'X (as in monicXn : monic 'X^n).
Set Implicit Arguments.
Declare Scope unity_root_scope.
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 i (p : poly_of (Phant R)) := p`_i.
End Polynomial.
We need to break off the section here to let the Bind Scope directives take effect.
Bind Scope ring_scope with poly_of.
Bind Scope ring_scope with polynomial.
Arguments polyseq {R} p%R.
Arguments poly_inj {R} [p1%R p2%R] : rename.
Arguments coefp {R} i%N / p%R.
Notation "{ 'poly' T }" := (poly_of (Phant T)) : type_scope.
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 polyCD : {morph polyC : a b / a + b}.
Lemma polyCN : {morph polyC : c / - c}.
Lemma polyCB : {morph polyC : a b / a - b}.
Canonical polyC_additive := Additive polyCB.
Lemma polyCMn n : {morph polyC : c / c *+ n}.
Lemma size_opp p : size (- p) = size p.
Lemma lead_coefN 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 polyCM : {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%N.
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%N.
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%N.
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).
Lemma monic_lreg p : p \is monic → GRing.lreg p.
Lemma monic_rreg p : p \is monic → GRing.rreg 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 commr_horner a b p : GRing.comm a b → comm_coef p a → GRing.comm a p.[b].
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 derivnB 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.
Arguments monic {R}.
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.
Arguments monicP {R p}.
Arguments rootP {R p x}.
Arguments rootPf {R p x}.
Arguments rootPt {R p x}.
Arguments unity_rootP {R n z}.
Arguments polyOverP {R S0 addS kS p} : rename.
Arguments polyC_inj {R} [x1 x2] eq_x12P.
Arguments eq_poly {R n} [E1] E2 eq_E12.
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].
Canonical poly_comAlgType := Eval hnf in [comAlgType R of {poly R}].
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].
Section HornerAlg.
Variable A : algType R. (* For univariate polys, commutativity is not needed *)
Section Defs.
Variable a : A.
Lemma in_alg_comm : commr_rmorph (in_alg A) a.
Definition horner_alg := horner_morph in_alg_comm.
Lemma horner_algC c : horner_alg c%:P = c%:A.
Lemma horner_algX : horner_alg 'X = a.
Fact horner_alg_is_lrmorphism : lrmorphism horner_alg.
Canonical horner_alg_additive := Additive horner_alg_is_lrmorphism.
Canonical horner_alg_rmorphism := RMorphism horner_alg_is_lrmorphism.
Canonical horner_alg_linear := AddLinear horner_alg_is_lrmorphism.
Canonical horner_alg_lrmorphism := [lrmorphism of horner_alg].
End Defs.
Variable (pf : {lrmorphism {poly R} → A}).
Lemma poly_alg_initial : pf =1 horner_alg (pf 'X).
End HornerAlg.
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 polyCV 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%N → size (p \Po q) = size p.
Lemma comp_poly2_eq0 p q : size q = 2%N → (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.
Arguments map_poly_inj {F R} f [p1 p2] : rename.
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%N → {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.
Arguments unity_rootP {R n z}.
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.