From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.algebra.poly.html | 1189 ++++++++++++++++---------------
1 file changed, 633 insertions(+), 556 deletions(-)
(limited to 'docs/htmldoc/mathcomp.algebra.poly.html')
diff --git a/docs/htmldoc/mathcomp.algebra.poly.html b/docs/htmldoc/mathcomp.algebra.poly.html
index f28edfc..d10d9bb 100644
--- a/docs/htmldoc/mathcomp.algebra.poly.html
+++ b/docs/htmldoc/mathcomp.algebra.poly.html
@@ -21,7 +21,6 @@
@@ -159,25 +158,25 @@
Defines a polynomial as a sequence with <> 0 last element
- We need to break off the section here to let the argument scope
- directives take effect.
+ We need to break off the section here to let the Bind Scope directives
+ take effect.
@@ -246,10 +251,10 @@
Extensional interpretation (poly <=> nat -> R)
@@ -258,21 +263,21 @@
Builds a polynomial by extension.
@@ -281,19 +286,19 @@
Build a polynomial directly from a list of coefficients.
@@ -303,29 +308,29 @@
@@ -334,41 +339,41 @@
Zmodule structure for polynomial
@@ -435,62 +446,65 @@
@@ -501,110 +515,110 @@
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].
+ \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.
+ (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.
+ (mul_poly p q)`_i = \sum_(j < i.+1) p`_(i - j)%N × q`_j.
-Fact mul_polyA : associative mul_poly.
+Fact mul_polyA : associative mul_poly.
-Fact mul_1poly : left_id 1%:P mul_poly.
+Fact mul_1poly : left_id 1%:P mul_poly.
-Fact mul_poly1 : right_id 1%:P mul_poly.
+Fact mul_poly1 : right_id 1%:P mul_poly.
-Fact mul_polyDl : left_distributive mul_poly +%R.
+Fact mul_polyDl : left_distributive mul_poly +%R.
-Fact mul_polyDr : right_distributive mul_poly +%R.
+Fact mul_polyDr : right_distributive mul_poly +%R.
-Fact poly1_neq0 : 1%:P != 0 :> {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 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 polyC1 : 1%:P = 1 :> {poly R}.
-Lemma polyseq1 : (1 : {poly R}) = [:: 1] :> seq R.
+Lemma polyseq1 : (1 : {poly R}) = [:: 1] :> seq R.
-Lemma size_poly1 : size (1 : {poly R}) = 1%N.
+Lemma size_poly1 : size (1 : {poly R}) = 1%N.
-Lemma coef1 i : (1 : {poly R})`_i = (i == 0%N)%:R.
+Lemma coef1 i : (1 : {poly R})`_i = (i == 0%N)%:R.
-Lemma lead_coef1 : lead_coef 1 = 1 :> 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 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 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 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.
+ 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.
+ 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.
+ 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 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 coefCM c p i : (c%:P × p)`_i = c × p`_i.
-Lemma coefMC c p i : (p × c%:P)`_i = p`_i × c.
+Lemma coefMC c p i : (p × c%:P)`_i = p`_i × c.
-Lemma polyC_mul : {morph polyC : a b / a × b}.
+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 polyC_exp n : {morph polyC : c / c ^+ n}.
-Lemma size_exp_leq p n : size (p ^+ n) ≤ ((size p).-1 × n).+1.
+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.
+Lemma size_Msign p n : size ((-1) ^+ n × p) = size p.
-Fact coefp0_multiplicative : multiplicative (coefp 0 : {poly R} → R).
+Fact coefp0_multiplicative : multiplicative (coefp 0 : {poly R} → R).
Canonical coefp0_rmorphism := AddRMorphism coefp0_multiplicative.
@@ -616,28 +630,28 @@
Algebra structure of polynomials.
@@ -677,98 +691,98 @@
The indeterminate, at last!
@@ -777,7 +791,7 @@
Expansion of a polynomial as an indexed sum
@@ -786,66 +800,66 @@
Monic predicate
@@ -856,41 +870,41 @@
@@ -900,75 +914,75 @@
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.
+
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 horner0 x :
(0
: {poly R}).[x] = 0.
-
Lemma hornerC c x :
(c%:P).[x] = c.
+
Lemma hornerC c x :
(c%:P).[x] = c.
-
Lemma hornerX x :
'X.[x] = x.
+
Lemma hornerX x :
'X.[x] = x.
-
Lemma horner_cons p c x :
(cons_poly c p).[x] = p.[x] × x + c.
+
Lemma horner_cons p c x :
(cons_poly c p).[x] = p.[x] × x + c.
-
Lemma horner_coef0 p :
p.[0
] = p`_0.
+
Lemma horner_coef0 p :
p.[0
] = p`_0.
-
Lemma hornerMXaddC p c x :
(p × 'X + c%:P).[x] = p.[x] × x + c.
+
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 hornerMX p x :
(p × 'X).[x] = p.[x] × x.
-
Lemma horner_Poly s x :
(Poly s).[x] = horner_rec s 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 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.
+
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 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 hornerN p x :
(- p).[x] = - p.[x].
-
Lemma hornerD p q x :
(p + q).[x] = p.[x] + q.[x].
+
Lemma hornerD p q x :
(p + q).[x] = p.[x] + q.[x].
-
Lemma hornerXsubC a x :
('X - a%:P).[x] = x - a.
+
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 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 hornerCM a p x :
(a%:P × p).[x] = a × p.[x].
-
Lemma hornerZ c p x :
(c *: p).[x] = c × p.[x].
+
Lemma hornerZ c p x :
(c *: p).[x] = c × p.[x].
-
Lemma hornerMn n p x :
(p *+ n).[x] = p.[x] *+ n.
+
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_coef p x :=
∀ i,
p`_i × x = x × p`_i.
-
Definition comm_poly p x :=
x × p.[x] = p.[x] × x.
+
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_coef_poly p x :
comm_coef p x → comm_poly p x.
Lemma comm_poly0 x :
comm_poly 0
x.
@@ -977,71 +991,71 @@
Lemma comm_poly1 x :
comm_poly 1
x.
-
Lemma comm_polyX x :
comm_poly 'X 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 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 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.
+
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)
)).
+
(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.
+
Definition root p :
pred R :=
fun x ⇒
p.[x] == 0.
-
Lemma mem_root p x :
x \in root p = (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 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 rootP p x :
reflect (
p.[x] = 0) (
root p x).
-
Lemma rootPt 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 rootPf p x :
reflect (
(p.[x] == 0
) = false) (
~~ root p x).
-
Lemma rootC a x :
root a%:P x = (a == 0
).
+
Lemma rootC a x :
root a%:P x = (a == 0
).
Lemma root0 x :
root 0
x.
-
Lemma root1 x :
~~ root 1
x.
+
Lemma root1 x :
~~ root 1
x.
-
Lemma rootX x :
root 'X x = (x == 0
).
+
Lemma rootX x :
root 'X x = (x == 0
).
-
Lemma rootN p x :
root (
- p)
x = root p x.
+
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_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_XsubC a x :
root (
'X - a%:P)
x = (x == a).
-
Lemma root_XaddC 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).
+
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}.
+
{m | exists2 q, (p != 0
) ==> ~~ root q a & p = q × ('X - a%:P) ^+ m}.
@@ -1052,63 +1066,63 @@
@@ -1119,35 +1133,37 @@
-
Definition polyOver (
S :
pred_class) :=
-
[qualify a p : {poly R} | all (
mem S)
p].
+
Implicit Type S :
{pred R}.
-
Fact polyOver_key S :
pred_key (
polyOver S).
-
Canonical polyOver_keyed S :=
KeyedQualifier (
polyOver_key S).
+
Definition polyOver S :=
[qualify a p : {poly R} | all (
mem S)
p].
-
Lemma polyOverS (
S1 S2 :
pred_class) :
-
{subset S1 ≤ S2} → {subset polyOver S1 ≤ polyOver S2}.
+
Fact polyOver_key S :
pred_key (
polyOver S).
+
Canonical polyOver_keyed S :=
KeyedQualifier (
polyOver_key S).
-
Lemma polyOver0 S : 0
\is a polyOver 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 :
pred_class)
n E :
-
(∀ i,
i < n → E i \in S) → \poly_(i < n) E i \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 :
predPredType R) (
addS :
addrPred S) (
kS :
keyed_pred addS).
+
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 polyOverP {
p} :
reflect (
∀ i,
p`_i \in kS) (
p \in polyOver kS).
-
Lemma polyOverC c :
(c%:P \in polyOver kS) = (c \in kS).
+
Lemma polyOverC c :
(c%:P \in polyOver kS) = (c \in kS).
Fact polyOver_addr_closed :
addr_closed (
polyOver kS).
@@ -1157,7 +1173,7 @@
End PolyOverAdd.
-
Fact polyOverNr S (
addS :
zmodPred S) (
kS :
keyed_pred addS) :
+
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).
@@ -1166,7 +1182,7 @@
Section PolyOverSemiring.
-
Context (
S :
pred_class) (
ringS : @
semiringPred R S) (
kS :
keyed_pred ringS).
+
Variables (
S :
{pred R}) (
ringS :
semiringPred S) (
kS :
keyed_pred ringS).
Fact polyOver_mulr_closed :
mulr_closed (
polyOver kS).
@@ -1174,13 +1190,13 @@
Canonical polyOver_semiringPred :=
SemiringPred polyOver_mulr_closed.
-
Lemma polyOverZ :
{in kS & polyOver kS, ∀ c p,
c *: p \is a polyOver kS}.
+
Lemma polyOverZ :
{in kS & polyOver kS, ∀ c p,
c *: p \is a polyOver kS}.
-
Lemma polyOverX :
'X \in polyOver kS.
+
Lemma polyOverX :
'X \in polyOver kS.
-
Lemma rpred_horner :
{in polyOver kS & kS, ∀ p x,
p.[x] \in kS}.
+
Lemma rpred_horner :
{in polyOver kS & kS, ∀ p x,
p.[x] \in kS}.
End PolyOverSemiring.
@@ -1189,12 +1205,12 @@
Section PolyOverRing.
-
Context (
S :
pred_class) (
ringS : @
subringPred R S) (
kS :
keyed_pred ringS).
+
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).
+
Lemma polyOverXsubC c :
('X - c%:P \in polyOver kS) = (c \in kS).
End PolyOverRing.
@@ -1208,25 +1224,25 @@
-
Definition deriv p :=
\poly_(i < (size p).-1) (p`_i.+1 *+ i.+1).
+
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 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 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 derivC c :
c%:P^` = 0.
-
Lemma derivX :
('X)^` = 1.
+
Lemma derivX :
('X)^` = 1.
-
Lemma derivXn n :
'X^n^` = 'X^n.-1 *+ n.
+
Lemma derivXn n :
'X^n^` = 'X^n.-1 *+ n.
Fact deriv_is_linear :
linear deriv.
@@ -1234,42 +1250,42 @@
Canonical deriv_linear :=
Linear deriv_is_linear.
-
Lemma deriv0 : 0
^` = 0.
+
Lemma deriv0 : 0
^` = 0.
-
Lemma derivD :
{morph deriv : p q / p + q}.
+
Lemma derivD :
{morph deriv : p q / p + q}.
-
Lemma derivN :
{morph deriv : p / - p}.
+
Lemma derivN :
{morph deriv : p / - p}.
-
Lemma derivB :
{morph deriv : p q / p - q}.
+
Lemma derivB :
{morph deriv : p q / p - q}.
-
Lemma derivXsubC (
a :
R) :
('X - a%:P)^` = 1.
+
Lemma derivXsubC (
a :
R) :
('X - a%:P)^` = 1.
-
Lemma derivMn n p :
(p *+ n)^` = p^` *+ n.
+
Lemma derivMn n p :
(p *+ n)^` = p^` *+ n.
-
Lemma derivMNn n p :
(p *- n)^` = p^` *- n.
+
Lemma derivMNn n p :
(p *- n)^` = p^` *- n.
-
Lemma derivZ c p :
(c *: p)^` = c *: p^`.
+
Lemma derivZ c p :
(c *: p)^` = c *: p^`.
-
Lemma deriv_mulC c p :
(c%:P × p)^` = c%:P × p^`.
+
Lemma deriv_mulC c p :
(c%:P × p)^` = c%:P × p^`.
-
Lemma derivMXaddC p c :
(p × 'X + c%:P)^` = p + p^` × 'X.
+
Lemma derivMXaddC p c :
(p × 'X + c%:P)^` = p + p^` × 'X.
-
Lemma derivM p q :
(p × q)^` = p^` × q + p × q^`.
+
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).
+
(derivZ, deriv_mulC, derivC, derivX, derivMXaddC, derivXsubC, derivM, derivB,
+
derivD, derivN, derivXn, derivM, derivMn).
@@ -1283,23 +1299,23 @@
-
Lemma derivn0 p :
p^`(0
) = p.
+
Lemma derivn0 p :
p^`(0
) = p.
-
Lemma derivn1 p :
p^`(1
) = p^`.
+
Lemma derivn1 p :
p^`(1
) = p^`.
-
Lemma derivnS p n :
p^`(n.+1) = p^`(n)^`.
+
Lemma derivnS p n :
p^`(n.+1) = p^`(n)^`.
-
Lemma derivSn 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 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}.
+
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).
@@ -1307,38 +1323,38 @@
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 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 derivnD n :
{morph derivn n : p q / p + q}.
-
Lemma derivn_sub 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 derivnMn n m p :
(p *+ m)^`(n) = p^`(n) *+ m.
-
Lemma derivnMNn 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 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 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.
+
(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 derivn_poly0 p n :
size p ≤ n → p^`(n) = 0.
-
Lemma lt_size_deriv (
p :
{poly R}) :
p != 0
→ size p^` < size p.
+
Lemma lt_size_deriv (
p :
{poly R}) :
p != 0
→ size p^` < size p.
@@ -1349,12 +1365,12 @@
@@ -1363,23 +1379,23 @@
Here is the division by n!
@@ -1450,10 +1477,10 @@
Section Definitions.
-Variables (aR rR : ringType) (f : aR → rR).
+Variables (aR rR : ringType) (f : aR → rR).
-Definition map_poly (p : {poly aR}) := \poly_(i < size p) f p`_i.
+Definition map_poly (p : {poly aR}) := \poly_(i < size p) f p`_i.
@@ -1464,13 +1491,13 @@
instance of size_poly.
-
Lemma map_polyE p :
map_poly p = Poly (
map f p).
+
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].
+
Definition horner_morph u of commr_rmorph u :=
fun p ⇒
(map_poly p).[u].
End Definitions.
@@ -1482,92 +1509,92 @@
Section Combinatorial.
-
Variables (
iR :
ringType) (
f :
aR → rR).
+
Variables (
iR :
ringType) (
f :
aR → rR).
-
Lemma map_poly0 : 0
^f = 0.
+
Lemma map_poly0 : 0
^f = 0.
-
Lemma eq_map_poly (
g :
aR → rR) :
f =1 g → map_poly f =1 map_poly g.
+
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 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 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_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 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 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 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).
+
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).
+
Hypotheses (
inj_f :
injective f) (
f_0 :
f 0
= 0).
-
Lemma size_map_inj_poly p :
size p^f = size p.
+
Lemma size_map_inj_poly p :
size p^f = size p.
-
Lemma map_inj_poly :
injective (
map_poly f).
+
Lemma map_inj_poly :
injective (
map_poly f).
-
Lemma lead_coef_map_inj p :
lead_coef p^f = f (
lead_coef p).
+
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).
+
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}).
+
Variables (
iR :
ringType) (
f :
{additive aR → rR}).
-
Lemma coef_map p i :
p^f`_i = f p`_i.
+
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 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).
+
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 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).
+
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}.
+
Variable f :
{rmorphism aR → rR}.
+
Implicit Types p :
{poly aR}.
@@ -1576,34 +1603,34 @@
Canonical map_poly_rmorphism :=
RMorphism map_poly_is_rmorphism.
-
Lemma map_polyZ c p :
(c *: p)^f = f c *: p^f.
+
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].
+
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_polyX :
('X)^f = 'X.
-
Lemma map_polyXn n :
('X^n)^f = 'X^n.
+
Lemma map_polyXn n :
('X^n)^f = 'X^n.
-
Lemma monic_map p :
p \is monic → p^f \is monic.
+
Lemma monic_map p :
p \is monic → p^f \is monic.
-
Lemma horner_map p x :
p^f.[f x] = f p.[x].
+
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_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 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_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).
+
Lemma rmorph_unity_root n z :
n.-unity_root z → n.-unity_root (
f z).
Section HornerMorph.
@@ -1613,29 +1640,29 @@
Hypothesis cfu :
commr_rmorph f u.
-
Lemma horner_morphC a :
horner_morph cfu a%:P = f a.
+
Lemma horner_morphC a :
horner_morph cfu a%:P = f a.
-
Lemma horner_morphX :
horner_morph cfu 'X = u.
+
Lemma horner_morphX :
horner_morph cfu 'X = u.
-
Fact horner_is_lrmorphism :
lrmorphism_for (
f \; *%R) (
horner_morph cfu).
+
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].
+
Canonical horner_lrmorphism :=
[lrmorphism of horner_morph cfu].
End HornerMorph.
-
Lemma deriv_map p :
p^f^` = (p^`)^f.
+
Lemma deriv_map p :
p^f^` = (p^`)^f.
-
Lemma derivn_map p n :
p^f^`(n) = (p^`(n))^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.
+
Lemma nderivn_map p n :
p^f^`N(n) = (p^`N(n))^f.
End MapPoly.
@@ -1651,56 +1678,60 @@
Section MorphPoly.
-
Variable (
aR rR :
ringType) (
pf :
{rmorphism {poly aR} → rR}).
+
Variable (
aR rR :
ringType) (
pf :
{rmorphism {poly aR} → rR}).
-
Lemma poly_morphX_comm :
commr_rmorph (
pf \o polyC) (
pf 'X).
+
Lemma poly_morphX_comm :
commr_rmorph (
pf \o polyC) (
pf 'X).
-
Lemma poly_initial :
pf =1 horner_morph poly_morphX_comm.
+
Lemma poly_initial :
pf =1 horner_morph poly_morphX_comm.
End MorphPoly.
-
Notation "p ^:P" := (
map_poly polyC p) :
ring_scope.
+
Notation "p ^:P" := (
map_poly polyC p) :
ring_scope.
Section PolyCompose.
Variable R :
ringType.
-
Implicit Types p q :
{poly R}.
+
Implicit Types p q :
{poly R}.
-
Definition comp_poly q p :=
p^:P.[q].
+
Definition comp_poly q p :=
p^:P.[q].
-
Lemma size_map_polyC p :
size p^:P = size p.
+
Lemma size_map_polyC p :
size p^:P = size p.
-
Lemma map_polyC_eq0 p :
(p^:P == 0
) = (p == 0
).
+
Lemma map_polyC_eq0 p :
(p^:P == 0
) = (p == 0
).
-
Lemma root_polyC p x :
root p^:P x%:P = root p x.
+
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 comp_polyE p q :
p \Po q = \sum_(i < size p) p`_i *: q^+i.
-
Lemma polyOver_comp S (
ringS :
semiringPred S) (
kS :
keyed_pred ringS) :
-
{in polyOver kS &, ∀ p q,
p \Po q \in polyOver kS}.
+
Lemma 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_polyCr p c :
p \Po c%:P = p.[c]%:P.
-
Lemma comp_poly0r p :
p \Po 0
= (p`_0)%:P.
+
Lemma comp_poly0r p :
p \Po 0
= (p`_0)%:P.
-
Lemma comp_polyC c p :
c%:P \Po p = c%:P.
+
Lemma comp_polyC c p :
c%:P \Po p = c%:P.
Fact comp_poly_is_linear p :
linear (
comp_poly p).
@@ -1708,116 +1739,122 @@
Canonical comp_poly_linear p :=
Linear (
comp_poly_is_linear p).
-
Lemma comp_poly0 p : 0
\Po p = 0.
+
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_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_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_polyZ c p q :
(c *: p) \Po q = c *: (p \Po q).
-
Lemma comp_polyXr p :
p \Po 'X = p.
+
Lemma comp_polyXr p :
p \Po 'X = p.
-
Lemma comp_polyX p :
'X \Po p = 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_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 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.
+
size (
p \Po q)
≤ ((size p).-1 × (size q).-1).+1.
End PolyCompose.
-
Notation "p \Po q" := (
comp_poly q p) :
ring_scope.
+
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.
+
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}.
+
Implicit Types p q :
{poly R}.
-
Fact poly_mul_comm p q :
p × q = q × p.
+
Fact poly_mul_comm p q :
p × q = q × p.
-
Canonical poly_comRingType :=
Eval hnf in ComRingType {poly R} poly_mul_comm.
+
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 poly_algType :=
Eval hnf in CommAlgType R {poly R}.
Canonical polynomial_algType :=
-
Eval hnf in [algType R of polynomial R for poly_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 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_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].
+
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).
+
(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].
+
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).
+
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].
+
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].
+
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_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 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 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 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_comp p q :
(p \Po q) ^` = (p ^` \Po q) × q^`.
-
Lemma deriv_exp p n :
(p ^+ n)^` = p^` × p ^+ n.-1 *+ n.
+
Lemma deriv_exp p n :
(p ^+ n)^` = p^` × p ^+ n.-1 *+ n.
-
Definition derivCE :=
(derivE, deriv_exp).
+
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.
@@ -1831,29 +1868,29 @@
Variable R :
idomainType.
-
Implicit Types (
a b x y :
R) (
p q r m :
{poly R}).
+
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.
+
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
).
+
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_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.
+
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_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_intro_unit p q :
q × p = 1
→ p \in poly_unit.
-
Fact poly_inv_out :
{in [predC poly_unit], poly_inv =1 id}.
+
Fact poly_inv_out :
{in [predC poly_unit], poly_inv =1 id}.
Definition poly_comUnitMixin :=
@@ -1861,130 +1898,170 @@
Canonical poly_unitRingType :=
-
Eval hnf in UnitRingType {poly R} poly_comUnitMixin.
+
Eval hnf in UnitRingType {poly R} poly_comUnitMixin.
Canonical polynomial_unitRingType :=
-
Eval hnf in [unitRingType of polynomial R for poly_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_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 poly_comUnitRingType :=
Eval hnf in [comUnitRingType of {poly R}].
Canonical polynomial_comUnitRingType :=
-
Eval hnf in [comUnitRingType of polynomial R].
+
Eval hnf in [comUnitRingType of polynomial R].
Canonical poly_idomainType :=
-
Eval hnf in IdomainType {poly R} poly_idomainAxiom.
+
Eval hnf in IdomainType {poly R} poly_idomainAxiom.
Canonical polynomial_idomainType :=
-
Eval hnf in [idomainType of polynomial R for poly_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).
+
(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 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 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 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 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_scale a p :
a != 0
→ size (
a *: p)
= size p.
-
Lemma size_Cmul a p :
a != 0
→ size (
a%:P × 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_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 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 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 (
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 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 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).
+
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 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.
+
(size (
p \Po q)
).-1 = (
(size p).-1 × (size q).-1)%
N.
-
Lemma size_comp_poly2 p q :
size q = 2
→ size (
p \Po q)
= size p.
+
Lemma lead_coef_comp p q :
size q > 1
→
+
lead_coef (
p \Po q)
= (lead_coef p) × lead_coef q ^+ (size p).-1.
-
Lemma comp_poly2_eq0 p q :
size q = 2
→ (p \Po q == 0
) = (p == 0
).
-
+
Lemma comp_poly_eq0 p q :
size q > 1
→ (p \Po q == 0
) = (p == 0
).
+
-
Lemma lead_coef_comp p q :
-
size q > 1
→ lead_coef (
p \Po q)
= lead_coef p × lead_coef q ^+ (size p).-1.
+
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.
+
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}).
+
Variables (
F :
fieldType) (
R :
ringType) (
f :
{rmorphism F → R}).
-
Lemma size_map_poly p :
size p^f = size p.
+
Lemma size_map_poly p :
size p^f = size p.
-
Lemma lead_coef_map p :
lead_coef p^f = f (
lead_coef 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_eq0 p :
(p^f == 0
) = (p == 0
).
-
Lemma map_poly_inj :
injective (
map_poly f).
+
Lemma map_poly_inj :
injective (
map_poly f).
-
Lemma map_monic p :
(p^f \is monic) = (p \is monic).
+
Lemma map_monic p :
(p^f \is monic) = (p \is monic).
-
Lemma map_poly_com p x :
comm_poly p^f (
f x).
+
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_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_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.
+
n.-primitive_root (
f z)
= n.-primitive_root z.
End MapFieldPoly.
@@ -1996,28 +2073,28 @@
Variable R :
unitRingType.
-
Implicit Types (
x y :
R) (
rs :
seq R) (
p :
{poly R}).
+
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).
+
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.
+
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).
+
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.
+
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).
+
size p = (size rs).+1 → all (
root p)
rs → uniq_roots rs →
+
p = lead_coef p *: \prod_(z <- rs) ('X - z%:P).
End MaxRoots.
@@ -2027,28 +2104,28 @@
Variable F :
fieldType.
-
Implicit Types (
p :
{poly F}) (
rs :
seq F).
+
Implicit Types (
p :
{poly F}) (
rs :
seq F).
-
Lemma poly2_root p :
size p = 2
→ {r | root p r}.
+
Lemma poly2_root p :
size p = 2
→ {r | root p r}.
-
Lemma uniq_rootsE rs :
uniq_roots rs = uniq rs.
+
Lemma uniq_rootsE rs :
uniq_roots rs = uniq rs.
Section UnityRoots.
-
Variable n :
nat.
+
Variable n :
nat.
Lemma max_unity_roots rs :
-
n > 0
→ all n.-unity_root rs → uniq rs → size rs ≤ n.
+
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.
+
n > 0
→ all n.-unity_root rs → uniq rs → size rs = n →
+
n.-unity_root =i rs.
Variable z : F.
-Hypothesis prim_z : n.-primitive_root z.
+Hypothesis prim_z : n.-primitive_root z.
-Let zn := [seq z ^+ i | i <- index_iota 0 n].
+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 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}.
+Lemma prim_rootP x : x ^+ n = 1 → {i : 'I_n | x = z ^+ i}.
End UnityRoots.
@@ -2081,13 +2158,13 @@
Section MapPolyRoots.
-Variables (F : fieldType) (R : unitRingType) (f : {rmorphism F → R}).
+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_diff_roots x y : diff_roots (f x) (f y) = (x != y).
-Lemma map_uniq_roots s : uniq_roots (map f s) = uniq s.
+Lemma map_uniq_roots s : uniq_roots (map f s) = uniq s.
End MapPolyRoots.
@@ -2103,17 +2180,17 @@
Variable F : fieldType.
-Implicit Types u v : {rmorphism F → F}.
+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}.
+ 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_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).
+Lemma aut_unity_rootC u v z n : n > 0 → z ^+ n = 1 → u (v z) = v (u z).
End AutPolyRoot.
@@ -2122,8 +2199,8 @@
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.
+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.
@@ -2156,9 +2233,9 @@
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)}}.
+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.
@@ -2170,13 +2247,13 @@
Variable F : fieldType.
Hypothesis closedF : GRing.ClosedField.axiom F.
-Implicit Type p : {poly F}.
+Implicit Type p : {poly F}.
-Lemma closed_rootP p : reflect (∃ x, root p x) (size p != 1%N).
+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_nonrootP p : reflect (∃ x, ~~ root p x) (p != 0).
End UseAxiom.
@@ -2187,20 +2264,20 @@
Variable F : closedFieldType.
-Implicit Type p : {poly F}.
+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_rootP p : reflect (∃ x, root p x) (size p != 1%N).
-Lemma closed_nonrootP p : reflect (∃ x, ~~ root p x) (p != 0).
+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)}.
+ {r : seq F | p = lead_coef p *: \prod_(z <- r) ('X - z%:P)}.
End ClosedField.
--
cgit v1.2.3