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.polydiv.html | 1115 ++++++++++++++--------------
1 file changed, 557 insertions(+), 558 deletions(-)
(limited to 'docs/htmldoc/mathcomp.algebra.polydiv.html')
diff --git a/docs/htmldoc/mathcomp.algebra.polydiv.html b/docs/htmldoc/mathcomp.algebra.polydiv.html
index e130606..7fba25f 100644
--- a/docs/htmldoc/mathcomp.algebra.polydiv.html
+++ b/docs/htmldoc/mathcomp.algebra.polydiv.html
@@ -21,7 +21,6 @@
@@ -161,7 +160,7 @@ rcoprimep p q == analogue of coprimep p q for coefficients in a ringType.
Variable R : ringType.
-Implicit Types d p q r : {poly R}.
+Implicit Types d p q r : {poly R}.
@@ -170,155 +169,155 @@ rcoprimep p q == analogue of coprimep p q for coefficients in a ringType.
Pseudo division, defined on an arbitrary ring
-
Definition redivp_rec (
q :
{poly R}) :=
+
Definition redivp_rec (
q :
{poly R}) :=
let sq :=
size q in
let cq :=
lead_coef q in
-
fix loop (
k :
nat) (
qq r :
{poly R})(
n :
nat) {
struct n} :=
-
if size r < sq then (k, qq, r) else
-
let m :=
(lead_coef r) *: 'X^(size r - sq) in
-
let qq1 :=
qq × cq%:P + m in
-
let r1 :=
r × cq%:P - m × q in
-
if n is n1.+1 then loop k.+1 qq1 r1 n1 else (k.+1, qq1, r1).
+
fix loop (
k :
nat) (
qq r :
{poly R})(
n :
nat) {
struct n} :=
+
if size r < sq then (k, qq, r) else
+
let m :=
(lead_coef r) *: 'X^(size r - sq) in
+
let qq1 :=
qq × cq%:P + m in
+
let r1 :=
r × cq%:P - m × q in
+
if n is n1.+1 then loop k.+1 qq1 r1 n1 else (k.+1, qq1, r1).
Definition redivp_expanded_def p q :=
-
if q == 0
then (0%
N, 0
, p) else redivp_rec q 0 0
p (
size p).
-
Fact redivp_key :
unit.
-
Definition redivp :
{poly R} → {poly R} → nat × {poly R} × {poly R} :=
-
locked_with redivp_key redivp_expanded_def.
-
Canonical redivp_unlockable :=
[unlockable fun redivp].
+
if q == 0
then (0%
N, 0
, p) else redivp_rec q 0 0
p (
size p).
+
Fact redivp_key :
unit.
+
Definition redivp :
{poly R} → {poly R} → nat × {poly R} × {poly R} :=
+
locked_with redivp_key redivp_expanded_def.
+
Canonical redivp_unlockable :=
[unlockable fun redivp].
-
Definition rdivp p q :=
((redivp p q).1).2.
-
Definition rmodp p q :=
(redivp p q).2.
-
Definition rscalp p q :=
((redivp p q).1).1.
-
Definition rdvdp p q :=
rmodp q p == 0.
+
Definition rdivp p q :=
((redivp p q).1).2.
+
Definition rmodp p q :=
(redivp p q).2.
+
Definition rscalp p q :=
((redivp p q).1).1.
+
Definition rdvdp p q :=
rmodp q p == 0.
Definition rmultp := [rel m d | rdvdp d m].
-
Lemma redivp_def p q :
redivp p q = (rscalp p q, rdivp p q, rmodp p q).
+
Lemma redivp_def p q :
redivp p q = (rscalp p q, rdivp p q, rmodp p q).
-
Lemma rdiv0p p :
rdivp 0
p = 0.
+
Lemma rdiv0p p :
rdivp 0
p = 0.
-
Lemma rdivp0 p :
rdivp p 0
= 0.
+
Lemma rdivp0 p :
rdivp p 0
= 0.
-
Lemma rdivp_small p q :
size p < size q → rdivp p q = 0.
+
Lemma rdivp_small p q :
size p < size q → rdivp p q = 0.
-
Lemma leq_rdivp p q :
size (
rdivp p q)
≤ size p.
+
Lemma leq_rdivp p q :
size (
rdivp p q)
≤ size p.
-
Lemma rmod0p p :
rmodp 0
p = 0.
+
Lemma rmod0p p :
rmodp 0
p = 0.
-
Lemma rmodp0 p :
rmodp p 0
= p.
+
Lemma rmodp0 p :
rmodp p 0
= p.
-
Lemma rscalp_small p q :
size p < size q → rscalp p q = 0%
N.
+
Lemma rscalp_small p q :
size p < size q → rscalp p q = 0%
N.
-
Lemma ltn_rmodp p q :
(size (
rmodp p q)
< size q) = (q != 0
).
+
Lemma ltn_rmodp p q :
(size (
rmodp p q)
< size q) = (q != 0
).
-
Lemma ltn_rmodpN0 p q :
q != 0
→ size (
rmodp p q)
< size q.
+
Lemma ltn_rmodpN0 p q :
q != 0
→ size (
rmodp p q)
< size q.
-
Lemma rmodp1 p :
rmodp p 1
= 0.
+
Lemma rmodp1 p :
rmodp p 1
= 0.
-
Lemma rmodp_small p q :
size p < size q → rmodp p q = p.
+
Lemma rmodp_small p q :
size p < size q → rmodp p q = p.
-
Lemma leq_rmodp m d :
size (
rmodp m d)
≤ size m.
+
Lemma leq_rmodp m d :
size (
rmodp m d)
≤ size m.
-
Lemma rmodpC p c :
c != 0
→ rmodp p c%:P = 0.
+
Lemma rmodpC p c :
c != 0
→ rmodp p c%:P = 0.
Lemma rdvdp0 d :
rdvdp d 0.
-
Lemma rdvd0p n :
(rdvdp 0
n) = (n == 0
).
+
Lemma rdvd0p n :
(rdvdp 0
n) = (n == 0
).
-
Lemma rdvd0pP n :
reflect (
n = 0) (
rdvdp 0
n).
+
Lemma rdvd0pP n :
reflect (
n = 0) (
rdvdp 0
n).
-
Lemma rdvdpN0 p q :
rdvdp p q → q != 0
→ p != 0.
+
Lemma rdvdpN0 p q :
rdvdp p q → q != 0
→ p != 0.
-
Lemma rdvdp1 d :
(rdvdp d 1
) = ((size d) == 1%
N).
+
Lemma rdvdp1 d :
(rdvdp d 1
) = ((size d) == 1%
N).
Lemma rdvd1p m :
rdvdp 1
m.
-
Lemma Nrdvdp_small (
n d :
{poly R}) :
-
n != 0
→ size n < size d → (rdvdp d n) = false.
+
Lemma Nrdvdp_small (
n d :
{poly R}) :
+
n != 0
→ size n < size d → (rdvdp d n) = false.
-
Lemma rmodp_eq0P p q :
reflect (
rmodp p q = 0) (
rdvdp q p).
+
Lemma rmodp_eq0P p q :
reflect (
rmodp p q = 0) (
rdvdp q p).
-
Lemma rmodp_eq0 p q :
rdvdp q p → rmodp p q = 0.
+
Lemma rmodp_eq0 p q :
rdvdp q p → rmodp p q = 0.
-
Lemma rdvdp_leq p q :
rdvdp p q → q != 0
→ size p ≤ size q.
+
Lemma rdvdp_leq p q :
rdvdp p q → q != 0
→ size p ≤ size q.
Definition rgcdp p q :=
-
let:
(p1, q1) :=
if size p < size q then (q, p) else (p, q) in
-
if p1 == 0
then q1 else
-
let fix loop (
n :
nat) (
pp qq :
{poly R}) {
struct n} :=
+
let:
(p1, q1) :=
if size p < size q then (q, p) else (p, q) in
+
if p1 == 0
then q1 else
+
let fix loop (
n :
nat) (
pp qq :
{poly R}) {
struct n} :=
let rr :=
rmodp pp qq in
-
if rr == 0
then qq else
-
if n is n1.+1 then loop n1 qq rr else rr in
+
if rr == 0
then qq else
+
if n is n1.+1 then loop n1 qq rr else rr in
loop (
size p1)
p1 q1.
-
Lemma rgcd0p :
left_id 0
rgcdp.
+
Lemma rgcd0p :
left_id 0
rgcdp.
-
Lemma rgcdp0 :
right_id 0
rgcdp.
+
Lemma rgcdp0 :
right_id 0
rgcdp.
Lemma rgcdpE p q :
-
rgcdp p q = if size p < size q
-
then rgcdp (
rmodp q p)
p else rgcdp (
rmodp p q)
q.
+
rgcdp p q = if size p < size q
+
then rgcdp (
rmodp q p)
p else rgcdp (
rmodp p q)
q.
-
CoInductive comm_redivp_spec m d :
nat × {poly R} × {poly R} → Type :=
-
ComEdivnSpec k (
q r :
{poly R})
of
- (
GRing.comm d (lead_coef d)%:P → m × (lead_coef d ^+ k)%:P = q × d + r) &
- (
d != 0
→ size r < size d) :
comm_redivp_spec m d (k, q, r).
+
Variant comm_redivp_spec m d :
nat × {poly R} × {poly R} → Type :=
+
ComEdivnSpec k (
q r :
{poly R})
of
+ (
GRing.comm d (lead_coef d)%:P → m × (lead_coef d ^+ k)%:P = q × d + r) &
+ (
d != 0
→ size r < size d) :
comm_redivp_spec m d (k, q, r).
Lemma comm_redivpP m d :
comm_redivp_spec m d (
redivp m d).
-
Lemma rmodpp p :
GRing.comm p (lead_coef p)%:P → rmodp p p = 0.
+
Lemma rmodpp p :
GRing.comm p (lead_coef p)%:P → rmodp p p = 0.
-
Definition rcoprimep (
p q :
{poly R}) :=
size (
rgcdp p q)
== 1%
N.
+
Definition rcoprimep (
p q :
{poly R}) :=
size (
rgcdp p q)
== 1%
N.
Fixpoint rgdcop_rec q p n :=
-
if n is m.+1 then
-
if rcoprimep p q then p
-
else rgdcop_rec q (
rdivp p (
rgcdp p q))
m
-
else (q == 0
)%:R.
+
if n is m.+1 then
+
if rcoprimep p q then p
+
else rgdcop_rec q (
rdivp p (
rgcdp p q))
m
+
else (q == 0
)%:R.
Definition rgdcop q p :=
rgdcop_rec q p (
size p).
-
Lemma rgdcop0 q :
rgdcop q 0
= (q == 0
)%:R.
+
Lemma rgdcop0 q :
rgdcop q 0
= (q == 0
)%:R.
End RingPseudoDivision.
@@ -337,19 +336,19 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
ringType.
-
Variable d :
{poly R}.
-
Hypothesis Cdl :
GRing.comm d (lead_coef d)%:P.
+
Variable d :
{poly R}.
+
Hypothesis Cdl :
GRing.comm d (lead_coef d)%:P.
Hypothesis Rreg :
GRing.rreg (
lead_coef d).
-
Implicit Types p q r :
{poly R}.
+
Implicit Types p q r :
{poly R}.
Lemma redivp_eq q r :
-
size r < size d →
-
let k :=
(redivp (
q × d + r)
d).1.1 in
-
let c :=
(lead_coef d ^+ k)%:P in
-
redivp (
q × d + r)
d = (k, q × c, r × c).
+
size r < size d →
+
let k :=
(redivp (
q × d + r)
d).1.1 in
+
let c :=
(lead_coef d ^+ k)%:P in
+
redivp (
q × d + r)
d = (k, q × c, r × c).
-Lemma rdvdp_mull p : rdvdp d (p × d).
+Lemma rdvdp_mull p : rdvdp d (p × d).
-Lemma rmodp_mull p : rmodp (p × d) d = 0.
+Lemma rmodp_mull p : rmodp (p × d) d = 0.
-Lemma rmodpp : rmodp d d = 0.
+Lemma rmodpp : rmodp d d = 0.
-Lemma rdivpp : rdivp d d = (lead_coef d ^+ rscalp d d)%:P.
+Lemma rdivpp : rdivp d d = (lead_coef d ^+ rscalp d d)%:P.
Lemma rdvdpp : rdvdp d d.
-Lemma rdivpK p : rdvdp d p →
- (rdivp p d) × d = p × (lead_coef d ^+ rscalp p d)%:P.
+Lemma rdivpK p : rdvdp d p →
+ (rdivp p d) × d = p × (lead_coef d ^+ rscalp p d)%:P.
End ComRegDivisor.
@@ -426,57 +425,57 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R : ringType.
-Implicit Types p q r : {poly R}.
+Implicit Types p q r : {poly R}.
-Variable d : {poly R}.
-Hypothesis mond : d \is monic.
+Variable d : {poly R}.
+Hypothesis mond : d \is monic.
-Lemma redivp_eq q r : size r < size d →
- let k := (redivp (q × d + r) d).1.1 in
- redivp (q × d + r) d = (k, q, r).
+Lemma redivp_eq q r : size r < size d →
+ let k := (redivp (q × d + r) d).1.1 in
+ redivp (q × d + r) d = (k, q, r).
Lemma rdivp_eq p :
- p = (rdivp p d) × d + (rmodp p d).
+ p = (rdivp p d) × d + (rmodp p d).
-Lemma rdivpp : rdivp d d = 1.
+Lemma rdivpp : rdivp d d = 1.
Lemma rdivp_addl_mul_small q r :
- size r < size d → rdivp (q × d + r) d = q.
+ size r < size d → rdivp (q × d + r) d = q.
-Lemma rdivp_addl_mul q r : rdivp (q × d + r) d = q + rdivp r d.
+Lemma rdivp_addl_mul q r : rdivp (q × d + r) d = q + rdivp r d.
Lemma rdivp_addl q r :
- rdvdp d q → rdivp (q + r) d = rdivp q d + rdivp r d.
+ rdvdp d q → rdivp (q + r) d = rdivp q d + rdivp r d.
Lemma rdivp_addr q r :
- rdvdp d r → rdivp (q + r) d = rdivp q d + rdivp r d.
+ rdvdp d r → rdivp (q + r) d = rdivp q d + rdivp r d.
-Lemma rdivp_mull p : rdivp (p × d) d = p.
+Lemma rdivp_mull p : rdivp (p × d) d = p.
-Lemma rmodp_mull p : rmodp (p × d) d = 0.
+Lemma rmodp_mull p : rmodp (p × d) d = 0.
-Lemma rmodpp : rmodp d d = 0.
+Lemma rmodpp : rmodp d d = 0.
Lemma rmodp_addl_mul_small q r :
- size r < size d → rmodp (q × d + r) d = r.
+ size r < size d → rmodp (q × d + r) d = r.
-Lemma rmodp_add p q : rmodp (p + q) d = rmodp p d + rmodp q d.
+Lemma rmodp_add p q : rmodp (p + q) d = rmodp p d + rmodp q d.
-Lemma rmodp_mulmr p q : rmodp (p × (rmodp q d)) d = rmodp (p × q) d.
+Lemma rmodp_mulmr p q : rmodp (p × (rmodp q d)) d = rmodp (p × q) d.
Lemma rdvdpp : rdvdp d d.
@@ -488,16 +487,16 @@ Definition rmultp := [rel m d | rdvdp d m].
section variables impose an inconvenient order on parameters
-
Lemma eq_rdvdp q1 p :
p = q1 × d → rdvdp d p.
+
Lemma eq_rdvdp q1 p :
p = q1 × d → rdvdp d p.
-
Lemma rdvdp_mull p :
rdvdp d (
p × d).
+
Lemma rdvdp_mull p :
rdvdp d (
p × d).
-
Lemma rdvdpP p :
reflect (
∃ qq, p = qq × d) (
rdvdp d p).
+
Lemma rdvdpP p :
reflect (
∃ qq, p = qq × d) (
rdvdp d p).
-
Lemma rdivpK p :
rdvdp d p → (rdivp p d) × d = p.
+
Lemma rdivpK p :
rdvdp d p → (rdivp p d) × d = p.
End MonicDivisor.
@@ -517,19 +516,19 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
ringType.
-
Implicit Types d p q r :
{poly R}.
+
Implicit Types d p q r :
{poly R}.
-
Lemma rdivp1 p :
rdivp p 1
= p.
+
Lemma rdivp1 p :
rdivp p 1
= p.
-
Lemma rdvdp_XsubCl p x :
rdvdp (
'X - x%:P)
p = root p x.
+
Lemma rdvdp_XsubCl p x :
rdvdp (
'X - x%:P)
p = root p x.
-
Lemma polyXsubCP p x :
reflect (
p.[x] = 0) (
rdvdp (
'X - x%:P)
p).
+
Lemma polyXsubCP p x :
reflect (
p.[x] = 0) (
rdvdp (
'X - x%:P)
p).
-
Lemma root_factor_theorem p x :
root p x = (rdvdp (
'X - x%:P)
p).
+
Lemma root_factor_theorem p x :
root p x = (rdvdp (
'X - x%:P)
p).
End ExtraMonicDivisor.
@@ -553,27 +552,27 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
comRingType.
-
Implicit Types d p q m n r :
{poly R}.
+
Implicit Types d p q m n r :
{poly R}.
-
CoInductive redivp_spec (
m d :
{poly R}) :
nat × {poly R} × {poly R} → Type :=
-
EdivnSpec k (
q r:
{poly R})
of
-
(lead_coef d ^+ k) *: m = q × d + r &
- (
d != 0
→ size r < size d) :
redivp_spec m d (k, q, r).
+
Variant redivp_spec (
m d :
{poly R}) :
nat × {poly R} × {poly R} → Type :=
+
EdivnSpec k (
q r:
{poly R})
of
+
(lead_coef d ^+ k) *: m = q × d + r &
+ (
d != 0
→ size r < size d) :
redivp_spec m d (k, q, r).
Lemma redivpP m d :
redivp_spec m d (
redivp m d).
Lemma rdivp_eq d p :
-
(lead_coef d ^+ (rscalp p d)) *: p = (rdivp p d) × d + (rmodp p d).
+
(lead_coef d ^+ (rscalp p d)) *: p = (rdivp p d) × d + (rmodp p d).
Lemma rdvdp_eqP d p :
rdvdp_spec p d (
rmodp p d) (
rdvdp d p).
Lemma rdvdp_eq q p :
-
(rdvdp q p) = ((lead_coef q) ^+ (rscalp p q) *: p == (rdivp p q) × q).
+
(rdvdp q p) = ((lead_coef q) ^+ (rscalp p q) *: p == (rdivp p q) × q).
End CommutativeRingPseudoDivision.
@@ -592,12 +591,12 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
unitRingType.
-
Implicit Type p q r d :
{poly R}.
+
Implicit Type p q r d :
{poly R}.
Lemma uniq_roots_rdvdp p rs :
-
all (
root p)
rs → uniq_roots rs →
-
rdvdp (
\prod_(z <- rs) ('X - z%:P))
p.
+
all (
root p)
rs → uniq_roots rs →
+
rdvdp (
\prod_(z <- rs) ('X - z%:P))
p.
End UnitRingPseudoDivision.
@@ -616,33 +615,33 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
idomainType.
-
Implicit Type p q r d :
{poly R}.
+
Implicit Type p q r d :
{poly R}.
Definition edivp_expanded_def p q :=
-
let:
(k, d, r) as edvpq :=
redivp p q in
-
if lead_coef q \in GRing.unit then
-
(0%
N, (lead_coef q)^-k *: d, (lead_coef q)^-k *: r)
-
else edvpq.
-
Fact edivp_key :
unit.
-
Definition edivp :=
locked_with edivp_key edivp_expanded_def.
-
Canonical edivp_unlockable :=
[unlockable fun edivp].
+
let:
(k, d, r) as edvpq :=
redivp p q in
+
if lead_coef q \in GRing.unit then
+
(0%
N, (lead_coef q)^-k *: d, (lead_coef q)^-k *: r)
+
else edvpq.
+
Fact edivp_key :
unit.
+
Definition edivp :=
locked_with edivp_key edivp_expanded_def.
+
Canonical edivp_unlockable :=
[unlockable fun edivp].
-
Definition divp p q :=
((edivp p q).1).2.
-
Definition modp p q :=
(edivp p q).2.
-
Definition scalp p q :=
((edivp p q).1).1.
-
Definition dvdp p q :=
modp q p == 0.
-
Definition eqp p q :=
(dvdp p q) && (dvdp q p).
+
Definition divp p q :=
((edivp p q).1).2.
+
Definition modp p q :=
(edivp p q).2.
+
Definition scalp p q :=
((edivp p q).1).1.
+
Definition dvdp p q :=
modp q p == 0.
+
Definition eqp p q :=
(dvdp p q) && (dvdp q p).
End IDomainPseudoDivisionDefs.
-
Notation "m %/ d" := (
divp m d) :
ring_scope.
-
Notation "m %% d" := (
modp m d) :
ring_scope.
-
Notation "p %| q" := (
dvdp p q) :
ring_scope.
-
Notation "p %= q" := (
eqp p q) :
ring_scope.
+
Notation "m %/ d" := (
divp m d) :
ring_scope.
+
Notation "m %% d" := (
modp m d) :
ring_scope.
+
Notation "p %| q" := (
dvdp p q) :
ring_scope.
+
Notation "p %= q" := (
eqp p q) :
ring_scope.
End IdomainDefs.
@@ -656,48 +655,48 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
idomainType.
-
Implicit Type p q r d :
{poly R}.
+
Implicit Type p q r d :
{poly R}.
-
Lemma edivp_def p q :
edivp p q = (scalp p q, divp p q, modp p q).
+
Lemma edivp_def p q :
edivp p q = (scalp p q, divp p q, modp p q).
-
Lemma edivp_redivp p q :
(lead_coef q \in GRing.unit) = false →
-
edivp p q = redivp p q.
+
Lemma edivp_redivp p q :
(lead_coef q \in GRing.unit) = false →
+
edivp p q = redivp p q.
Lemma divpE p q :
-
p %/ q = if lead_coef q \in GRing.unit
-
then (lead_coef q)^-(rscalp p q) *: (rdivp p q)
-
else rdivp p q.
+
p %/ q = if lead_coef q \in GRing.unit
+
then (lead_coef q)^-(rscalp p q) *: (rdivp p q)
+
else rdivp p q.
Lemma modpE p q :
-
p %% q = if lead_coef q \in GRing.unit
-
then (lead_coef q)^-(rscalp p q) *: (rmodp p q)
-
else rmodp p q.
+
p %% q = if lead_coef q \in GRing.unit
+
then (lead_coef q)^-(rscalp p q) *: (rmodp p q)
+
else rmodp p q.
Lemma scalpE p q :
-
scalp p q = if lead_coef q \in GRing.unit then 0%
N else rscalp p q.
+
scalp p q = if lead_coef q \in GRing.unit then 0%
N else rscalp p q.
-
Lemma dvdpE p q :
p %| q = rdvdp p q.
+
Lemma dvdpE p q :
p %| q = rdvdp p q.
-
Lemma lc_expn_scalp_neq0 p q :
lead_coef q ^+ scalp p q != 0.
+
Lemma lc_expn_scalp_neq0 p q :
lead_coef q ^+ scalp p q != 0.
-
Hint Resolve lc_expn_scalp_neq0.
+
Hint Resolve lc_expn_scalp_neq0 :
core.
-
CoInductive edivp_spec (
m d :
{poly R}) :
-
nat × {poly R} × {poly R} → bool → Type :=
-|
Redivp_spec k (
q r:
{poly R})
of
-
(lead_coef d ^+ k) *: m = q × d + r &
lead_coef d \notin GRing.unit &
- (
d != 0
→ size r < size d) :
edivp_spec m d (k, q, r) false
-|
Fedivp_spec (
q r:
{poly R})
of m = q × d + r & (
lead_coef d \in GRing.unit) &
- (
d != 0
→ size r < size d) :
edivp_spec m d (0%
N, q, r) true.
+
Variant edivp_spec (
m d :
{poly R}) :
+
nat × {poly R} × {poly R} → bool → Type :=
+|
Redivp_spec k (
q r:
{poly R})
of
+
(lead_coef d ^+ k) *: m = q × d + r &
lead_coef d \notin GRing.unit &
+ (
d != 0
→ size r < size d) :
edivp_spec m d (k, q, r) false
+|
Fedivp_spec (
q r:
{poly R})
of m = q × d + r & (
lead_coef d \in GRing.unit) &
+ (
d != 0
→ size r < size d) :
edivp_spec m d (0%
N, q, r) true.
-
Lemma edivpP m d :
edivp_spec m d (
edivp m d) (
lead_coef d \in GRing.unit).
+
Lemma edivpP m d :
edivp_spec m d (
edivp m d) (
lead_coef d \in GRing.unit).
-
Lemma edivp_eq d q r :
size r < size d → lead_coef d \in GRing.unit →
-
edivp (
q × d + r)
d = (0%
N, q, r).
+
Lemma edivp_eq d q r :
size r < size d → lead_coef d \in GRing.unit →
+
edivp (
q × d + r)
d = (0%
N, q, r).
Lemma divp_eq p q :
-
(lead_coef q ^+ (scalp p q)) *: p = (p %/ q) × q + (p %% q).
+
(lead_coef q ^+ (scalp p q)) *: p = (p %/ q) × q + (p %% q).
Lemma dvdp_eq q p :
-
(q %| p) = ((lead_coef q) ^+ (scalp p q) *: p == (p %/ q) × q).
+
(q %| p) = ((lead_coef q) ^+ (scalp p q) *: p == (p %/ q) × q).
-
Lemma divpK d p :
d %| p → p %/ d × d = ((lead_coef d) ^+ (scalp p d)) *: p.
+
Lemma divpK d p :
d %| p → p %/ d × d = ((lead_coef d) ^+ (scalp p d)) *: p.
-
Lemma divpKC d p :
d %| p → d × (p %/ d) = ((lead_coef d) ^+ (scalp p d)) *: p.
+
Lemma divpKC d p :
d %| p → d × (p %/ d) = ((lead_coef d) ^+ (scalp p d)) *: p.
Lemma dvdpP q p :
-
reflect (
exists2 cqq, cqq.1 != 0
& cqq.1 *: p = cqq.2 × q) (
q %| p).
+
reflect (
exists2 cqq, cqq.1 != 0
& cqq.1 *: p = cqq.2 × q) (
q %| p).
-
Lemma mulpK p q :
q != 0
→
-
p × q %/ q = lead_coef q ^+ scalp (
p × q)
q *: p.
+
Lemma mulpK p q :
q != 0
→
+
p × q %/ q = lead_coef q ^+ scalp (
p × q)
q *: p.
-
Lemma mulKp p q :
q != 0
→
-
q × p %/ q = lead_coef q ^+ scalp (
p × q)
q *: p.
+
Lemma mulKp p q :
q != 0
→
+
q × p %/ q = lead_coef q ^+ scalp (
p × q)
q *: p.
-
Lemma divpp p :
p != 0
→ p %/ p = (lead_coef p ^+ scalp p p)%:P.
+
Lemma divpp p :
p != 0
→ p %/ p = (lead_coef p ^+ scalp p p)%:P.
End WeakTheoryForIDomainPseudoDivision.
-
Hint Resolve lc_expn_scalp_neq0.
+
Hint Resolve lc_expn_scalp_neq0 :
core.
End WeakIdomain.
@@ -762,460 +761,460 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
idomainType.
-
Implicit Type p q r d m n :
{poly R}.
+
Implicit Type p q r d m n :
{poly R}.
-
Lemma scalp0 p :
scalp p 0
= 0%
N.
+
Lemma scalp0 p :
scalp p 0
= 0%
N.
-
Lemma divp_small p q :
size p < size q → p %/ q = 0.
+
Lemma divp_small p q :
size p < size q → p %/ q = 0.
-
Lemma leq_divp p q : (
size (
p %/ q)
≤ size p).
+
Lemma leq_divp p q : (
size (
p %/ q)
≤ size p).
-
Lemma div0p p : 0
%/ p = 0.
+
Lemma div0p p : 0
%/ p = 0.
-
Lemma divp0 p :
p %/ 0
= 0.
+
Lemma divp0 p :
p %/ 0
= 0.
-
Lemma divp1 m :
m %/ 1
= m.
+
Lemma divp1 m :
m %/ 1
= m.
-
Lemma modp0 p :
p %% 0
= p.
+
Lemma modp0 p :
p %% 0
= p.
-
Lemma mod0p p : 0
%% p = 0.
+
Lemma mod0p p : 0
%% p = 0.
-
Lemma modp1 p :
p %% 1
= 0.
+
Lemma modp1 p :
p %% 1
= 0.
-
Hint Resolve divp0 divp1 mod0p modp0 modp1.
+
Hint Resolve divp0 divp1 mod0p modp0 modp1 :
core.
-
Lemma modp_small p q :
size p < size q → p %% q = p.
+
Lemma modp_small p q :
size p < size q → p %% q = p.
-
Lemma modpC p c :
c != 0
→ p %% c%:P = 0.
+
Lemma modpC p c :
c != 0
→ p %% c%:P = 0.
-
Lemma modp_mull p q :
(p × q) %% q = 0.
+
Lemma modp_mull p q :
(p × q) %% q = 0.
-
Lemma modp_mulr d p :
(d × p) %% d = 0.
+
Lemma modp_mulr d p :
(d × p) %% d = 0.
-
Lemma modpp d :
d %% d = 0.
+
Lemma modpp d :
d %% d = 0.
-
Lemma ltn_modp p q :
(size (
p %% q)
< size q) = (q != 0
).
+
Lemma ltn_modp p q :
(size (
p %% q)
< size q) = (q != 0
).
-
Lemma ltn_divpl d q p :
d != 0
→
-
(size (
q %/ d)
< size p) = (size q < size (
p × d)
).
+
Lemma ltn_divpl d q p :
d != 0
→
+
(size (
q %/ d)
< size p) = (size q < size (
p × d)
).
-
Lemma leq_divpr d p q :
d != 0
→
-
(size p ≤ size (
q %/ d)
) = (size (
p × d)
≤ size q).
+
Lemma leq_divpr d p q :
d != 0
→
+
(size p ≤ size (
q %/ d)
) = (size (
p × d)
≤ size q).
-
Lemma divpN0 d p :
d != 0
→ (p %/ d != 0
) = (size d ≤ size p).
+
Lemma divpN0 d p :
d != 0
→ (p %/ d != 0
) = (size d ≤ size p).
-
Lemma size_divp p q :
q != 0
→ size (
p %/ q)
= (
(size p) - (size q).-1)%
N.
+
Lemma size_divp p q :
q != 0
→ size (
p %/ q)
= (
(size p) - (size q).-1)%
N.
-
Lemma ltn_modpN0 p q :
q != 0
→ size (
p %% q)
< size q.
+
Lemma ltn_modpN0 p q :
q != 0
→ size (
p %% q)
< size q.
-
Lemma modp_mod p q :
(p %% q) %% q = p %% q.
+
Lemma modp_mod p q :
(p %% q) %% q = p %% q.
-
Lemma leq_modp m d :
size (
m %% d)
≤ size m.
+
Lemma leq_modp m d :
size (
m %% d)
≤ size m.
-
Lemma dvdp0 d :
d %| 0.
+
Lemma dvdp0 d :
d %| 0.
-
Hint Resolve dvdp0.
+
Hint Resolve dvdp0 :
core.
-
Lemma dvd0p p :
(0
%| p) = (p == 0
).
+
Lemma dvd0p p :
(0
%| p) = (p == 0
).
-
Lemma dvd0pP p :
reflect (
p = 0) (0
%| p).
+
Lemma dvd0pP p :
reflect (
p = 0) (0
%| p).
-
Lemma dvdpN0 p q :
p %| q → q != 0
→ p != 0.
+
Lemma dvdpN0 p q :
p %| q → q != 0
→ p != 0.
-
Lemma dvdp1 d :
(d %| 1
) = ((size d) == 1%
N).
+
Lemma dvdp1 d :
(d %| 1
) = ((size d) == 1%
N).
-
Lemma dvd1p m : 1
%| m.
+
Lemma dvd1p m : 1
%| m.
-
Lemma gtNdvdp p q :
p != 0
→ size p < size q → (q %| p) = false.
+
Lemma gtNdvdp p q :
p != 0
→ size p < size q → (q %| p) = false.
-
Lemma modp_eq0P p q :
reflect (
p %% q = 0) (
q %| p).
+
Lemma modp_eq0P p q :
reflect (
p %% q = 0) (
q %| p).
-
Lemma modp_eq0 p q :
(q %| p) → p %% q = 0.
+
Lemma modp_eq0 p q :
(q %| p) → p %% q = 0.
Lemma leq_divpl d p q :
-
d %| p → (size (
p %/ d)
≤ size q) = (size p ≤ size (
q × d)
).
+
d %| p → (size (
p %/ d)
≤ size q) = (size p ≤ size (
q × d)
).
-
Lemma dvdp_leq p q :
q != 0
→ p %| q → size p ≤ size q.
+
Lemma dvdp_leq p q :
q != 0
→ p %| q → size p ≤ size q.
-
Lemma eq_dvdp c quo q p :
c != 0
→ c *: p = quo × q → q %| p.
+
Lemma eq_dvdp c quo q p :
c != 0
→ c *: p = quo × q → q %| p.
-
Lemma dvdpp d :
d %| d.
+
Lemma dvdpp d :
d %| d.
-
Hint Resolve dvdpp.
+
Hint Resolve dvdpp :
core.
-
Lemma divp_dvd p q :
(p %| q) → ((q %/ p) %| q).
+
Lemma divp_dvd p q :
(p %| q) → ((q %/ p) %| q).
-
Lemma dvdp_mull m d n :
d %| n → d %| m × n.
+
Lemma dvdp_mull m d n :
d %| n → d %| m × n.
-
Lemma dvdp_mulr n d m :
d %| m → d %| m × n.
+
Lemma dvdp_mulr n d m :
d %| m → d %| m × n.
-
Hint Resolve dvdp_mull dvdp_mulr.
+
Hint Resolve dvdp_mull dvdp_mulr :
core.
-
Lemma dvdp_mul d1 d2 m1 m2 :
d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2.
+
Lemma dvdp_mul d1 d2 m1 m2 :
d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2.
-
Lemma dvdp_addr m d n :
d %| m → (d %| m + n) = (d %| n).
+
Lemma dvdp_addr m d n :
d %| m → (d %| m + n) = (d %| n).
-
Lemma dvdp_addl n d m :
d %| n → (d %| m + n) = (d %| m).
+
Lemma dvdp_addl n d m :
d %| n → (d %| m + n) = (d %| m).
-
Lemma dvdp_add d m n :
d %| m → d %| n → d %| m + n.
+
Lemma dvdp_add d m n :
d %| m → d %| n → d %| m + n.
-
Lemma dvdp_add_eq d m n :
d %| m + n → (d %| m) = (d %| n).
+
Lemma dvdp_add_eq d m n :
d %| m + n → (d %| m) = (d %| n).
-
Lemma dvdp_subr d m n :
d %| m → (d %| m - n) = (d %| n).
+
Lemma dvdp_subr d m n :
d %| m → (d %| m - n) = (d %| n).
-
Lemma dvdp_subl d m n :
d %| n → (d %| m - n) = (d %| m).
+
Lemma dvdp_subl d m n :
d %| n → (d %| m - n) = (d %| m).
-
Lemma dvdp_sub d m n :
d %| m → d %| n → d %| m - n.
+
Lemma dvdp_sub d m n :
d %| m → d %| n → d %| m - n.
-
Lemma dvdp_mod d n m :
d %| n → (d %| m) = (d %| m %% n).
+
Lemma dvdp_mod d n m :
d %| n → (d %| m) = (d %| m %% n).
-
Lemma dvdp_trans :
transitive (@
dvdp R).
+
Lemma dvdp_trans :
transitive (@
dvdp R).
-
Lemma dvdp_mulIl p q :
p %| p × q.
+
Lemma dvdp_mulIl p q :
p %| p × q.
-
Lemma dvdp_mulIr p q :
q %| p × q.
+
Lemma dvdp_mulIr p q :
q %| p × q.
-
Lemma dvdp_mul2r r p q :
r != 0
→ (p × r %| q × r) = (p %| q).
+
Lemma dvdp_mul2r r p q :
r != 0
→ (p × r %| q × r) = (p %| q).
-
Lemma dvdp_mul2l r p q:
r != 0
→ (r × p %| r × q) = (p %| q).
+
Lemma dvdp_mul2l r p q:
r != 0
→ (r × p %| r × q) = (p %| q).
Lemma ltn_divpr d p q :
-
d %| q → (size p < size (
q %/ d)
) = (size (
p × d)
< size q).
+
d %| q → (size p < size (
q %/ d)
) = (size (
p × d)
< size q).
-
Lemma dvdp_exp d k p : 0
< k → d %| p → d %| (p ^+ k).
+
Lemma dvdp_exp d k p : 0
< k → d %| p → d %| (p ^+ k).
-
Lemma dvdp_exp2l d k l :
k ≤ l → d ^+ k %| d ^+ l.
+
Lemma dvdp_exp2l d k l :
k ≤ l → d ^+ k %| d ^+ l.
-
Lemma dvdp_Pexp2l d k l : 1
< size d → (d ^+ k %| d ^+ l) = (k ≤ l).
+
Lemma dvdp_Pexp2l d k l : 1
< size d → (d ^+ k %| d ^+ l) = (k ≤ l).
-
Lemma dvdp_exp2r p q k :
p %| q → p ^+ k %| q ^+ k.
+
Lemma dvdp_exp2r p q k :
p %| q → p ^+ k %| q ^+ k.
-
Lemma dvdp_exp_sub p q k l:
p != 0
→
-
(p ^+ k %| q × p ^+ l) = (p ^+ (k - l) %| q).
+
Lemma dvdp_exp_sub p q k l:
p != 0
→
+
(p ^+ k %| q × p ^+ l) = (p ^+ (k - l) %| q).
-
Lemma dvdp_XsubCl p x :
('X - x%:P) %| p = root p x.
+
Lemma dvdp_XsubCl p x :
('X - x%:P) %| p = root p x.
-
Lemma polyXsubCP p x :
reflect (
p.[x] = 0) (
('X - x%:P) %| p).
+
Lemma polyXsubCP p x :
reflect (
p.[x] = 0) (
('X - x%:P) %| p).
Lemma eqp_div_XsubC p c :
-
(p == (p %/ ('X - c%:P)) × ('X - c%:P)) = ('X - c%:P %| p).
+
(p == (p %/ ('X - c%:P)) × ('X - c%:P)) = ('X - c%:P %| p).
-
Lemma root_factor_theorem p x :
root p x = (('X - x%:P) %| p).
+
Lemma root_factor_theorem p x :
root p x = (('X - x%:P) %| p).
-
Lemma uniq_roots_dvdp p rs :
all (
root p)
rs → uniq_roots rs →
-
(\prod_(z <- rs) ('X - z%:P)) %| p.
+
Lemma uniq_roots_dvdp p rs :
all (
root p)
rs → uniq_roots rs →
+
(\prod_(z <- rs) ('X - z%:P)) %| p.
-
Lemma root_bigmul :
∀ x (
ps :
seq {poly R}),
-
~~root (
\big[*%R/1
]_(p <- ps) p)
x = all (
fun p ⇒
~~ root p x)
ps.
+
Lemma root_bigmul :
∀ x (
ps :
seq {poly R}),
+
~~root (
\big[*%R/1
]_(p <- ps) p)
x = all (
fun p ⇒
~~ root p x)
ps.
Lemma eqpP m n :
-
reflect (
exists2 c12, (c12.1 != 0
) && (c12.2 != 0
) & c12.1 *: m = c12.2 *: n)
- (
m %= n).
+
reflect (
exists2 c12, (c12.1 != 0
) && (c12.2 != 0
) & c12.1 *: m = c12.2 *: n)
+ (
m %= n).
-
Lemma eqp_eq p q:
p %= q → (lead_coef q) *: p = (lead_coef p) *: q.
+
Lemma eqp_eq p q:
p %= q → (lead_coef q) *: p = (lead_coef p) *: q.
-
Lemma eqpxx :
reflexive (@
eqp R).
+
Lemma eqpxx :
reflexive (@
eqp R).
-
Hint Resolve eqpxx.
+
Hint Resolve eqpxx :
core.
-
Lemma eqp_sym :
symmetric (@
eqp R).
+
Lemma eqp_sym :
symmetric (@
eqp R).
-
Lemma eqp_trans :
transitive (@
eqp R).
+
Lemma eqp_trans :
transitive (@
eqp R).
-
Lemma eqp_ltrans :
left_transitive (@
eqp R).
+
Lemma eqp_ltrans :
left_transitive (@
eqp R).
-
Lemma eqp_rtrans :
right_transitive (@
eqp R).
+
Lemma eqp_rtrans :
right_transitive (@
eqp R).
-
Lemma eqp0 :
∀ p,
(p %= 0
) = (p == 0
).
+
Lemma eqp0 :
∀ p,
(p %= 0
) = (p == 0
).
-
Lemma eqp01 : 0
%= (1
: {poly R}) = false.
+
Lemma eqp01 : 0
%= (1
: {poly R}) = false.
-
Lemma eqp_scale p c :
c != 0
→ c *: p %= p.
+
Lemma eqp_scale p c :
c != 0
→ c *: p %= p.
-
Lemma eqp_size p q :
p %= q → size p = size q.
+
Lemma eqp_size p q :
p %= q → size p = size q.
-
Lemma size_poly_eq1 p :
(size p == 1%
N) = (p %= 1
).
+
Lemma size_poly_eq1 p :
(size p == 1%
N) = (p %= 1
).
-
Lemma polyXsubC_eqp1 (
x :
R) :
('X - x%:P %= 1
) = false.
+
Lemma polyXsubC_eqp1 (
x :
R) :
('X - x%:P %= 1
) = false.
-
Lemma dvdp_eqp1 p q :
p %| q → q %= 1
→ p %= 1.
+
Lemma dvdp_eqp1 p q :
p %| q → q %= 1
→ p %= 1.
-
Lemma eqp_dvdr q p d:
p %= q → d %| p = (d %| q).
+
Lemma eqp_dvdr q p d:
p %= q → d %| p = (d %| q).
-
Lemma eqp_dvdl d2 d1 p :
d1 %= d2 → d1 %| p = (d2 %| p).
+
Lemma eqp_dvdl d2 d1 p :
d1 %= d2 → d1 %| p = (d2 %| p).
-
Lemma dvdp_scaler c m n :
c != 0
→ m %| c *: n = (m %| n).
+
Lemma dvdp_scaler c m n :
c != 0
→ m %| c *: n = (m %| n).
-
Lemma dvdp_scalel c m n :
c != 0
→ (c *: m %| n) = (m %| n).
+
Lemma dvdp_scalel c m n :
c != 0
→ (c *: m %| n) = (m %| n).
-
Lemma dvdp_opp d p :
d %| (- p) = (d %| p).
+
Lemma dvdp_opp d p :
d %| (- p) = (d %| p).
-
Lemma eqp_mul2r r p q :
r != 0
→ (p × r %= q × r) = (p %= q).
+
Lemma eqp_mul2r r p q :
r != 0
→ (p × r %= q × r) = (p %= q).
-
Lemma eqp_mul2l r p q:
r != 0
→ (r × p %= r × q) = (p %= q).
+
Lemma eqp_mul2l r p q:
r != 0
→ (r × p %= r × q) = (p %= q).
-
Lemma eqp_mull r p q:
(q %= r) → (p × q %= p × r).
+
Lemma eqp_mull r p q:
(q %= r) → (p × q %= p × r).
-
Lemma eqp_mulr q p r :
(p %= q) → (p × r %= q × r).
+
Lemma eqp_mulr q p r :
(p %= q) → (p × r %= q × r).
-
Lemma eqp_exp p q k :
p %= q → p ^+ k %= q ^+ k.
+
Lemma eqp_exp p q k :
p %= q → p ^+ k %= q ^+ k.
-
Lemma polyC_eqp1 (
c :
R) :
(c%:P %= 1
) = (c != 0
).
+
Lemma polyC_eqp1 (
c :
R) :
(c%:P %= 1
) = (c != 0
).
-
Lemma dvdUp d p:
d %= 1
→ d %| p.
+
Lemma dvdUp d p:
d %= 1
→ d %| p.
-
Lemma dvdp_size_eqp p q :
p %| q → size p == size q = (p %= q).
+
Lemma dvdp_size_eqp p q :
p %| q → size p == size q = (p %= q).
-
Lemma eqp_root p q :
p %= q → root p =1 root q.
+
Lemma eqp_root p q :
p %= q → root p =1 root q.
-
Lemma eqp_rmod_mod p q :
rmodp p q %= modp p q.
+
Lemma eqp_rmod_mod p q :
rmodp p q %= modp p q.
-
Lemma eqp_rdiv_div p q :
rdivp p q %= divp p q.
+
Lemma eqp_rdiv_div p q :
rdivp p q %= divp p q.
-
Lemma dvd_eqp_divl d p q (
dvd_dp :
d %| q) (
eq_pq :
p %= q) :
-
p %/ d %= q %/ d.
+
Lemma dvd_eqp_divl d p q (
dvd_dp :
d %| q) (
eq_pq :
p %= q) :
+
p %/ d %= q %/ d.
Definition gcdp_rec p q :=
-
let:
(p1, q1) :=
if size p < size q then (q, p) else (p, q) in
-
if p1 == 0
then q1 else
-
let fix loop (
n :
nat) (
pp qq :
{poly R}) {
struct n} :=
+
let:
(p1, q1) :=
if size p < size q then (q, p) else (p, q) in
+
if p1 == 0
then q1 else
+
let fix loop (
n :
nat) (
pp qq :
{poly R}) {
struct n} :=
let rr :=
modp pp qq in
-
if rr == 0
then qq else
-
if n is n1.+1 then loop n1 qq rr else rr in
+
if rr == 0
then qq else
+
if n is n1.+1 then loop n1 qq rr else rr in
loop (
size p1)
p1 q1.
-
Definition gcdp :=
nosimpl gcdp_rec.
+
Definition gcdp :=
nosimpl gcdp_rec.
-
Lemma gcd0p :
left_id 0
gcdp.
+
Lemma gcd0p :
left_id 0
gcdp.
-
Lemma gcdp0 :
right_id 0
gcdp.
+
Lemma gcdp0 :
right_id 0
gcdp.
Lemma gcdpE p q :
-
gcdp p q = if size p < size q
-
then gcdp (
modp q p)
p else gcdp (
modp p q)
q.
+
gcdp p q = if size p < size q
+
then gcdp (
modp q p)
p else gcdp (
modp p q)
q.
-
Lemma size_gcd1p p :
size (
gcdp 1
p)
= 1%
N.
+
Lemma size_gcd1p p :
size (
gcdp 1
p)
= 1%
N.
-
Lemma size_gcdp1 p :
size (
gcdp p 1)
= 1%
N.
+
Lemma size_gcdp1 p :
size (
gcdp p 1)
= 1%
N.
-
Lemma gcdpp :
idempotent gcdp.
+
Lemma gcdpp :
idempotent gcdp.
-
Lemma dvdp_gcdlr p q :
(gcdp p q %| p) && (gcdp p q %| q).
+
Lemma dvdp_gcdlr p q :
(gcdp p q %| p) && (gcdp p q %| q).
-
Lemma dvdp_gcdl p q :
gcdp p q %| p.
+
Lemma dvdp_gcdl p q :
gcdp p q %| p.
-
Lemma dvdp_gcdr p q :
gcdp p q %| q.
+
Lemma dvdp_gcdr p q :
gcdp p q %| q.
-
Lemma leq_gcdpl p q :
p != 0
→ size (
gcdp p q)
≤ size p.
+
Lemma leq_gcdpl p q :
p != 0
→ size (
gcdp p q)
≤ size p.
-
Lemma leq_gcdpr p q :
q != 0
→ size (
gcdp p q)
≤ size q.
+
Lemma leq_gcdpr p q :
q != 0
→ size (
gcdp p q)
≤ size q.
-
Lemma dvdp_gcd p m n :
p %| gcdp m n = (p %| m) && (p %| n).
+
Lemma dvdp_gcd p m n :
p %| gcdp m n = (p %| m) && (p %| n).
-
Lemma gcdpC :
∀ p q,
gcdp p q %= gcdp q p.
+
Lemma gcdpC :
∀ p q,
gcdp p q %= gcdp q p.
-
Lemma gcd1p p :
gcdp 1
p %= 1.
+
Lemma gcd1p p :
gcdp 1
p %= 1.
-
Lemma gcdp1 p :
gcdp p 1
%= 1.
+
Lemma gcdp1 p :
gcdp p 1
%= 1.
-
Lemma gcdp_addl_mul p q r:
gcdp r (
p × r + q)
%= gcdp r q.
+
Lemma gcdp_addl_mul p q r:
gcdp r (
p × r + q)
%= gcdp r q.
-
Lemma gcdp_addl m n :
gcdp m (
m + n)
%= gcdp m n.
+
Lemma gcdp_addl m n :
gcdp m (
m + n)
%= gcdp m n.
-
Lemma gcdp_addr m n :
gcdp m (
n + m)
%= gcdp m n.
+
Lemma gcdp_addr m n :
gcdp m (
n + m)
%= gcdp m n.
-
Lemma gcdp_mull m n :
gcdp n (
m × n)
%= n.
+
Lemma gcdp_mull m n :
gcdp n (
m × n)
%= n.
-
Lemma gcdp_mulr m n :
gcdp n (
n × m)
%= n.
+
Lemma gcdp_mulr m n :
gcdp n (
n × m)
%= n.
-
Lemma gcdp_scalel c m n :
c != 0
→ gcdp (
c *: m)
n %= gcdp m n.
+
Lemma gcdp_scalel c m n :
c != 0
→ gcdp (
c *: m)
n %= gcdp m n.
-
Lemma gcdp_scaler c m n :
c != 0
→ gcdp m (
c *: n)
%= gcdp m n.
+
Lemma gcdp_scaler c m n :
c != 0
→ gcdp m (
c *: n)
%= gcdp m n.
-
Lemma dvdp_gcd_idl m n :
m %| n → gcdp m n %= m.
+
Lemma dvdp_gcd_idl m n :
m %| n → gcdp m n %= m.
-
Lemma dvdp_gcd_idr m n :
n %| m → gcdp m n %= n.
+
Lemma dvdp_gcd_idr m n :
n %| m → gcdp m n %= n.
-
Lemma gcdp_exp p k l :
gcdp (
p ^+ k) (
p ^+ l)
%= p ^+ minn k l.
+
Lemma gcdp_exp p k l :
gcdp (
p ^+ k) (
p ^+ l)
%= p ^+ minn k l.
-
Lemma gcdp_eq0 p q :
gcdp p q == 0
= (p == 0
) && (q == 0
).
+
Lemma gcdp_eq0 p q :
gcdp p q == 0
= (p == 0
) && (q == 0
).
-
Lemma eqp_gcdr p q r :
q %= r → gcdp p q %= gcdp p r.
+
Lemma eqp_gcdr p q r :
q %= r → gcdp p q %= gcdp p r.
-
Lemma eqp_gcdl r p q :
p %= q → gcdp p r %= gcdp q r.
+
Lemma eqp_gcdl r p q :
p %= q → gcdp p r %= gcdp q r.
-
Lemma eqp_gcd p1 p2 q1 q2 :
p1 %= p2 → q1 %= q2 → gcdp p1 q1 %= gcdp p2 q2.
+
Lemma eqp_gcd p1 p2 q1 q2 :
p1 %= p2 → q1 %= q2 → gcdp p1 q1 %= gcdp p2 q2.
-
Lemma eqp_rgcd_gcd p q :
rgcdp p q %= gcdp p q.
+
Lemma eqp_rgcd_gcd p q :
rgcdp p q %= gcdp p q.
-
Lemma gcdp_modr m n :
gcdp m (
n %% m)
%= gcdp m n.
+
Lemma gcdp_modr m n :
gcdp m (
n %% m)
%= gcdp m n.
-
Lemma gcdp_modl m n :
gcdp (
m %% n)
n %= gcdp m n.
+
Lemma gcdp_modl m n :
gcdp (
m %% n)
n %= gcdp m n.
Lemma gcdp_def d m n :
-
d %| m → d %| n → (∀ d',
d' %| m → d' %| n → d' %| d) →
-
gcdp m n %= d.
+
d %| m → d %| n → (∀ d',
d' %| m → d' %| n → d' %| d) →
+
gcdp m n %= d.
-
Definition coprimep p q :=
size (
gcdp p q)
== 1%
N.
+
Definition coprimep p q :=
size (
gcdp p q)
== 1%
N.
-
Lemma coprimep_size_gcd p q :
coprimep p q → size (
gcdp p q)
= 1%
N.
+
Lemma coprimep_size_gcd p q :
coprimep p q → size (
gcdp p q)
= 1%
N.
-
Lemma coprimep_def p q :
(coprimep p q) = (size (
gcdp p q)
== 1%
N).
+
Lemma coprimep_def p q :
(coprimep p q) = (size (
gcdp p q)
== 1%
N).
Lemma coprimep_scalel c m n :
-
c != 0
→ coprimep (
c *: m)
n = coprimep m n.
+
c != 0
→ coprimep (
c *: m)
n = coprimep m n.
Lemma coprimep_scaler c m n:
-
c != 0
→ coprimep m (
c *: n)
= coprimep m n.
+
c != 0
→ coprimep m (
c *: n)
= coprimep m n.
-
Lemma coprimepp p :
coprimep p p = (size p == 1%
N).
+
Lemma coprimepp p :
coprimep p p = (size p == 1%
N).
-
Lemma gcdp_eqp1 p q :
gcdp p q %= 1
= (coprimep p q).
+
Lemma gcdp_eqp1 p q :
gcdp p q %= 1
= (coprimep p q).
-
Lemma coprimep_sym p q :
coprimep p q = coprimep q p.
+
Lemma coprimep_sym p q :
coprimep p q = coprimep q p.
Lemma coprime1p p :
coprimep 1
p.
@@ -1224,10 +1223,10 @@ Definition rmultp := [rel m d | rdvdp d m].
Lemma coprimep1 p :
coprimep p 1.
-
Lemma coprimep0 p :
coprimep p 0
= (p %= 1
).
+
Lemma coprimep0 p :
coprimep p 0
= (p %= 1
).
-
Lemma coprime0p p :
coprimep 0
p = (p %= 1
).
+
Lemma coprime0p p :
coprimep 0
p = (p %= 1
).
-
Fixpoint egcdp_rec p q k {
struct k} :
{poly R} × {poly R} :=
-
if k is k'.+1 then
-
if q == 0
then (1
, 0
) else
-
let:
(u, v) :=
egcdp_rec q (
p %% q)
k' in
-
(lead_coef q ^+ scalp p q *: v, (u - v × (p %/ q)))
-
else (1
, 0
).
+
Fixpoint egcdp_rec p q k {
struct k} :
{poly R} × {poly R} :=
+
if k is k'.+1 then
+
if q == 0
then (1
, 0
) else
+
let:
(u, v) :=
egcdp_rec q (
p %% q)
k' in
+
(lead_coef q ^+ scalp p q *: v, (u - v × (p %/ q)))
+
else (1
, 0
).
Definition egcdp p q :=
-
if size q ≤ size p then egcdp_rec p q (
size q)
-
else let e :=
egcdp_rec q p (
size p)
in (e.2, e.1).
+
if size q ≤ size p then egcdp_rec p q (
size q)
+
else let e :=
egcdp_rec q p (
size p)
in (e.2, e.1).
-
Lemma egcdp0 p :
egcdp p 0
= (1
, 0
).
+
Lemma egcdp0 p :
egcdp p 0
= (1
, 0
).
-
Lemma egcdp_recP :
∀ k p q,
q != 0
→ size q ≤ k → size q ≤ size p →
+
Lemma egcdp_recP :
∀ k p q,
q != 0
→ size q ≤ k → size q ≤ size p →
let e := (
egcdp_rec p q k)
in
-
[/\ size e.1 ≤ size q, size e.2 ≤ size p & gcdp p q %= e.1 × p + e.2 × q].
+
[/\ size e.1 ≤ size q, size e.2 ≤ size p & gcdp p q %= e.1 × p + e.2 × q].
-
Lemma egcdpP p q :
p != 0
→ q != 0
→ ∀ (
e :=
egcdp p q),
-
[/\ size e.1 ≤ size q, size e.2 ≤ size p & gcdp p q %= e.1 × p + e.2 × q].
+
Lemma egcdpP p q :
p != 0
→ q != 0
→ ∀ (
e :=
egcdp p q),
+
[/\ size e.1 ≤ size q, size e.2 ≤ size p & gcdp p q %= e.1 × p + e.2 × q].
-
Lemma egcdpE p q (
e :=
egcdp p q) :
gcdp p q %= e.1 × p + e.2 × q.
+
Lemma egcdpE p q (
e :=
egcdp p q) :
gcdp p q %= e.1 × p + e.2 × q.
-
Lemma Bezoutp p q :
∃ u, u.1 × p + u.2 × q %= (gcdp p q).
+
Lemma Bezoutp p q :
∃ u, u.1 × p + u.2 × q %= (gcdp p q).
Lemma Bezout_coprimepP :
∀ p q,
-
reflect (
∃ u, u.1 × p + u.2 × q %= 1) (
coprimep p q).
+
reflect (
∃ u, u.1 × p + u.2 × q %= 1) (
coprimep p q).
-
Lemma coprimep_root p q x :
coprimep p q → root p x → q.[x] != 0.
+
Lemma coprimep_root p q x :
coprimep p q → root p x → q.[x] != 0.
-
Lemma Gauss_dvdpl p q d:
coprimep d q → (d %| p × q) = (d %| p).
+
Lemma Gauss_dvdpl p q d:
coprimep d q → (d %| p × q) = (d %| p).
-
Lemma Gauss_dvdpr p q d:
coprimep d q → (d %| q × p) = (d %| p).
+
Lemma Gauss_dvdpr p q d:
coprimep d q → (d %| q × p) = (d %| p).
Fixpoint gdcop_rec q p k :=
-
if k is m.+1 then
-
if coprimep p q then p
-
else gdcop_rec q (
divp p (
gcdp p q))
m
-
else (q == 0
)%:R.
+
if k is m.+1 then
+
if coprimep p q then p
+
else gdcop_rec q (
divp p (
gcdp p q))
m
+
else (q == 0
)%:R.
Definition gdcop q p :=
gdcop_rec q p (
size p).
-
CoInductive gdcop_spec q p :
{poly R} → Type :=
-
GdcopSpec r of (
dvdp r p) & (
(coprimep r q) || (p == 0
))
- & (
∀ d,
dvdp d p → coprimep d q → dvdp d r)
+
Variant gdcop_spec q p :
{poly R} → Type :=
+
GdcopSpec r of (
dvdp r p) & (
(coprimep r q) || (p == 0
))
+ & (
∀ d,
dvdp d p → coprimep d q → dvdp d r)
:
gdcop_spec q p r.
-
Lemma gdcop0 q :
gdcop q 0
= (q == 0
)%:R.
+
Lemma gdcop0 q :
gdcop q 0
= (q == 0
)%:R.
Lemma gdcop_recP :
∀ q p k,
-
size p ≤ k → gdcop_spec q p (
gdcop_rec q p k).
+
size p ≤ k → gdcop_spec q p (
gdcop_rec q p k).
Lemma gdcopP q p :
gdcop_spec q p (
gdcop q p).
-
Lemma coprimep_gdco p q : (
q != 0)%
B → coprimep (
gdcop p q)
p.
+
Lemma coprimep_gdco p q : (
q != 0)%
B → coprimep (
gdcop p q)
p.
-
Lemma size2_dvdp_gdco p q d :
p != 0
→ size d = 2%
N →
-
(d %| (gdcop q p)) = (d %| p) && ~~(d %| q).
+
Lemma size2_dvdp_gdco p q d :
p != 0
→ size d = 2%
N →
+
(d %| (gdcop q p)) = (d %| p) && ~~(d %| q).
-
Lemma dvdp_gdco p q :
(gdcop p q) %| q.
+
Lemma dvdp_gdco p q :
(gdcop p q) %| q.
-
Lemma root_gdco p q x :
p != 0
→ root (
gdcop q p)
x = root p x && ~~(root q x).
+
Lemma root_gdco p q x :
p != 0
→ root (
gdcop q p)
x = root p x && ~~(root q x).
-
Lemma dvdp_comp_poly r p q :
(p %| q) → (p \Po r) %| (q \Po r).
+
Lemma dvdp_comp_poly r p q :
(p %| q) → (p \Po r) %| (q \Po r).
-
Lemma gcdp_comp_poly r p q :
gcdp p q \Po r %= gcdp (
p \Po r) (
q \Po r).
+
Lemma gcdp_comp_poly r p q :
gcdp p q \Po r %= gcdp (
p \Po r) (
q \Po r).
-
Lemma coprimep_comp_poly r p q :
coprimep p q → coprimep (
p \Po r) (
q \Po r).
+
Lemma coprimep_comp_poly r p q :
coprimep p q → coprimep (
p \Po r) (
q \Po r).
-
Lemma coprimep_addl_mul p q r :
coprimep r (
p × r + q)
= coprimep r q.
+
Lemma coprimep_addl_mul p q r :
coprimep r (
p × r + q)
= coprimep r q.
Definition irreducible_poly p :=
-
(size p > 1
) × (∀ q,
size q != 1%
N → q %| p → q %= p) : Prop.
+
(size p > 1
) × (∀ q,
size q != 1%
N → q %| p → q %= p) : Prop.
-
Lemma irredp_neq0 p :
irreducible_poly p → p != 0.
+
Lemma irredp_neq0 p :
irreducible_poly p → p != 0.
-
Definition apply_irredp p (
irr_p :
irreducible_poly p) :=
irr_p.2.
+
Definition apply_irredp p (
irr_p :
irreducible_poly p) :=
irr_p.2.
Coercion apply_irredp : irreducible_poly >-> Funclass.
-
Lemma modp_XsubC p c :
p %% ('X - c%:P) = p.[c]%:P.
+
Lemma modp_XsubC p c :
p %% ('X - c%:P) = p.[c]%:P.
-
Lemma coprimep_XsubC p c :
coprimep p (
'X - c%:P)
= ~~ root p c.
+
Lemma coprimep_XsubC p c :
coprimep p (
'X - c%:P)
= ~~ root p c.
-
Lemma coprimepX p :
coprimep p 'X = ~~ root p 0.
+
Lemma coprimepX p :
coprimep p 'X = ~~ root p 0.
-
Lemma eqp_monic :
{in monic &, ∀ p q,
(p %= q) = (p == q)}.
+
Lemma eqp_monic :
{in monic &, ∀ p q,
(p %= q) = (p == q)}.
Lemma dvdp_mul_XsubC p q c :
-
(p %| ('X - c%:P) × q) = ((if root p c then p %/ ('X - c%:P) else p) %| q).
+
(p %| ('X - c%:P) × q) = ((if root p c then p %/ ('X - c%:P) else p) %| q).
-
Lemma dvdp_prod_XsubC (
I :
Type) (
r :
seq I) (
F :
I → R)
p :
-
p %| \prod_(i <- r) ('X - (F i)%:P) →
-
{m | p %= \prod_(i <- mask m r) ('X - (F i)%:P)}.
+
Lemma dvdp_prod_XsubC (
I :
Type) (
r :
seq I) (
F :
I → R)
p :
+
p %| \prod_(i <- r) ('X - (F i)%:P) →
+
{m | p %= \prod_(i <- mask m r) ('X - (F i)%:P)}.
-
Lemma irredp_XsubC (
x :
R) :
irreducible_poly (
'X - x%:P).
+
Lemma irredp_XsubC (
x :
R) :
irreducible_poly (
'X - x%:P).
Lemma irredp_XsubCP d p :
-
irreducible_poly p → d %| p → {d %= 1
} + {d %= p}.
+
irreducible_poly p → d %| p → {d %= 1
} + {d %= p}.
End IDomainPseudoDivision.
-
Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp.
-
Hint Resolve dvdp0.
+
Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp :
core.
+
Hint Resolve dvdp0 :
core.
End CommonIdomain.
@@ -1526,38 +1525,38 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
idomainType.
-
Variable q :
{poly R}.
-
Hypothesis monq :
q \is monic.
+
Variable q :
{poly R}.
+
Hypothesis monq :
q \is monic.
-
Implicit Type p d r :
{poly R}.
+
Implicit Type p d r :
{poly R}.
-
Lemma divpE p :
p %/ q = rdivp p q.
+
Lemma divpE p :
p %/ q = rdivp p q.
-
Lemma modpE p :
p %% q = rmodp p q.
+
Lemma modpE p :
p %% q = rmodp p q.
-
Lemma scalpE p :
scalp p q = 0%
N.
+
Lemma scalpE p :
scalp p q = 0%
N.
-
Lemma divp_eq p :
p = (p %/ q) × q + (p %% q).
+
Lemma divp_eq p :
p = (p %/ q) × q + (p %% q).
-
Lemma divpp p :
q %/ q = 1.
+
Lemma divpp p :
q %/ q = 1.
-
Lemma dvdp_eq p :
(q %| p) = (p == (p %/ q) × q).
+
Lemma dvdp_eq p :
(q %| p) = (p == (p %/ q) × q).
-
Lemma dvdpP p :
reflect (
∃ qq, p = qq × q) (
q %| p).
+
Lemma dvdpP p :
reflect (
∃ qq, p = qq × q) (
q %| p).
-
Lemma mulpK p :
p × q %/ q = p.
+
Lemma mulpK p :
p × q %/ q = p.
-
Lemma mulKp p :
q × p %/ q = p.
+
Lemma mulKp p :
q × p %/ q = p.
End MonicDivisor.
@@ -1576,112 +1575,112 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
idomainType.
-
Variable d :
{poly R}.
+
Variable d :
{poly R}.
-
Hypothesis ulcd :
lead_coef d \in GRing.unit.
+
Hypothesis ulcd :
lead_coef d \in GRing.unit.
-
Implicit Type p q r :
{poly R}.
+
Implicit Type p q r :
{poly R}.
-
Lemma divp_eq p :
p = (p %/ d) × d + (p %% d).
+
Lemma divp_eq p :
p = (p %/ d) × d + (p %% d).
-
Lemma edivpP p q r :
p = q × d + r → size r < size d →
-
q = (p %/ d) ∧ r = p %% d.
+
Lemma edivpP p q r :
p = q × d + r → size r < size d →
+
q = (p %/ d) ∧ r = p %% d.
-
Lemma divpP p q r :
p = q × d + r → size r < size d →
-
q = (p %/ d).
+
Lemma divpP p q r :
p = q × d + r → size r < size d →
+
q = (p %/ d).
-
Lemma modpP p q r :
p = q × d + r → size r < size d → r = (p %% d).
+
Lemma modpP p q r :
p = q × d + r → size r < size d → r = (p %% d).
-
Lemma ulc_eqpP p q :
lead_coef q \is a GRing.unit →
-
reflect (
exists2 c : R, c != 0
& p = c *: q) (
p %= q).
+
Lemma ulc_eqpP p q :
lead_coef q \is a GRing.unit →
+
reflect (
exists2 c : R, c != 0
& p = c *: q) (
p %= q).
-
Lemma dvdp_eq p :
(d %| p) = (p == p %/ d × d).
+
Lemma dvdp_eq p :
(d %| p) = (p == p %/ d × d).
-
Lemma ucl_eqp_eq p q :
lead_coef q \is a GRing.unit →
-
p %= q → p = (lead_coef p / lead_coef q) *: q.
+
Lemma ucl_eqp_eq p q :
lead_coef q \is a GRing.unit →
+
p %= q → p = (lead_coef p / lead_coef q) *: q.
-
Lemma modp_scalel c p :
(c *: p) %% d = c *: (p %% d).
+
Lemma modp_scalel c p :
(c *: p) %% d = c *: (p %% d).
-
Lemma divp_scalel c p :
(c *: p) %/ d = c *: (p %/ d).
+
Lemma divp_scalel c p :
(c *: p) %/ d = c *: (p %/ d).
-
Lemma eqp_modpl p q :
p %= q → (p %% d) %= (q %% d).
+
Lemma eqp_modpl p q :
p %= q → (p %% d) %= (q %% d).
-
Lemma eqp_divl p q :
p %= q → (p %/ d) %= (q %/ d).
+
Lemma eqp_divl p q :
p %= q → (p %/ d) %= (q %/ d).
-
Lemma modp_opp p :
(- p) %% d = - (p %% d).
+
Lemma modp_opp p :
(- p) %% d = - (p %% d).
-
Lemma divp_opp p :
(- p) %/ d = - (p %/ d).
+
Lemma divp_opp p :
(- p) %/ d = - (p %/ d).
-
Lemma modp_add p q :
(p + q) %% d = p %% d + q %% d.
+
Lemma modp_add p q :
(p + q) %% d = p %% d + q %% d.
-
Lemma divp_add p q :
(p + q) %/ d = p %/ d + q %/ d.
+
Lemma divp_add p q :
(p + q) %/ d = p %/ d + q %/ d.
-
Lemma mulpK q :
(q × d) %/ d = q.
+
Lemma mulpK q :
(q × d) %/ d = q.
-
Lemma mulKp q :
(d × q) %/ d = q.
+
Lemma mulKp q :
(d × q) %/ d = q.
Lemma divp_addl_mul_small q r :
-
size r < size d → (q × d + r) %/ d = q.
+
size r < size d → (q × d + r) %/ d = q.
Lemma modp_addl_mul_small q r :
-
size r < size d → (q × d + r) %% d = r.
+
size r < size d → (q × d + r) %% d = r.
-
Lemma divp_addl_mul q r :
(q × d + r) %/ d = q + r %/ d.
+
Lemma divp_addl_mul q r :
(q × d + r) %/ d = q + r %/ d.
-
Lemma divpp :
d %/ d = 1.
+
Lemma divpp :
d %/ d = 1.
-
Lemma leq_trunc_divp m :
size (
m %/ d × d)
≤ size m.
+
Lemma leq_trunc_divp m :
size (
m %/ d × d)
≤ size m.
-
Lemma dvdpP p :
reflect (
∃ q, p = q × d) (
d %| p).
+
Lemma dvdpP p :
reflect (
∃ q, p = q × d) (
d %| p).
-
Lemma divpK p :
d %| p → p %/ d × d = p.
+
Lemma divpK p :
d %| p → p %/ d × d = p.
-
Lemma divpKC p :
d %| p → d × (p %/ d) = p.
+
Lemma divpKC p :
d %| p → d × (p %/ d) = p.
-
Lemma dvdp_eq_div p q :
d %| p → (q == p %/ d) = (q × d == p).
+
Lemma dvdp_eq_div p q :
d %| p → (q == p %/ d) = (q × d == p).
-
Lemma dvdp_eq_mul p q :
d %| p → (p == q × d) = (p %/ d == q).
+
Lemma dvdp_eq_mul p q :
d %| p → (p == q × d) = (p %/ d == q).
-
Lemma divp_mulA p q :
d %| q → p × (q %/ d) = p × q %/ d.
+
Lemma divp_mulA p q :
d %| q → p × (q %/ d) = p × q %/ d.
-
Lemma divp_mulAC m n :
d %| m → m %/ d × n = m × n %/ d.
+
Lemma divp_mulAC m n :
d %| m → m %/ d × n = m × n %/ d.
-
Lemma divp_mulCA p q :
d %| p → d %| q → p × (q %/ d) = q × (p %/ d).
+
Lemma divp_mulCA p q :
d %| p → d %| q → p × (q %/ d) = q × (p %/ d).
-
Lemma modp_mul p q :
(p × (q %% d)) %% d = (p × q) %% d.
+
Lemma modp_mul p q :
(p × (q %% d)) %% d = (p × q) %% d.
End UnitDivisor.
@@ -1691,35 +1690,35 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable R :
idomainType.
-
Variable d :
{poly R}.
-
Hypothesis ulcd :
lead_coef d \in GRing.unit.
+
Variable d :
{poly R}.
+
Hypothesis ulcd :
lead_coef d \in GRing.unit.
-
Implicit Types p q :
{poly R}.
+
Implicit Types p q :
{poly R}.
-
Lemma expp_sub m n :
n ≤ m → (
d ^+ (m - n))%
N = d ^+ m %/ d ^+ n.
+
Lemma expp_sub m n :
n ≤ m → (
d ^+ (m - n))%
N = d ^+ m %/ d ^+ n.
-
Lemma divp_pmul2l p q :
lead_coef q \in GRing.unit → d × p %/ (d × q) = p %/ q.
+
Lemma divp_pmul2l p q :
lead_coef q \in GRing.unit → d × p %/ (d × q) = p %/ q.
Lemma divp_pmul2r p q :
-
lead_coef p \in GRing.unit → q × d %/ (p × d) = q %/ p.
+
lead_coef p \in GRing.unit → q × d %/ (p × d) = q %/ p.
Lemma divp_divl r p q :
-
lead_coef r \in GRing.unit → lead_coef p \in GRing.unit →
-
q %/ p %/ r = q %/ (p × r).
+
lead_coef r \in GRing.unit → lead_coef p \in GRing.unit →
+
q %/ p %/ r = q %/ (p × r).
-
Lemma divpAC p q :
lead_coef p \in GRing.unit → q %/ d %/ p = q %/ p %/ d.
+
Lemma divpAC p q :
lead_coef p \in GRing.unit → q %/ d %/ p = q %/ p %/ d.
-
Lemma modp_scaler c p :
c \in GRing.unit → p %% (c *: d) = (p %% d).
+
Lemma modp_scaler c p :
c \in GRing.unit → p %% (c *: d) = (p %% d).
-
Lemma divp_scaler c p :
c \in GRing.unit → p %/ (c *: d) = c^-1 *: (p %/ d).
+
Lemma divp_scaler c p :
c \in GRing.unit → p %/ (c *: d) = c^-1 *: (p %/ d).
End MoreUnitDivisor.
@@ -1743,155 +1742,155 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable F :
fieldType.
-
Implicit Type p q r d :
{poly F}.
+
Implicit Type p q r d :
{poly F}.
-
Lemma divp_eq p q :
p = (p %/ q) × q + (p %% q).
+
Lemma divp_eq p q :
p = (p %/ q) × q + (p %% q).
-
Lemma divp_modpP p q d r :
p = q × d + r → size r < size d →
-
q = (p %/ d) ∧ r = p %% d.
+
Lemma divp_modpP p q d r :
p = q × d + r → size r < size d →
+
q = (p %/ d) ∧ r = p %% d.
-
Lemma divpP p q d r :
p = q × d + r → size r < size d →
-
q = (p %/ d).
+
Lemma divpP p q d r :
p = q × d + r → size r < size d →
+
q = (p %/ d).
-
Lemma modpP p q d r :
p = q × d + r → size r < size d → r = (p %% d).
+
Lemma modpP p q d r :
p = q × d + r → size r < size d → r = (p %% d).
-
Lemma eqpfP p q :
p %= q → p = (lead_coef p / lead_coef q) *: q.
+
Lemma eqpfP p q :
p %= q → p = (lead_coef p / lead_coef q) *: q.
-
Lemma dvdp_eq q p :
(q %| p) = (p == p %/ q × q).
+
Lemma dvdp_eq q p :
(q %| p) = (p == p %/ q × q).
-
Lemma eqpf_eq p q :
reflect (
exists2 c, c != 0
& p = c *: q) (
p %= q).
+
Lemma eqpf_eq p q :
reflect (
exists2 c, c != 0
& p = c *: q) (
p %= q).
-
Lemma modp_scalel c p q :
(c *: p) %% q = c *: (p %% q).
+
Lemma modp_scalel c p q :
(c *: p) %% q = c *: (p %% q).
-
Lemma mulpK p q :
q != 0
→ p × q %/ q = p.
+
Lemma mulpK p q :
q != 0
→ p × q %/ q = p.
-
Lemma mulKp p q :
q != 0
→ q × p %/ q = p.
+
Lemma mulKp p q :
q != 0
→ q × p %/ q = p.
-
Lemma divp_scalel c p q :
(c *: p) %/ q = c *: (p %/ q).
+
Lemma divp_scalel c p q :
(c *: p) %/ q = c *: (p %/ q).
-
Lemma modp_scaler c p d :
c != 0
→ p %% (c *: d) = (p %% d).
+
Lemma modp_scaler c p d :
c != 0
→ p %% (c *: d) = (p %% d).
-
Lemma divp_scaler c p d :
c != 0
→ p %/ (c *: d) = c^-1 *: (p %/ d).
+
Lemma divp_scaler c p d :
c != 0
→ p %/ (c *: d) = c^-1 *: (p %/ d).
-
Lemma eqp_modpl d p q :
p %= q → (p %% d) %= (q %% d).
+
Lemma eqp_modpl d p q :
p %= q → (p %% d) %= (q %% d).
-
Lemma eqp_divl d p q :
p %= q → (p %/ d) %= (q %/ d).
+
Lemma eqp_divl d p q :
p %= q → (p %/ d) %= (q %/ d).
-
Lemma eqp_modpr d p q :
p %= q → (d %% p) %= (d %% q).
+
Lemma eqp_modpr d p q :
p %= q → (d %% p) %= (d %% q).
-
Lemma eqp_mod p1 p2 q1 q2 :
p1 %= p2 → q1 %= q2 → p1 %% q1 %= p2 %% q2.
+
Lemma eqp_mod p1 p2 q1 q2 :
p1 %= p2 → q1 %= q2 → p1 %% q1 %= p2 %% q2.
-
Lemma eqp_divr (
d m n :
{poly F}) :
m %= n → (d %/ m) %= (d %/ n).
+
Lemma eqp_divr (
d m n :
{poly F}) :
m %= n → (d %/ m) %= (d %/ n).
-
Lemma eqp_div p1 p2 q1 q2 :
p1 %= p2 → q1 %= q2 → p1 %/ q1 %= p2 %/ q2.
+
Lemma eqp_div p1 p2 q1 q2 :
p1 %= p2 → q1 %= q2 → p1 %/ q1 %= p2 %/ q2.
-
Lemma eqp_gdcor p q r :
q %= r → gdcop p q %= gdcop p r.
+
Lemma eqp_gdcor p q r :
q %= r → gdcop p q %= gdcop p r.
-
Lemma eqp_gdcol p q r :
q %= r → gdcop q p %= gdcop r p.
+
Lemma eqp_gdcol p q r :
q %= r → gdcop q p %= gdcop r p.
-
Lemma eqp_rgdco_gdco q p :
rgdcop q p %= gdcop q p.
+
Lemma eqp_rgdco_gdco q p :
rgdcop q p %= gdcop q p.
-
Lemma modp_opp p q :
(- p) %% q = - (p %% q).
+
Lemma modp_opp p q :
(- p) %% q = - (p %% q).
-
Lemma divp_opp p q :
(- p) %/ q = - (p %/ q).
+
Lemma divp_opp p q :
(- p) %/ q = - (p %/ q).
-
Lemma modp_add d p q :
(p + q) %% d = p %% d + q %% d.
+
Lemma modp_add d p q :
(p + q) %% d = p %% d + q %% d.
-
Lemma modNp p q :
(- p) %% q = - (p %% q).
+
Lemma modNp p q :
(- p) %% q = - (p %% q).
-
Lemma divp_add d p q :
(p + q) %/ d = p %/ d + q %/ d.
+
Lemma divp_add d p q :
(p + q) %/ d = p %/ d + q %/ d.
Lemma divp_addl_mul_small d q r :
-
size r < size d → (q × d + r) %/ d = q.
+
size r < size d → (q × d + r) %/ d = q.
Lemma modp_addl_mul_small d q r :
-
size r < size d → (q × d + r) %% d = r.
+
size r < size d → (q × d + r) %% d = r.
-
Lemma divp_addl_mul d q r :
d != 0
→ (q × d + r) %/ d = q + r %/ d.
+
Lemma divp_addl_mul d q r :
d != 0
→ (q × d + r) %/ d = q + r %/ d.
-
Lemma divpp d :
d != 0
→ d %/ d = 1.
+
Lemma divpp d :
d != 0
→ d %/ d = 1.
-
Lemma leq_trunc_divp d m :
size (
m %/ d × d)
≤ size m.
+
Lemma leq_trunc_divp d m :
size (
m %/ d × d)
≤ size m.
-
Lemma divpK d p :
d %| p → p %/ d × d = p.
+
Lemma divpK d p :
d %| p → p %/ d × d = p.
-
Lemma divpKC d p :
d %| p → d × (p %/ d) = p.
+
Lemma divpKC d p :
d %| p → d × (p %/ d) = p.
-
Lemma dvdp_eq_div d p q :
d != 0
→ d %| p → (q == p %/ d) = (q × d == p).
+
Lemma dvdp_eq_div d p q :
d != 0
→ d %| p → (q == p %/ d) = (q × d == p).
-
Lemma dvdp_eq_mul d p q :
d != 0
→ d %| p → (p == q × d) = (p %/ d == q).
+
Lemma dvdp_eq_mul d p q :
d != 0
→ d %| p → (p == q × d) = (p %/ d == q).
-
Lemma divp_mulA d p q :
d %| q → p × (q %/ d) = p × q %/ d.
+
Lemma divp_mulA d p q :
d %| q → p × (q %/ d) = p × q %/ d.
-
Lemma divp_mulAC d m n :
d %| m → m %/ d × n = m × n %/ d.
+
Lemma divp_mulAC d m n :
d %| m → m %/ d × n = m × n %/ d.
-
Lemma divp_mulCA d p q :
d %| p → d %| q → p × (q %/ d) = q × (p %/ d).
+
Lemma divp_mulCA d p q :
d %| p → d %| q → p × (q %/ d) = q × (p %/ d).
-
Lemma expp_sub d m n :
d != 0
→ m ≥ n → (
d ^+ (m - n))%
N = d ^+ m %/ d ^+ n.
+
Lemma expp_sub d m n :
d != 0
→ m ≥ n → (
d ^+ (m - n))%
N = d ^+ m %/ d ^+ n.
-
Lemma divp_pmul2l d q p :
d != 0
→ q != 0
→ d × p %/ (d × q) = p %/ q.
+
Lemma divp_pmul2l d q p :
d != 0
→ q != 0
→ d × p %/ (d × q) = p %/ q.
-
Lemma divp_pmul2r d p q :
d != 0
→ p != 0
→ q × d %/ (p × d) = q %/ p.
+
Lemma divp_pmul2r d p q :
d != 0
→ p != 0
→ q × d %/ (p × d) = q %/ p.
-
Lemma divp_divl r p q :
q %/ p %/ r = q %/ (p × r).
+
Lemma divp_divl r p q :
q %/ p %/ r = q %/ (p × r).
-
Lemma divpAC d p q :
q %/ d %/ p = q %/ p %/ d.
+
Lemma divpAC d p q :
q %/ d %/ p = q %/ p %/ d.
-
Lemma edivp_def p q :
edivp p q = (0%
N, p %/ q, p %% q).
+
Lemma edivp_def p q :
edivp p q = (0%
N, p %/ q, p %% q).
-
Lemma divpE p q :
p %/ q = (lead_coef q)^-(rscalp p q) *: (rdivp p q).
+
Lemma divpE p q :
p %/ q = (lead_coef q)^-(rscalp p q) *: (rdivp p q).
-
Lemma modpE p q :
p %% q = (lead_coef q)^-(rscalp p q) *: (rmodp p q).
+
Lemma modpE p q :
p %% q = (lead_coef q)^-(rscalp p q) *: (rmodp p q).
-
Lemma scalpE p q :
scalp p q = 0%
N.
+
Lemma scalpE p q :
scalp p q = 0%
N.
@@ -1900,39 +1899,39 @@ Definition rmultp := [rel m d | rdvdp d m].
Just to have it without importing the weak theory
-
Lemma dvdpE p q :
p %| q = rdvdp p q.
+
Lemma dvdpE p q :
p %| q = rdvdp p q.
-
CoInductive edivp_spec m d :
nat × {poly F} × {poly F} → Type :=
+
Variant edivp_spec m d :
nat × {poly F} × {poly F} → Type :=
EdivpSpec n q r of
-
m = q × d + r &
(d != 0
) ==> (size r < size d) :
edivp_spec m d (n, q, r).
+
m = q × d + r &
(d != 0
) ==> (size r < size d) :
edivp_spec m d (n, q, r).
Lemma edivpP m d :
edivp_spec m d (
edivp m d).
-
Lemma edivp_eq d q r :
size r < size d → edivp (
q × d + r)
d = (0%
N, q, r).
+
Lemma edivp_eq d q r :
size r < size d → edivp (
q × d + r)
d = (0%
N, q, r).
-
Lemma modp_mul p q m :
(p × (q %% m)) %% m = (p × q) %% m.
+
Lemma modp_mul p q m :
(p × (q %% m)) %% m = (p × q) %% m.
-
Lemma dvdpP p q :
reflect (
∃ qq, p = qq × q) (
q %| p).
+
Lemma dvdpP p q :
reflect (
∃ qq, p = qq × q) (
q %| p).
Lemma Bezout_eq1_coprimepP :
∀ p q,
-
reflect (
∃ u, u.1 × p + u.2 × q = 1) (
coprimep p q).
+
reflect (
∃ u, u.1 × p + u.2 × q = 1) (
coprimep p q).
-
Lemma dvdp_gdcor p q :
q != 0
→ p %| (gdcop q p) × (q ^+ size p).
+
Lemma dvdp_gdcor p q :
q != 0
→ p %| (gdcop q p) × (q ^+ size p).
Lemma reducible_cubic_root p q :
-
size p ≤ 4
→ 1
< size q < size p → q %| p → {r | root p r}.
+
size p ≤ 4
→ 1
< size q < size p → q %| p → {r | root p r}.
Lemma cubic_irreducible p :
- 1
< size p ≤ 4
→ (∀ x,
~~ root p x) → irreducible_poly p.
+ 1
< size p ≤ 4
→ (∀ x,
~~ root p x) → irreducible_poly p.
Section FieldRingMap.
@@ -1941,14 +1940,14 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable rR :
ringType.
-
Variable f :
{rmorphism F → rR}.
+
Variable f :
{rmorphism F → rR}.
-
Implicit Type a b :
{poly F}.
+
Implicit Type a b :
{poly F}.
Lemma redivp_map a b :
-
redivp a^f b^f = (rscalp a b, (rdivp a b)^f, (rmodp a b)^f).
+
redivp a^f b^f = (rscalp a b, (rdivp a b)^f, (rmodp a b)^f).
End FieldRingMap.
@@ -1960,46 +1959,46 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable rR :
idomainType.
-
Variable f :
{rmorphism F → rR}.
+
Variable f :
{rmorphism F → rR}.
-
Implicit Type a b :
{poly F}.
+
Implicit Type a b :
{poly F}.
Lemma edivp_map a b :
-
edivp a^f b^f = (0%
N, (a %/ b)^f, (a %% b)^f).
+
edivp a^f b^f = (0%
N, (a %/ b)^f, (a %% b)^f).
-
Lemma scalp_map p q :
scalp p^f q^f = scalp p q.
+
Lemma scalp_map p q :
scalp p^f q^f = scalp p q.
-
Lemma map_divp p q :
(p %/ q)^f = p^f %/ q^f.
+
Lemma map_divp p q :
(p %/ q)^f = p^f %/ q^f.
-
Lemma map_modp p q :
(p %% q)^f = p^f %% q^f.
+
Lemma map_modp p q :
(p %% q)^f = p^f %% q^f.
Lemma egcdp_map p q :
egcdp (
map_poly f p) (
map_poly f q)
-
= (map_poly f (egcdp p q).1, map_poly f (egcdp p q).2).
+
= (map_poly f (egcdp p q).1, map_poly f (egcdp p q).2).
-
Lemma dvdp_map p q :
(p^f %| q^f) = (p %| q).
+
Lemma dvdp_map p q :
(p^f %| q^f) = (p %| q).
-
Lemma eqp_map p q :
(p^f %= q^f) = (p %= q).
+
Lemma eqp_map p q :
(p^f %= q^f) = (p %= q).
-
Lemma gcdp_map p q :
(gcdp p q)^f = gcdp p^f q^f.
+
Lemma gcdp_map p q :
(gcdp p q)^f = gcdp p^f q^f.
-
Lemma coprimep_map p q :
coprimep p^f q^f = coprimep p q.
+
Lemma coprimep_map p q :
coprimep p^f q^f = coprimep p q.
-
Lemma gdcop_rec_map p q n :
(gdcop_rec p q n)^f = (gdcop_rec p^f q^f n).
+
Lemma gdcop_rec_map p q n :
(gdcop_rec p q n)^f = (gdcop_rec p^f q^f n).
-
Lemma gdcop_map p q :
(gdcop p q)^f = (gdcop p^f q^f).
+
Lemma gdcop_map p q :
(gdcop p q)^f = (gdcop p^f q^f).
End FieldMap.
@@ -2023,12 +2022,12 @@ Definition rmultp := [rel m d | rdvdp d m].
Variable F :
closedFieldType.
-
Lemma root_coprimep (
p q :
{poly F}):
-
(∀ x,
root p x → q.[x] != 0
) → coprimep p q.
+
Lemma root_coprimep (
p q :
{poly F}):
+
(∀ x,
root p x → q.[x] != 0
) → coprimep p q.
-
Lemma coprimepP (
p q :
{poly F}):
-
reflect (
∀ x,
root p x → q.[x] != 0) (
coprimep p q).
+
Lemma coprimepP (
p q :
{poly F}):
+
reflect (
∀ x,
root p x → q.[x] != 0) (
coprimep p q).
End closed.
--
cgit v1.2.3