- -

Library mathcomp.algebra.polydiv

- -

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

- -

- This file provides a library for the basic theory of Euclidean and pseudo- - Euclidean division for polynomials over ring structures. - The library defines two versions of the pseudo-euclidean division: one for - coefficients in a (not necessarily commutative) ring structure and one for - coefficients equipped with a structure of integral domain. From the latter - we derive the definition of the usual Euclidean division for coefficients - in a field. Only the definition of the pseudo-division for coefficients in - an integral domain is exported by default and benefits from notations. - Also, the only theory exported by default is the one of division for - polynomials with coefficients in a field. - Other definitions and facts are qualified using name spaces indicating the - hypotheses made on the structure of coefficients and the properties of the - polynomial one divides with. - -

- - Pdiv.Field (exported by the present library): - edivp p q == pseudo-division of p by q with p q : {poly R} where - R is an idomainType. - Computes (k, quo, rem) : nat * {poly r} * {poly R}, - such that size rem < size q and: - + if lead_coef q is not a unit, then: - (lead_coef q ^+ k) *: p = q * quo + rem - + else if lead_coef q is a unit, then: - p = q * quo + rem and k = 0 - p %/ q == quotient (second component) computed by (edivp p q). - p %% q == remainder (third component) computed by (edivp p q). - scalp p q == exponent (first component) computed by (edivp p q). - p %| q == tests the nullity of the remainder of the - pseudo-division of p by q. - rgcdp p q == Pseudo-greater common divisor obtained by performing - the Euclidean algorithm on p and q using redivp as - Euclidean division. - p %= q == p and q are associate polynomials, i.e., p %| q and - q %| p, or equivalently, p = c *: q for some nonzero - constant c. - gcdp p q == Pseudo-greater common divisor obtained by performing - the Euclidean algorithm on p and q using edivp as - Euclidean division. - egcdp p q == The pair of Bezout coefficients: if e := egcdp p q, - then size e.1 <= size q, size e.2 <= size p, and - gcdp p q %= e.1 * p + e.2 * q - coprimep p q == p and q are coprime, i.e., (gcdp p q) is a nonzero - constant. - gdcop q p == greatest divisor of p which is coprime to q. - irreducible_poly p <-> p has only trivial (constant) divisors. - -

- - Pdiv.Idomain: theory available for edivp and the related operation under - the sole assumption that the ring of coefficients is canonically an - integral domain (R : idomainType). - -

- - Pdiv.IdomainMonic: theory available for edivp and the related operations - under the assumption that the ring of coefficients is canonically - and integral domain (R : idomainType) an the divisor is monic. - -

- - Pdiv.IdomainUnit: theory available for edivp and the related operations - under the assumption that the ring of coefficients is canonically an - integral domain (R : idomainType) and the leading coefficient of the - divisor is a unit. - -

- - Pdiv.ClosedField: theory available for edivp and the related operation - under the sole assumption that the ring of coefficients is canonically - an algebraically closed field (R : closedField). - -

- - Pdiv.Ring : - redivp p q == pseudo-division of p by q with p q : {poly R} where R is - a ringType. - Computes (k, quo, rem) : nat * {poly r} * {poly R}, - such that if rem = 0 then quo * q = p * (lead_coef q ^+ k) - -

- - rdivp p q == quotient (second component) computed by (redivp p q). - rmodp p q == remainder (third component) computed by (redivp p q). - rscalp p q == exponent (first component) computed by (redivp p q). - rdvdp p q == tests the nullity of the remainder of the pseudo-division - of p by q. - rgcdp p q == analogue of gcdp for coefficients in a ringType. - rgdcop p q == analogue of gdcop for coefficients in a ringType. -rcoprimep p q == analogue of coprimep p q for coefficients in a ringType. - -

- - Pdiv.RingComRreg : theory of the operations defined in Pdiv.Ring, when the - ring of coefficients is canonically commutative (R : comRingType) and - the leading coefficient of the divisor is both right regular and - commutes as a constant polynomial with the divisor itself - -

- - Pdiv.RingMonic : theory of the operations defined in Pdiv.Ring, under the - assumption that the divisor is monic. - -

- - Pdiv.UnitRing: theory of the operations defined in Pdiv.Ring, when the - ring R of coefficients is canonically with units (R : unitRingType). - -

- -
-Set Implicit Arguments.
- -
-Import GRing.Theory.
-Local Open Scope ring_scope.
- -
-Reserved Notation "p %= q" (at level 70, no associativity).
- -
- -
-Module Pdiv.
- -
-Module CommonRing.
- -
-Section RingPseudoDivision.
- -
-Variable R : ringType.
-Implicit Types d p q r : {poly R }.
- -
-

- -

- Pseudo division, defined on an arbitrary ring -

-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 ).
- -
-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 ].
- -
-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 rdiv0p p : rdivp 0 p = 0.
- -
-Lemma rdivp0 p : rdivp p 0 = 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 rmod0p p : rmodp 0 p = 0.
- -
-Lemma rmodp0 p : rmodp p 0 = p.
- -
-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_rmodpN0 p q : q != 0 → size (rmodp p q) < size q.
- -
-Lemma rmodp1 p : rmodp p 1 = 0.
- -
-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 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 rdvd0pP n : reflect (n = 0) (rdvdp 0 n).
- -
-Lemma rdvdpN0 p q : rdvdp p q → q != 0 → p != 0.
- -
-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 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 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 rr := rmodp pp qq 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 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.
- -
-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.
- -
-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.
- -
-Definition rgdcop q p := rgdcop_rec q p (size p).
- -
-Lemma rgdcop0 q : rgdcop q 0 = (q == 0)%:R.
- -
-End RingPseudoDivision.
- -
-End CommonRing.
- -
-Module RingComRreg.
- -
-Import CommonRing.
- -
-Section ComRegDivisor.
- -
-Variable R : ringType.
-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 }.
- -
-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 ).
- -
-

- -

- this is a bad name -

-Lemma rdivp_eq p :
- p × (lead_coef d ^+ (rscalp p d ))%:P = (rdivp p d ) × d + (rmodp p d ).
- -
-

- -

- section variables impose an inconvenient order on parameters -

-Lemma eq_rdvdp k q1 p:
-  p × ((lead_coef d )^+ k )%:P = q1 × d → rdvdp d p.
- -
-Variant rdvdp_spec p q : {poly R } → bool → Type :=
-  | Rdvdp k q1 & p × ((lead_coef q )^+ k )%:P = q1 × q : rdvdp_spec p q 0 true
-  | RdvdpN & rmodp p q != 0 : rdvdp_spec p q (rmodp p q) false.
- -
-

- -

- Is that version useable ? -

- -
-Lemma rdvdp_eqP p : rdvdp_spec p d (rmodp p d) (rdvdp d p).
- -
-Lemma rdvdp_mull p : rdvdp d (p × d).
- -
-Lemma rmodp_mull p : rmodp (p × d) d = 0.
- -
-Lemma rmodpp : rmodp d d = 0.
- -
-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.
- -
-End ComRegDivisor.
- -
-End RingComRreg.
- -
-Module RingMonic.
- -
-Import CommonRing.
- -
-Import RingComRreg.
- -
-Section MonicDivisor.
- -
-Variable R : ringType.
-Implicit Types p q r : {poly R }.
- -
-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 rdivp_eq p :
-  p = (rdivp p d ) × d + (rmodp p d ).
- -
-Lemma rdivpp : rdivp d d = 1.
- -
-Lemma rdivp_addl_mul_small q r :
-  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 q r :
-  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.
- -
-Lemma rdivp_mull p : rdivp (p × d) d = p.
- -
-Lemma rmodp_mull p : rmodp (p × 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.
- -
-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 rdvdpp : rdvdp d d.
- -
-

- -

- section variables impose an inconvenient order on parameters -

-Lemma eq_rdvdp q1 p : p = q1 × d → rdvdp d p.
- -
-Lemma rdvdp_mull p : rdvdp d (p × d).
- -
-Lemma rdvdpP p : reflect (∃ qq, p = qq × d) (rdvdp d p).
- -
-Lemma rdivpK p : rdvdp d p → (rdivp p d ) × d = p.
- -
-End MonicDivisor.
-End RingMonic.
- -
-Module Ring.
- -
-Include CommonRing.
-Import RingMonic.
- -
-Section ExtraMonicDivisor.
- -
-Variable R : ringType.
- -
-Implicit Types d p q r : {poly R }.
- -
-Lemma rdivp1 p : rdivp p 1 = p.
- -
-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 root_factor_theorem p x : root p x = (rdvdp ('X - x %:P) p ).
- -
-End ExtraMonicDivisor.
- -
-End Ring.
- -
-Module ComRing.
- -
-Import Ring.
- -
-Import RingComRreg.
- -
-Section CommutativeRingPseudoDivision.
- -
-Variable R : comRingType.
- -
-Implicit Types d p q m n r : {poly 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 ).
- -
-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 ).
- -
-End CommutativeRingPseudoDivision.
- -
-End ComRing.
- -
-Module UnitRing.
- -
-Import Ring.
- -
-Section UnitRingPseudoDivision.
- -
-Variable R : unitRingType.
-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.
- -
-End UnitRingPseudoDivision.
- -
-End UnitRing.
- -
-Module IdomainDefs.
- -
-Import Ring.
- -
-Section IDomainPseudoDivisionDefs.
- -
-Variable R : idomainType.
-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 ].
- -
-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.
-End IdomainDefs.
- -
-Module WeakIdomain.
- -
-Import Ring ComRing UnitRing IdomainDefs.
- -
-Section WeakTheoryForIDomainPseudoDivision.
- -
-Variable R : idomainType.
-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_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.
- -
-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.
- -
-Lemma scalpE 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 lc_expn_scalp_neq0 p q : lead_coef q ^+ scalp p q != 0.
- -
-Hint Resolve lc_expn_scalp_neq0 : core.
- -
-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.
- -
-

- -

- There are several ways to state this fact. The most appropriate statement - might be polished in light of usage. -

-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 divp_eq 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 ).
- -
-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 dvdpP 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 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.
- -
-End WeakTheoryForIDomainPseudoDivision.
- -
-Hint Resolve lc_expn_scalp_neq0 : core.
- -
-End WeakIdomain.
- -
-Module CommonIdomain.
- -
-Import Ring ComRing UnitRing IdomainDefs WeakIdomain.
- -
-Section IDomainPseudoDivision.
- -
-Variable R : idomainType.
-Implicit Type p q r d m n : {poly R }.
- -
-Lemma scalp0 p : scalp p 0 = 0%N.
- -
-Lemma divp_small p q : size p < size q → p %/ q = 0.
- -
-Lemma leq_divp p q : (size (p %/ q) ≤ size p).
- -
-Lemma div0p p : 0 %/ p = 0.
- -
-Lemma divp0 p : p %/ 0 = 0.
- -
-Lemma divp1 m : m %/ 1 = m.
- -
-Lemma modp0 p : p %% 0 = p.
- -
-Lemma mod0p p : 0 %% p = 0.
- -
-Lemma modp1 p : p %% 1 = 0.
- -
-Hint Resolve divp0 divp1 mod0p modp0 modp1 : core.
- -
-Lemma modp_small p q : size p < size q → p %% q = p.
- -
-Lemma modpC p c : c != 0 → p %% c %:P = 0.
- -
-Lemma modp_mull p q : (p × q ) %% q = 0.
- -
-Lemma modp_mulr d p : (d × p ) %% d = 0.
- -
-Lemma modpp d : d %% d = 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 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 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 modp_mod p q : (p %% q ) %% q = p %% q.
- -
-Lemma leq_modp m d : size (m %% d) ≤ size m.
- -
-Lemma dvdp0 d : d %| 0.
- -
-Hint Resolve dvdp0 : core.
- -
-Lemma dvd0p p : (0 %| p ) = (p == 0).
- -
-Lemma dvd0pP p : reflect (p = 0) (0 %| p).
- -
-Lemma dvdpN0 p q : p %| q → q != 0 → p != 0.
- -
-Lemma dvdp1 d : (d %| 1) = ((size d ) == 1%N).
- -
-Lemma dvd1p m : 1 %| m.
- -
-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_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)).
- -
-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 dvdpp d : d %| d.
- -
-Hint Resolve dvdpp : core.
- -
-Lemma divp_dvd p q : (p %| q ) → ((q %/ p ) %| q ).
- -
-Lemma dvdp_mull m d n : d %| n → d %| m × n.
- -
-Lemma dvdp_mulr n d m : d %| m → d %| m × n.
- -
-Hint Resolve dvdp_mull dvdp_mulr : core.
- -
-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_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_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_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_mod d n m : d %| n → (d %| m ) = (d %| m %% n ).
- -
-Lemma dvdp_trans : transitive (@dvdp R).
- -
-Lemma dvdp_mulIl p q : p %| 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_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 ).
- -
-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_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_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 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 ).
- -
-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 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).
- -
-Lemma eqp_eq p q: p %= q → (lead_coef q ) *: p = (lead_coef p ) *: q.
- -
-Lemma eqpxx : reflexive (@eqp R).
- -
-Hint Resolve eqpxx : core.
- -
-Lemma eqp_sym : symmetric (@eqp R).
- -
-Lemma eqp_trans : transitive (@eqp R).
- -
-Lemma eqp_ltrans : left_transitive (@eqp R).
- -
-Lemma eqp_rtrans : right_transitive (@eqp R).
- -
-Lemma eqp0 : ∀ p, (p %= 0) = (p == 0).
- -
-Lemma eqp01 : 0 %= (1 : {poly R }) = false.
- -
-Lemma eqp_scale p c : c != 0 → c *: p %= p.
- -
-Lemma eqp_size p q : p %= q → size p = size q.
- -
-Lemma size_poly_eq1 p : (size p == 1%N) = (p %= 1).
- -
-Lemma polyXsubC_eqp1 (x : R) : ('X - x %:P %= 1) = false.
- -
-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_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_scalel c m n : c != 0 → (c *: m %| n ) = (m %| n ).
- -
-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_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_mulr q p r : (p %= q ) → (p × r %= q × r ).
- -
-Lemma eqp_exp p q k : p %= q → p ^+ k %= q ^+ k.
- -
-Lemma polyC_eqp1 (c : R) : (c %:P %= 1) = (c != 0).
- -
-Lemma dvdUp d p: d %= 1 → d %| p.
- -
-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_rmod_mod p q : rmodp p q %= modp 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.
- -
-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 rr := modp pp qq 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.
- -
-Lemma gcd0p : left_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.
- -
-Lemma size_gcd1p p : size (gcdp 1 p) = 1%N.
- -
-Lemma size_gcdp1 p : size (gcdp p 1) = 1%N.
- -
-Lemma gcdpp : idempotent gcdp.
- -
-Lemma dvdp_gcdlr p q : (gcdp p q %| p ) && (gcdp p q %| q ).
- -
-Lemma dvdp_gcdl p q : gcdp p q %| p.
- -
-Lemma dvdp_gcdr p q :gcdp p q %| q.
- -
-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 dvdp_gcd p m n : p %| gcdp m n = (p %| m ) && (p %| n ).
- -
-Lemma gcdpC : ∀ p q, gcdp p q %= gcdp q p.
- -
-Lemma gcd1p p : gcdp 1 p %= 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 m n : gcdp m (m + n) %= 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_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_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_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_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_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_rgcd_gcd p q : rgcdp p q %= gcdp p q.
- -
-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_def d m n :
-    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.
- -
-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_scalel c 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.
- -
-Lemma coprimepp p : coprimep p p = (size p == 1%N).
- -
-Lemma gcdp_eqp1 p q : gcdp p q %= 1 = (coprimep p q ).
- -
-Lemma coprimep_sym p q : coprimep p q = coprimep q p.
- -
-Lemma coprime1p p : coprimep 1 p.
- -
-Lemma coprimep1 p : coprimep p 1.
- -
-Lemma coprimep0 p : coprimep p 0 = (p %= 1).
- -
-Lemma coprime0p p : coprimep 0 p = (p %= 1).
- -
-

- -

- This is different from coprimeP in div. shall we keep this? -

-Lemma coprimepP p q :
- reflect (∀ d, d %| p → d %| q → d %= 1) (coprimep p q).
- -
-Lemma coprimepPn p q : p != 0 →
- reflect (∃ d, (d %| gcdp p q ) && ~~ (d %= 1)) (~~ coprimep p q).
- -
-Lemma coprimep_dvdl q p r : r %| q → coprimep p q → coprimep p r.
- -
-Lemma coprimep_dvdr p q r :
- r %| p → coprimep p q → coprimep r q.
- -
-Lemma coprimep_modl p q : coprimep (p %% q) q = coprimep p q.
- -
-Lemma coprimep_modr q p : coprimep q (p %% q) = coprimep q p.
- -
-Lemma rcoprimep_coprimep q p : rcoprimep q p = coprimep q p.
- -
-Lemma eqp_coprimepr p q r : q %= r → coprimep p q = coprimep p r.
- -
-Lemma eqp_coprimepl p q r : q %= r → coprimep q p = coprimep r p.
- -
-

- -

- This should be implemented with an extended remainder sequence -

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

- -

- No provable egcd0p -

-Lemma egcdp0 p : egcdp p 0 = (1, 0).
- -
-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 ].
- -
-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 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).
- -
-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_dvdpr p q d: coprimep d q → (d %| q × p ) = (d %| p ).
- -
-

- -

- This could be simplified with the introduction of lcmp -

-Lemma Gauss_dvdp m n p : coprimep m n → (m × n %| p ) = (m %| p ) && (n %| p ).
- -
-Lemma Gauss_gcdpr p m n : coprimep p m → gcdp p (m × n) %= gcdp p n.
- -
-Lemma Gauss_gcdpl p m n : coprimep p n → gcdp p (m × n) %= gcdp p m.
- -
-Lemma coprimep_mulr p q r : coprimep p (q × r) = (coprimep p q && coprimep p r ).
- -
-Lemma coprimep_mull p q r: coprimep (q × r) p = (coprimep q p && coprimep r p ).
- -
-Lemma modp_coprime k u n : k != 0 → (k × u ) %% n %= 1 → coprimep k n.
- -
-Lemma coprimep_pexpl k m n : 0 < k → coprimep (m ^+ k) n = coprimep m n.
- -
-Lemma coprimep_pexpr k m n : 0 < k → coprimep m (n ^+ k) = coprimep m n.
- -
-Lemma coprimep_expl k m n : coprimep m n → coprimep (m ^+ k) n.
- -
-Lemma coprimep_expr k m n : coprimep m n → coprimep m (n ^+ k).
- -
-Lemma gcdp_mul2l p q r : gcdp (p × q) (p × r) %= (p × gcdp q r ).
- -
-Lemma gcdp_mul2r q r p : gcdp (q × p) (r × p) %= (gcdp q r × p ).
- -
-Lemma mulp_gcdr p q r : r × (gcdp p q ) %= gcdp (r × p) (r × q).
- -
-Lemma mulp_gcdl p q r : (gcdp p q ) × r %= gcdp (p × r) (q × r).
- -
-Lemma coprimep_div_gcd p q : (p != 0) || (q != 0) →
-  coprimep (p %/ (gcdp p q )) (q %/ gcdp p q).
- -
-Lemma divp_eq0 p q : (p %/ q == 0) = [|| p == 0, q ==0 | size p < size q ].
- -
-Lemma dvdp_div_eq0 p q : q %| p → (p %/ q == 0) = (p == 0).
- -
-Lemma Bezout_coprimepPn p q : p != 0 → q != 0 →
-  reflect (exists2 uv : {poly R } × {poly R },
-    (0 < size uv .1 < size q ) && (0 < size uv .2 < size p ) &
-      uv .1 × p = uv .2 × q)
-    (~~ (coprimep p q )).
- -
-Lemma dvdp_pexp2r m n k : k > 0 → (m ^+ k %| n ^+ k ) = (m %| n ).
- -
-Lemma root_gcd p q x : root (gcdp p q) x = root p x && root q x.
- -
-Lemma root_biggcd : ∀ x (ps : seq {poly R }),
-  root (\big [gcdp /0]_(p <- ps ) p) x = all (fun p ⇒ root p x) ps.
- -
-

- -

- "gdcop Q P" is the Greatest Divisor of P which is coprime to Q - if P null, we pose that gdcop returns 1 if Q null, 0 otherwise -

-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.
- -
-Definition gdcop q p := gdcop_rec q p (size p).
- -
-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 gdcop_recP : ∀ 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 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 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 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_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.
- -
-Lemma irredp_neq0 p : irreducible_poly p → p != 0.
- -
-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 coprimep_XsubC p c : coprimep p ('X - c %:P) = ~~ root p c.
- -
-Lemma coprimepX p : coprimep p 'X = ~~ root p 0.
- -
-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 ).
- -
-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_XsubCP 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 : core.
-Hint Resolve dvdp0 : core.
- -
-End CommonIdomain.
- -
-Module Idomain.
- -
-Include IdomainDefs.
-Export IdomainDefs.
-Include WeakIdomain.
-Include CommonIdomain.
- -
-End Idomain.
- -
-Module IdomainMonic.
- -
-Import Ring ComRing UnitRing IdomainDefs Idomain.
- -
-Section MonicDivisor.
- -
-Variable R : idomainType.
-Variable q : {poly R }.
-Hypothesis monq : q \is monic.
- -
-Implicit Type p d r : {poly R }.
- -
-Lemma divpE p : p %/ q = rdivp p q.
- -
-Lemma modpE p : p %% q = rmodp p q.
- -
-Lemma scalpE p : scalp p q = 0%N.
- -
-Lemma divp_eq p : p = (p %/ q ) × q + (p %% q ).
- -
-Lemma divpp p : q %/ q = 1.
- -
-Lemma dvdp_eq p : (q %| p ) = (p == (p %/ q ) × q ).
- -
-Lemma dvdpP p : reflect (∃ qq, p = qq × q) (q %| p).
- -
-Lemma mulpK p : p × q %/ q = p.
- -
-Lemma mulKp p : q × p %/ q = p.
- -
-End MonicDivisor.
- -
-End IdomainMonic.
- -
-Module IdomainUnit.
- -
-Import Ring ComRing UnitRing IdomainDefs Idomain.
- -
-Section UnitDivisor.
- -
-Variable R : idomainType.
-Variable d : {poly R }.
- -
-Hypothesis ulcd : lead_coef d \in GRing.unit.
- -
-Implicit Type p q r : {poly R }.
- -
-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 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 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 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 divp_scalel c p : (c *: p ) %/ d = c *: (p %/ d ).
- -
-Lemma eqp_modpl 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 divp_opp p : (- p ) %/ d = - (p %/ 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 mulpK q : (q × d ) %/ 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.
- -
-Lemma modp_addl_mul_small q r :
-  size r < size d → (q × d + r ) %% d = r.
- -
-Lemma divp_addl_mul q r : (q × d + r ) %/ d = q + r %/ d.
- -
-Lemma divpp : d %/ d = 1.
- -
-Lemma leq_trunc_divp m : size (m %/ d × d) ≤ size m.
- -
-Lemma dvdpP p : reflect (∃ q, p = q × d) (d %| p).
- -
-Lemma divpK p : d %| p → p %/ d × 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_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_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 modp_mul p q : (p × (q %% d )) %% d = (p × q ) %% d.
- -
-End UnitDivisor.
- -
-Section MoreUnitDivisor.
- -
-Variable R : idomainType.
-Variable d : {poly R }.
-Hypothesis ulcd : lead_coef d \in GRing.unit.
- -
-Implicit Types p q : {poly R }.
- -
-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_pmul2r p q :
-  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 ).
- -
-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 divp_scaler c p : c \in GRing.unit → p %/ (c *: d ) = c ^-1 *: (p %/ d ).
- -
-End MoreUnitDivisor.
- -
-End IdomainUnit.
- -
-Module Field.
- -
-Import Ring ComRing UnitRing.
-Include IdomainDefs.
-Export IdomainDefs.
-Include CommonIdomain.
- -
-Section FieldDivision.
- -
-Variable F : fieldType.
- -
-Implicit Type p q r d : {poly F }.
- -
-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 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 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 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 mulpK p q : q != 0 → p × q %/ 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 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 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_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_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_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_rgdco_gdco q p : rgdcop q p %= gdcop q p.
- -
-Lemma modp_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 modNp p q : (- p ) %% q = - (p %% q ).
- -
-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.
- -
-Lemma modp_addl_mul_small d q 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 divpp d : d != 0 → d %/ d = 1.
- -
-Lemma leq_trunc_divp d m : size (m %/ d × d) ≤ size m.
- -
-Lemma divpK d p : d %| p → p %/ d × 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_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_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 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_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 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 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 scalpE p q : scalp p q = 0%N.
- -
-

- -

- Just to have it without importing the weak theory -

-Lemma dvdpE p q : p %| q = rdvdp p q.
- -
-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 ).
- -
-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 modp_mul p q m : (p × (q %% m )) %% m = (p × q ) %% m.
- -
-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).
- -
-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 }.
- -
-Lemma cubic_irreducible p :
-  1 < size p ≤ 4 → (∀ x, ~~ root p x ) → irreducible_poly p.
- -
-Section FieldRingMap.
- -
-Variable rR : ringType.
- -
-Variable f : {rmorphism F → rR }.
- -
-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 ).
- -
-End FieldRingMap.
- -
-Section FieldMap.
- -
-Variable rR : idomainType.
- -
-Variable f : {rmorphism F → rR }.
- -
-Implicit Type a b : {poly F }.
- -
-Lemma edivp_map a b :
-  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 map_divp 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 ).
- -
-Lemma dvdp_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 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_map p q : (gdcop p q )^f = (gdcop p ^f q ^f ).
- -
-End FieldMap.
- -
-End FieldDivision.
- -
-End Field.
- -
-Module ClosedField.
- -
-Import Field.
- -
-Section closed.
- -
-Variable F : closedFieldType.
- -
-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).
- -
-End closed.
- -
-End ClosedField.
- -
-End Pdiv.
- -
-Export Pdiv.Field.
-