Library mathcomp.algebra.intdiv
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ This file provides various results on divisibility of integers.
+ It defines, for m, n, d : int,
+ (m %% d)%Z == the remainder of the Euclidean division of m by d; this is
+ the least non-negative element of the coset m + dZ when
+ d != 0, and m if d = 0.
+ (m %/ d)%Z == the quotient of the Euclidean division of m by d, such
+ that m = (m %/ d)%Z * d + (m %% d)%Z. Since for d != 0 the
+ remainder is non-negative, (m %/ d)%Z is non-zero for
+ (d %| m)%Z <=> m is divisible by d; dvdz d is the (collective) predicate
+ for integers divisible by d, and (d %| m)%Z is actually
+ (transposing) notation for m \in dvdz d.
+ (m = n % [mod d])%Z, (m == n % [mod d])%Z, (m != n % [mod d])%Z
+ m and n are (resp. compare, don't compare) equal mod d.
+ gcdz m n == the (non-negative) greatest common divisor of m and n,
+ with gcdz 0 0 = 0.
+ coprimez m n <=> m and n are coprime.
+ egcdz m n == the Bezout coefficients of the gcd of m and n: a pair
+ (u, v) of coprime integers such that u*m + v*n = gcdz m n.
+ Alternatively, a Bezoutz lemma states such u and v exist.
+ zchinese m1 m2 n1 n2 == for coprime m1 and m2, a solution to the Chinese
+ remainder problem for n1 and n2, i.e., and integer n such
+ that n = n1 % [mod m1] and n = n2 % [mod m2].
+ zcontents p == the contents of p : {poly int}, that is, the gcd of the
+ coefficients of p, with the lead coefficient of p,
+ zprimitive p == the primitive part of p : {poly int}, i.e., p divided by
+ its contents.
+ inIntSpan X v <-> v is an integral linear combination of elements of
+ X : seq V, where V is a zmodType. We prove that this is a
+ decidable property for Q-vector spaces.
+ int_Smith_normal_form :: a theorem asserting the existence of the Smith
+ normal form for integer matrices.
+ Note that many of the concepts and results in this file could and perhaps
+ sould be generalized to the more general setting of integral, unique
+ factorization, principal ideal, or Euclidean domains.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GRing.Theory Num.Theory.
+Local Open Scope ring_scope.
+ +
+Definition divz (m d : int) :=
+ let: (K, n) := match m with Posz n ⇒ (Posz, n) | Negz n ⇒ (Negz, n) end in
+ sgz d × K (n %/ `|d|)%N.
+ +
+Definition modz (m d : int) : int := m - divz m d × d.
+ +
+Definition dvdz d m := (`|d| %| `|m|)%N.
+ +
+Definition gcdz m n := (gcdn `|m| `|n|)%:Z.
+ +
+Definition egcdz m n : int × int :=
+ if m == 0 then (0, (-1) ^+ (n < 0)%R) else
+ let: (u, v) := egcdn `|m| `|n| in (sgz m × u, - (-1) ^+ (n < 0)%R × v%:Z).
+ +
+Definition coprimez m n := (gcdz m n == 1).
+ +
+Infix "%/" := divz : int_scope.
+Infix "%%" := modz : int_scope.
+Notation "d %| m" := (m \in dvdz d) : int_scope.
+Notation "m = n %[mod d ]" := (modz m d = modz n d) : int_scope.
+Notation "m == n %[mod d ]" := (modz m d == modz n d) : int_scope.
+Notation "m <> n %[mod d ]" := (modz m d ≠ modz n d) : int_scope.
+Notation "m != n %[mod d ]" := (modz m d != modz n d) : int_scope.
+ +
+Lemma divz_nat (n d : nat) : (n %/ d)%Z = (n %/ d)%N.
+ +
+Lemma divzN m d : (m %/ - d)%Z = - (m %/ d)%Z.
+ +
+Lemma divz_abs m d : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R × (m %/ d)%Z.
+ +
+Lemma div0z d : (0 %/ d)%Z = 0.
+ +
+Lemma divNz_nat m d : (d > 0)%N → (Negz m %/ d)%Z = - (m %/ d).+1%:Z.
+ +
+Lemma divz_eq m d : m = (m %/ d)%Z × d + (m %% d)%Z.
+ +
+Lemma modzN m d : (m %% - d)%Z = (m %% d)%Z.
+ +
+Lemma modz_abs m d : (m %% `|d|%N)%Z = (m %% d)%Z.
+ +
+Lemma modz_nat (m d : nat) : (m %% d)%Z = (m %% d)%N.
+ +
+Lemma modNz_nat m d : (d > 0)%N → (Negz m %% d)%Z = d%:Z - 1 - (m %% d)%:Z.
+ +
+Lemma modz_ge0 m d : d != 0 → 0 ≤ (m %% d)%Z.
+ +
+Lemma divz0 m : (m %/ 0)%Z = 0.
+Lemma mod0z d : (0 %% d)%Z = 0.
+Lemma modz0 m : (m %% 0)%Z = m.
+ +
+Lemma divz_small m d : 0 ≤ m < `|d|%:Z → (m %/ d)%Z = 0.
+ +
+Lemma divzMDl q m d : d != 0 → ((q × d + m) %/ d)%Z = q + (m %/ d)%Z.
+ +
+Lemma mulzK m d : d != 0 → (m × d %/ d)%Z = m.
+ +
+Lemma mulKz m d : d != 0 → (d × m %/ d)%Z = m.
+ +
+Lemma expzB p m n : p != 0 → (m ≥ n)%N → p ^+ (m - n) = (p ^+ m %/ p ^+ n)%Z.
+ +
+Lemma modz1 m : (m %% 1)%Z = 0.
+ +
+Lemma divz1 m : (m %/ 1)%Z = m.
+ +
+Lemma divzz d : (d %/ d)%Z = (d != 0).
+ +
+Lemma ltz_pmod m d : d > 0 → (m %% d)%Z < d.
+ +
+Lemma ltz_mod m d : d != 0 → (m %% d)%Z < `|d|.
+ +
+Lemma divzMpl p m d : p > 0 → (p × m %/ (p × d) = m %/ d)%Z.
+ +
+Lemma divzMpr p m d : p > 0 → (m × p %/ (d × p) = m %/ d)%Z.
+ +
+Lemma lez_floor m d : d != 0 → (m %/ d)%Z × d ≤ m.
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GRing.Theory Num.Theory.
+Local Open Scope ring_scope.
+ +
+Definition divz (m d : int) :=
+ let: (K, n) := match m with Posz n ⇒ (Posz, n) | Negz n ⇒ (Negz, n) end in
+ sgz d × K (n %/ `|d|)%N.
+ +
+Definition modz (m d : int) : int := m - divz m d × d.
+ +
+Definition dvdz d m := (`|d| %| `|m|)%N.
+ +
+Definition gcdz m n := (gcdn `|m| `|n|)%:Z.
+ +
+Definition egcdz m n : int × int :=
+ if m == 0 then (0, (-1) ^+ (n < 0)%R) else
+ let: (u, v) := egcdn `|m| `|n| in (sgz m × u, - (-1) ^+ (n < 0)%R × v%:Z).
+ +
+Definition coprimez m n := (gcdz m n == 1).
+ +
+Infix "%/" := divz : int_scope.
+Infix "%%" := modz : int_scope.
+Notation "d %| m" := (m \in dvdz d) : int_scope.
+Notation "m = n %[mod d ]" := (modz m d = modz n d) : int_scope.
+Notation "m == n %[mod d ]" := (modz m d == modz n d) : int_scope.
+Notation "m <> n %[mod d ]" := (modz m d ≠ modz n d) : int_scope.
+Notation "m != n %[mod d ]" := (modz m d != modz n d) : int_scope.
+ +
+Lemma divz_nat (n d : nat) : (n %/ d)%Z = (n %/ d)%N.
+ +
+Lemma divzN m d : (m %/ - d)%Z = - (m %/ d)%Z.
+ +
+Lemma divz_abs m d : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R × (m %/ d)%Z.
+ +
+Lemma div0z d : (0 %/ d)%Z = 0.
+ +
+Lemma divNz_nat m d : (d > 0)%N → (Negz m %/ d)%Z = - (m %/ d).+1%:Z.
+ +
+Lemma divz_eq m d : m = (m %/ d)%Z × d + (m %% d)%Z.
+ +
+Lemma modzN m d : (m %% - d)%Z = (m %% d)%Z.
+ +
+Lemma modz_abs m d : (m %% `|d|%N)%Z = (m %% d)%Z.
+ +
+Lemma modz_nat (m d : nat) : (m %% d)%Z = (m %% d)%N.
+ +
+Lemma modNz_nat m d : (d > 0)%N → (Negz m %% d)%Z = d%:Z - 1 - (m %% d)%:Z.
+ +
+Lemma modz_ge0 m d : d != 0 → 0 ≤ (m %% d)%Z.
+ +
+Lemma divz0 m : (m %/ 0)%Z = 0.
+Lemma mod0z d : (0 %% d)%Z = 0.
+Lemma modz0 m : (m %% 0)%Z = m.
+ +
+Lemma divz_small m d : 0 ≤ m < `|d|%:Z → (m %/ d)%Z = 0.
+ +
+Lemma divzMDl q m d : d != 0 → ((q × d + m) %/ d)%Z = q + (m %/ d)%Z.
+ +
+Lemma mulzK m d : d != 0 → (m × d %/ d)%Z = m.
+ +
+Lemma mulKz m d : d != 0 → (d × m %/ d)%Z = m.
+ +
+Lemma expzB p m n : p != 0 → (m ≥ n)%N → p ^+ (m - n) = (p ^+ m %/ p ^+ n)%Z.
+ +
+Lemma modz1 m : (m %% 1)%Z = 0.
+ +
+Lemma divz1 m : (m %/ 1)%Z = m.
+ +
+Lemma divzz d : (d %/ d)%Z = (d != 0).
+ +
+Lemma ltz_pmod m d : d > 0 → (m %% d)%Z < d.
+ +
+Lemma ltz_mod m d : d != 0 → (m %% d)%Z < `|d|.
+ +
+Lemma divzMpl p m d : p > 0 → (p × m %/ (p × d) = m %/ d)%Z.
+ +
+Lemma divzMpr p m d : p > 0 → (m × p %/ (d × p) = m %/ d)%Z.
+ +
+Lemma lez_floor m d : d != 0 → (m %/ d)%Z × d ≤ m.
+ +
+
+ leq_mod does not extend to negative m.
+
+
+Lemma lez_div m d : (`|(m %/ d)%Z| ≤ `|m|)%N.
+ +
+Lemma ltz_ceil m d : d > 0 → m < ((m %/ d)%Z + 1) × d.
+ +
+Lemma ltz_divLR m n d : d > 0 → ((m %/ d)%Z < n) = (m < n × d).
+ +
+Lemma lez_divRL m n d : d > 0 → (m ≤ (n %/ d)%Z) = (m × d ≤ n).
+ +
+Lemma divz_ge0 m d : d > 0 → ((m %/ d)%Z ≥ 0) = (m ≥ 0).
+ +
+Lemma divzMA_ge0 m n p : n ≥ 0 → (m %/ (n × p) = (m %/ n)%Z %/ p)%Z.
+ +
+Lemma modz_small m d : 0 ≤ m < d → (m %% d)%Z = m.
+ +
+Lemma modz_mod m d : ((m %% d)%Z = m %[mod d])%Z.
+ +
+Lemma modzMDl p m d : (p × d + m = m %[mod d])%Z.
+ +
+Lemma mulz_modr {p m d} : 0 < p → p × (m %% d)%Z = ((p × m) %% (p × d))%Z.
+ +
+Lemma mulz_modl {p m d} : 0 < p → (m %% d)%Z × p = ((m × p) %% (d × p))%Z.
+ +
+Lemma modzDl m d : (d + m = m %[mod d])%Z.
+ +
+Lemma modzDr m d : (m + d = m %[mod d])%Z.
+ +
+Lemma modzz d : (d %% d)%Z = 0.
+ +
+Lemma modzMl p d : (p × d %% d)%Z = 0.
+ +
+Lemma modzMr p d : (d × p %% d)%Z = 0.
+ +
+Lemma modzDml m n d : ((m %% d)%Z + n = m + n %[mod d])%Z.
+ +
+Lemma modzDmr m n d : (m + (n %% d)%Z = m + n %[mod d])%Z.
+ +
+Lemma modzDm m n d : ((m %% d)%Z + (n %% d)%Z = m + n %[mod d])%Z.
+ +
+Lemma eqz_modDl p m n d : (p + m == p + n %[mod d])%Z = (m == n %[mod d])%Z.
+ +
+Lemma eqz_modDr p m n d : (m + p == n + p %[mod d])%Z = (m == n %[mod d])%Z.
+ +
+Lemma modzMml m n d : ((m %% d)%Z × n = m × n %[mod d])%Z.
+ +
+Lemma modzMmr m n d : (m × (n %% d)%Z = m × n %[mod d])%Z.
+ +
+Lemma modzMm m n d : ((m %% d)%Z × (n %% d)%Z = m × n %[mod d])%Z.
+ +
+Lemma modzXm k m d : ((m %% d)%Z ^+ k = m ^+ k %[mod d])%Z.
+ +
+Lemma modzNm m d : (- (m %% d)%Z = - m %[mod d])%Z.
+ +
+Lemma modz_absm m d : ((-1) ^+ (m < 0)%R × (m %% d)%Z = `|m|%:Z %[mod d])%Z.
+ +
+
+
++ +
+Lemma ltz_ceil m d : d > 0 → m < ((m %/ d)%Z + 1) × d.
+ +
+Lemma ltz_divLR m n d : d > 0 → ((m %/ d)%Z < n) = (m < n × d).
+ +
+Lemma lez_divRL m n d : d > 0 → (m ≤ (n %/ d)%Z) = (m × d ≤ n).
+ +
+Lemma divz_ge0 m d : d > 0 → ((m %/ d)%Z ≥ 0) = (m ≥ 0).
+ +
+Lemma divzMA_ge0 m n p : n ≥ 0 → (m %/ (n × p) = (m %/ n)%Z %/ p)%Z.
+ +
+Lemma modz_small m d : 0 ≤ m < d → (m %% d)%Z = m.
+ +
+Lemma modz_mod m d : ((m %% d)%Z = m %[mod d])%Z.
+ +
+Lemma modzMDl p m d : (p × d + m = m %[mod d])%Z.
+ +
+Lemma mulz_modr {p m d} : 0 < p → p × (m %% d)%Z = ((p × m) %% (p × d))%Z.
+ +
+Lemma mulz_modl {p m d} : 0 < p → (m %% d)%Z × p = ((m × p) %% (d × p))%Z.
+ +
+Lemma modzDl m d : (d + m = m %[mod d])%Z.
+ +
+Lemma modzDr m d : (m + d = m %[mod d])%Z.
+ +
+Lemma modzz d : (d %% d)%Z = 0.
+ +
+Lemma modzMl p d : (p × d %% d)%Z = 0.
+ +
+Lemma modzMr p d : (d × p %% d)%Z = 0.
+ +
+Lemma modzDml m n d : ((m %% d)%Z + n = m + n %[mod d])%Z.
+ +
+Lemma modzDmr m n d : (m + (n %% d)%Z = m + n %[mod d])%Z.
+ +
+Lemma modzDm m n d : ((m %% d)%Z + (n %% d)%Z = m + n %[mod d])%Z.
+ +
+Lemma eqz_modDl p m n d : (p + m == p + n %[mod d])%Z = (m == n %[mod d])%Z.
+ +
+Lemma eqz_modDr p m n d : (m + p == n + p %[mod d])%Z = (m == n %[mod d])%Z.
+ +
+Lemma modzMml m n d : ((m %% d)%Z × n = m × n %[mod d])%Z.
+ +
+Lemma modzMmr m n d : (m × (n %% d)%Z = m × n %[mod d])%Z.
+ +
+Lemma modzMm m n d : ((m %% d)%Z × (n %% d)%Z = m × n %[mod d])%Z.
+ +
+Lemma modzXm k m d : ((m %% d)%Z ^+ k = m ^+ k %[mod d])%Z.
+ +
+Lemma modzNm m d : (- (m %% d)%Z = - m %[mod d])%Z.
+ +
+Lemma modz_absm m d : ((-1) ^+ (m < 0)%R × (m %% d)%Z = `|m|%:Z %[mod d])%Z.
+ +
+
+ Divisibility *
+
+
+
+
+Fact dvdz_key d : pred_key (dvdz d).
+Canonical dvdz_keyed d := KeyedPred (dvdz_key d).
+ +
+Lemma dvdzE d m : (d %| m)%Z = (`|d| %| `|m|)%N.
+Lemma dvdz0 d : (d %| 0)%Z.
+Lemma dvd0z n : (0 %| n)%Z = (n == 0).
+Lemma dvdz1 d : (d %| 1)%Z = (`|d|%N == 1%N).
+Lemma dvd1z m : (1 %| m)%Z.
+Lemma dvdzz m : (m %| m)%Z.
+ +
+Lemma dvdz_mull d m n : (d %| n)%Z → (d %| m × n)%Z.
+ +
+Lemma dvdz_mulr d m n : (d %| m)%Z → (d %| m × n)%Z.
+ Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr.
+ +
+Lemma dvdz_mul d1 d2 m1 m2 : (d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2)%Z.
+ +
+Lemma dvdz_trans n d m : (d %| n → n %| m → d %| m)%Z.
+ +
+Lemma dvdzP d m : reflect (∃ q, m = q × d) (d %| m)%Z.
+ +
+Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
+ +
+Lemma dvdz_eq d m : (d %| m)%Z = ((m %/ d)%Z × d == m).
+ +
+Lemma divzK d m : (d %| m)%Z → (m %/ d)%Z × d = m.
+ +
+Lemma lez_divLR d m n : 0 < d → (d %| m)%Z → ((m %/ d)%Z ≤ n) = (m ≤ n × d).
+ +
+Lemma ltz_divRL d m n : 0 < d → (d %| m)%Z → (n < m %/ d)%Z = (n × d < m).
+ +
+Lemma eqz_div d m n : d != 0 → (d %| m)%Z → (n == m %/ d)%Z = (n × d == m).
+ +
+Lemma eqz_mul d m n : d != 0 → (d %| m)%Z → (m == n × d) = (m %/ d == n)%Z.
+ +
+Lemma divz_mulAC d m n : (d %| m)%Z → (m %/ d)%Z × n = (m × n %/ d)%Z.
+ +
+Lemma mulz_divA d m n : (d %| n)%Z → m × (n %/ d)%Z = (m × n %/ d)%Z.
+ +
+Lemma mulz_divCA d m n :
+ (d %| m)%Z → (d %| n)%Z → m × (n %/ d)%Z = n × (m %/ d)%Z.
+ +
+Lemma divzA m n p : (p %| n → n %| m × p → m %/ (n %/ p)%Z = m × p %/ n)%Z.
+ +
+Lemma divzMA m n p : (n × p %| m → m %/ (n × p) = (m %/ n)%Z %/ p)%Z.
+ +
+Lemma divzAC m n p : (n × p %| m → (m %/ n)%Z %/ p = (m %/ p)%Z %/ n)%Z.
+ +
+Lemma divzMl p m d : p != 0 → (d %| m → p × m %/ (p × d) = m %/ d)%Z.
+ +
+Lemma divzMr p m d : p != 0 → (d %| m → m × p %/ (d × p) = m %/ d)%Z.
+ +
+Lemma dvdz_mul2l p d m : p != 0 → (p × d %| p × m)%Z = (d %| m)%Z.
+ +
+Lemma dvdz_mul2r p d m : p != 0 → (d × p %| m × p)%Z = (d %| m)%Z.
+ +
+Lemma dvdz_exp2l p m n : (m ≤ n)%N → (p ^+ m %| p ^+ n)%Z.
+ +
+Lemma dvdz_Pexp2l p m n : `|p| > 1 → (p ^+ m %| p ^+ n)%Z = (m ≤ n)%N.
+ +
+Lemma dvdz_exp2r m n k : (m %| n → m ^+ k %| n ^+ k)%Z.
+ +
+Fact dvdz_zmod_closed d : zmod_closed (dvdz d).
+Canonical dvdz_addPred d := AddrPred (dvdz_zmod_closed d).
+Canonical dvdz_oppPred d := OpprPred (dvdz_zmod_closed d).
+Canonical dvdz_zmodPred d := ZmodPred (dvdz_zmod_closed d).
+ +
+Lemma dvdz_exp k d m : (0 < k)%N → (d %| m → d %| m ^+ k)%Z.
+ +
+Lemma eqz_mod_dvd d m n : (m == n %[mod d])%Z = (d %| m - n)%Z.
+ +
+Lemma divzDl m n d :
+ (d %| m)%Z → ((m + n) %/ d)%Z = (m %/ d)%Z + (n %/ d)%Z.
+ +
+Lemma divzDr m n d :
+ (d %| n)%Z → ((m + n) %/ d)%Z = (m %/ d)%Z + (n %/ d)%Z.
+ +
+Lemma Qint_dvdz (m d : int) : (d %| m)%Z → ((m%:~R / d%:~R : rat) \is a Qint).
+ +
+Lemma Qnat_dvd (m d : nat) : (d %| m)%N → ((m%:R / d%:R : rat) \is a Qnat).
+ +
+
+
++Fact dvdz_key d : pred_key (dvdz d).
+Canonical dvdz_keyed d := KeyedPred (dvdz_key d).
+ +
+Lemma dvdzE d m : (d %| m)%Z = (`|d| %| `|m|)%N.
+Lemma dvdz0 d : (d %| 0)%Z.
+Lemma dvd0z n : (0 %| n)%Z = (n == 0).
+Lemma dvdz1 d : (d %| 1)%Z = (`|d|%N == 1%N).
+Lemma dvd1z m : (1 %| m)%Z.
+Lemma dvdzz m : (m %| m)%Z.
+ +
+Lemma dvdz_mull d m n : (d %| n)%Z → (d %| m × n)%Z.
+ +
+Lemma dvdz_mulr d m n : (d %| m)%Z → (d %| m × n)%Z.
+ Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr.
+ +
+Lemma dvdz_mul d1 d2 m1 m2 : (d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2)%Z.
+ +
+Lemma dvdz_trans n d m : (d %| n → n %| m → d %| m)%Z.
+ +
+Lemma dvdzP d m : reflect (∃ q, m = q × d) (d %| m)%Z.
+ +
+Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
+ +
+Lemma dvdz_eq d m : (d %| m)%Z = ((m %/ d)%Z × d == m).
+ +
+Lemma divzK d m : (d %| m)%Z → (m %/ d)%Z × d = m.
+ +
+Lemma lez_divLR d m n : 0 < d → (d %| m)%Z → ((m %/ d)%Z ≤ n) = (m ≤ n × d).
+ +
+Lemma ltz_divRL d m n : 0 < d → (d %| m)%Z → (n < m %/ d)%Z = (n × d < m).
+ +
+Lemma eqz_div d m n : d != 0 → (d %| m)%Z → (n == m %/ d)%Z = (n × d == m).
+ +
+Lemma eqz_mul d m n : d != 0 → (d %| m)%Z → (m == n × d) = (m %/ d == n)%Z.
+ +
+Lemma divz_mulAC d m n : (d %| m)%Z → (m %/ d)%Z × n = (m × n %/ d)%Z.
+ +
+Lemma mulz_divA d m n : (d %| n)%Z → m × (n %/ d)%Z = (m × n %/ d)%Z.
+ +
+Lemma mulz_divCA d m n :
+ (d %| m)%Z → (d %| n)%Z → m × (n %/ d)%Z = n × (m %/ d)%Z.
+ +
+Lemma divzA m n p : (p %| n → n %| m × p → m %/ (n %/ p)%Z = m × p %/ n)%Z.
+ +
+Lemma divzMA m n p : (n × p %| m → m %/ (n × p) = (m %/ n)%Z %/ p)%Z.
+ +
+Lemma divzAC m n p : (n × p %| m → (m %/ n)%Z %/ p = (m %/ p)%Z %/ n)%Z.
+ +
+Lemma divzMl p m d : p != 0 → (d %| m → p × m %/ (p × d) = m %/ d)%Z.
+ +
+Lemma divzMr p m d : p != 0 → (d %| m → m × p %/ (d × p) = m %/ d)%Z.
+ +
+Lemma dvdz_mul2l p d m : p != 0 → (p × d %| p × m)%Z = (d %| m)%Z.
+ +
+Lemma dvdz_mul2r p d m : p != 0 → (d × p %| m × p)%Z = (d %| m)%Z.
+ +
+Lemma dvdz_exp2l p m n : (m ≤ n)%N → (p ^+ m %| p ^+ n)%Z.
+ +
+Lemma dvdz_Pexp2l p m n : `|p| > 1 → (p ^+ m %| p ^+ n)%Z = (m ≤ n)%N.
+ +
+Lemma dvdz_exp2r m n k : (m %| n → m ^+ k %| n ^+ k)%Z.
+ +
+Fact dvdz_zmod_closed d : zmod_closed (dvdz d).
+Canonical dvdz_addPred d := AddrPred (dvdz_zmod_closed d).
+Canonical dvdz_oppPred d := OpprPred (dvdz_zmod_closed d).
+Canonical dvdz_zmodPred d := ZmodPred (dvdz_zmod_closed d).
+ +
+Lemma dvdz_exp k d m : (0 < k)%N → (d %| m → d %| m ^+ k)%Z.
+ +
+Lemma eqz_mod_dvd d m n : (m == n %[mod d])%Z = (d %| m - n)%Z.
+ +
+Lemma divzDl m n d :
+ (d %| m)%Z → ((m + n) %/ d)%Z = (m %/ d)%Z + (n %/ d)%Z.
+ +
+Lemma divzDr m n d :
+ (d %| n)%Z → ((m + n) %/ d)%Z = (m %/ d)%Z + (n %/ d)%Z.
+ +
+Lemma Qint_dvdz (m d : int) : (d %| m)%Z → ((m%:~R / d%:~R : rat) \is a Qint).
+ +
+Lemma Qnat_dvd (m d : nat) : (d %| m)%N → ((m%:R / d%:R : rat) \is a Qnat).
+ +
+
+ Greatest common divisor
+
+
+
+
+Lemma gcdzz m : gcdz m m = `|m|%:Z.
+Lemma gcdzC : commutative gcdz.
+Lemma gcd0z m : gcdz 0 m = `|m|%:Z.
+Lemma gcdz0 m : gcdz m 0 = `|m|%:Z.
+Lemma gcd1z : left_zero 1 gcdz.
+Lemma gcdz1 : right_zero 1 gcdz.
+Lemma dvdz_gcdr m n : (gcdz m n %| n)%Z.
+Lemma dvdz_gcdl m n : (gcdz m n %| m)%Z.
+Lemma gcdz_eq0 m n : (gcdz m n == 0) = (m == 0) && (n == 0).
+ Lemma gcdNz m n : gcdz (- m) n = gcdz m n.
+Lemma gcdzN m n : gcdz m (- n) = gcdz m n.
+ +
+Lemma gcdz_modr m n : gcdz m (n %% m)%Z = gcdz m n.
+ +
+Lemma gcdz_modl m n : gcdz (m %% n)%Z n = gcdz m n.
+ +
+Lemma gcdzMDl q m n : gcdz m (q × m + n) = gcdz m n.
+ +
+Lemma gcdzDl m n : gcdz m (m + n) = gcdz m n.
+ +
+Lemma gcdzDr m n : gcdz m (n + m) = gcdz m n.
+ +
+Lemma gcdzMl n m : gcdz n (m × n) = `|n|%:Z.
+ +
+Lemma gcdzMr n m : gcdz n (n × m) = `|n|%:Z.
+ +
+Lemma gcdz_idPl {m n} : reflect (gcdz m n = `|m|%:Z) (m %| n)%Z.
+ +
+Lemma gcdz_idPr {m n} : reflect (gcdz m n = `|n|%:Z) (n %| m)%Z.
+ +
+Lemma expz_min e m n : e ≥ 0 → e ^+ minn m n = gcdz (e ^+ m) (e ^+ n).
+ +
+Lemma dvdz_gcd p m n : (p %| gcdz m n)%Z = (p %| m)%Z && (p %| n)%Z.
+ +
+Lemma gcdzAC : right_commutative gcdz.
+ +
+Lemma gcdzA : associative gcdz.
+ +
+Lemma gcdzCA : left_commutative gcdz.
+ +
+Lemma gcdzACA : interchange gcdz gcdz.
+ +
+Lemma mulz_gcdr m n p : `|m|%:Z × gcdz n p = gcdz (m × n) (m × p).
+ +
+Lemma mulz_gcdl m n p : gcdz m n × `|p|%:Z = gcdz (m × p) (n × p).
+ +
+Lemma mulz_divCA_gcd n m : n × (m %/ gcdz n m)%Z = m × (n %/ gcdz n m)%Z.
+ +
+
+
++Lemma gcdzz m : gcdz m m = `|m|%:Z.
+Lemma gcdzC : commutative gcdz.
+Lemma gcd0z m : gcdz 0 m = `|m|%:Z.
+Lemma gcdz0 m : gcdz m 0 = `|m|%:Z.
+Lemma gcd1z : left_zero 1 gcdz.
+Lemma gcdz1 : right_zero 1 gcdz.
+Lemma dvdz_gcdr m n : (gcdz m n %| n)%Z.
+Lemma dvdz_gcdl m n : (gcdz m n %| m)%Z.
+Lemma gcdz_eq0 m n : (gcdz m n == 0) = (m == 0) && (n == 0).
+ Lemma gcdNz m n : gcdz (- m) n = gcdz m n.
+Lemma gcdzN m n : gcdz m (- n) = gcdz m n.
+ +
+Lemma gcdz_modr m n : gcdz m (n %% m)%Z = gcdz m n.
+ +
+Lemma gcdz_modl m n : gcdz (m %% n)%Z n = gcdz m n.
+ +
+Lemma gcdzMDl q m n : gcdz m (q × m + n) = gcdz m n.
+ +
+Lemma gcdzDl m n : gcdz m (m + n) = gcdz m n.
+ +
+Lemma gcdzDr m n : gcdz m (n + m) = gcdz m n.
+ +
+Lemma gcdzMl n m : gcdz n (m × n) = `|n|%:Z.
+ +
+Lemma gcdzMr n m : gcdz n (n × m) = `|n|%:Z.
+ +
+Lemma gcdz_idPl {m n} : reflect (gcdz m n = `|m|%:Z) (m %| n)%Z.
+ +
+Lemma gcdz_idPr {m n} : reflect (gcdz m n = `|n|%:Z) (n %| m)%Z.
+ +
+Lemma expz_min e m n : e ≥ 0 → e ^+ minn m n = gcdz (e ^+ m) (e ^+ n).
+ +
+Lemma dvdz_gcd p m n : (p %| gcdz m n)%Z = (p %| m)%Z && (p %| n)%Z.
+ +
+Lemma gcdzAC : right_commutative gcdz.
+ +
+Lemma gcdzA : associative gcdz.
+ +
+Lemma gcdzCA : left_commutative gcdz.
+ +
+Lemma gcdzACA : interchange gcdz gcdz.
+ +
+Lemma mulz_gcdr m n p : `|m|%:Z × gcdz n p = gcdz (m × n) (m × p).
+ +
+Lemma mulz_gcdl m n p : gcdz m n × `|p|%:Z = gcdz (m × p) (n × p).
+ +
+Lemma mulz_divCA_gcd n m : n × (m %/ gcdz n m)%Z = m × (n %/ gcdz n m)%Z.
+ +
+
+ Not including lcm theory, for now.
+
+
+ Coprime factors
+
+
+
+
+Lemma coprimezE m n : coprimez m n = coprime `|m| `|n|.
+ +
+Lemma coprimez_sym : symmetric coprimez.
+ +
+Lemma coprimeNz m n : coprimez (- m) n = coprimez m n.
+ +
+Lemma coprimezN m n : coprimez m (- n) = coprimez m n.
+ +
+CoInductive egcdz_spec m n : int × int → Type :=
+ EgcdzSpec u v of u × m + v × n = gcdz m n & coprimez u v
+ : egcdz_spec m n (u, v).
+ +
+Lemma egcdzP m n : egcdz_spec m n (egcdz m n).
+ +
+Lemma Bezoutz m n : {u : int & {v : int | u × m + v × n = gcdz m n}}.
+ +
+Lemma coprimezP m n :
+ reflect (∃ uv, uv.1 × m + uv.2 × n = 1) (coprimez m n).
+ +
+Lemma Gauss_dvdz m n p :
+ coprimez m n → (m × n %| p)%Z = (m %| p)%Z && (n %| p)%Z.
+ +
+Lemma Gauss_dvdzr m n p : coprimez m n → (m %| n × p)%Z = (m %| p)%Z.
+ +
+Lemma Gauss_dvdzl m n p : coprimez m p → (m %| n × p)%Z = (m %| n)%Z.
+ +
+Lemma Gauss_gcdzr p m n : coprimez p m → gcdz p (m × n) = gcdz p n.
+ +
+Lemma Gauss_gcdzl p m n : coprimez p n → gcdz p (m × n) = gcdz p m.
+ +
+Lemma coprimez_mulr p m n : coprimez p (m × n) = coprimez p m && coprimez p n.
+ +
+Lemma coprimez_mull p m n : coprimez (m × n) p = coprimez m p && coprimez n p.
+ +
+Lemma coprimez_pexpl k m n : (0 < k)%N → coprimez (m ^+ k) n = coprimez m n.
+ +
+Lemma coprimez_pexpr k m n : (0 < k)%N → coprimez m (n ^+ k) = coprimez m n.
+ +
+Lemma coprimez_expl k m n : coprimez m n → coprimez (m ^+ k) n.
+ +
+Lemma coprimez_expr k m n : coprimez m n → coprimez m (n ^+ k).
+ +
+Lemma coprimez_dvdl m n p : (m %| n)%N → coprimez n p → coprimez m p.
+ +
+Lemma coprimez_dvdr m n p : (m %| n)%N → coprimez p n → coprimez p m.
+ +
+Lemma dvdz_pexp2r m n k : (k > 0)%N → (m ^+ k %| n ^+ k)%Z = (m %| n)%Z.
+ +
+Section Chinese.
+ +
+
+
++Lemma coprimezE m n : coprimez m n = coprime `|m| `|n|.
+ +
+Lemma coprimez_sym : symmetric coprimez.
+ +
+Lemma coprimeNz m n : coprimez (- m) n = coprimez m n.
+ +
+Lemma coprimezN m n : coprimez m (- n) = coprimez m n.
+ +
+CoInductive egcdz_spec m n : int × int → Type :=
+ EgcdzSpec u v of u × m + v × n = gcdz m n & coprimez u v
+ : egcdz_spec m n (u, v).
+ +
+Lemma egcdzP m n : egcdz_spec m n (egcdz m n).
+ +
+Lemma Bezoutz m n : {u : int & {v : int | u × m + v × n = gcdz m n}}.
+ +
+Lemma coprimezP m n :
+ reflect (∃ uv, uv.1 × m + uv.2 × n = 1) (coprimez m n).
+ +
+Lemma Gauss_dvdz m n p :
+ coprimez m n → (m × n %| p)%Z = (m %| p)%Z && (n %| p)%Z.
+ +
+Lemma Gauss_dvdzr m n p : coprimez m n → (m %| n × p)%Z = (m %| p)%Z.
+ +
+Lemma Gauss_dvdzl m n p : coprimez m p → (m %| n × p)%Z = (m %| n)%Z.
+ +
+Lemma Gauss_gcdzr p m n : coprimez p m → gcdz p (m × n) = gcdz p n.
+ +
+Lemma Gauss_gcdzl p m n : coprimez p n → gcdz p (m × n) = gcdz p m.
+ +
+Lemma coprimez_mulr p m n : coprimez p (m × n) = coprimez p m && coprimez p n.
+ +
+Lemma coprimez_mull p m n : coprimez (m × n) p = coprimez m p && coprimez n p.
+ +
+Lemma coprimez_pexpl k m n : (0 < k)%N → coprimez (m ^+ k) n = coprimez m n.
+ +
+Lemma coprimez_pexpr k m n : (0 < k)%N → coprimez m (n ^+ k) = coprimez m n.
+ +
+Lemma coprimez_expl k m n : coprimez m n → coprimez (m ^+ k) n.
+ +
+Lemma coprimez_expr k m n : coprimez m n → coprimez m (n ^+ k).
+ +
+Lemma coprimez_dvdl m n p : (m %| n)%N → coprimez n p → coprimez m p.
+ +
+Lemma coprimez_dvdr m n p : (m %| n)%N → coprimez p n → coprimez p m.
+ +
+Lemma dvdz_pexp2r m n k : (k > 0)%N → (m ^+ k %| n ^+ k)%Z = (m %| n)%Z.
+ +
+Section Chinese.
+ +
+
+ The chinese remainder theorem
+
+
+
+
+Variables m1 m2 : int.
+Hypothesis co_m12 : coprimez m1 m2.
+ +
+Lemma zchinese_remainder x y :
+ (x == y %[mod m1 × m2])%Z = (x == y %[mod m1])%Z && (x == y %[mod m2])%Z.
+ +
+
+
++Variables m1 m2 : int.
+Hypothesis co_m12 : coprimez m1 m2.
+ +
+Lemma zchinese_remainder x y :
+ (x == y %[mod m1 × m2])%Z = (x == y %[mod m1])%Z && (x == y %[mod m2])%Z.
+ +
+
+ A function that solves the chinese remainder problem
+
+
+
+
+Definition zchinese r1 r2 :=
+ r1 × m2 × (egcdz m1 m2).2 + r2 × m1 × (egcdz m1 m2).1.
+ +
+Lemma zchinese_modl r1 r2 : (zchinese r1 r2 = r1 %[mod m1])%Z.
+ +
+Lemma zchinese_modr r1 r2 : (zchinese r1 r2 = r2 %[mod m2])%Z.
+ +
+Lemma zchinese_mod x : (x = zchinese (x %% m1)%Z (x %% m2)%Z %[mod m1 × m2])%Z.
+ +
+End Chinese.
+ +
+Section ZpolyScale.
+ +
+Definition zcontents p :=
+ sgz (lead_coef p) × \big[gcdn/0%N]_(i < size p) `|(p`_i)%R|%N.
+ +
+Lemma sgz_contents p : sgz (zcontents p) = sgz (lead_coef p).
+ +
+Lemma zcontents_eq0 p : (zcontents p == 0) = (p == 0).
+ +
+Lemma zcontents0 : zcontents 0 = 0.
+ +
+Lemma zcontentsZ a p : zcontents (a *: p) = a × zcontents p.
+ +
+Lemma zcontents_monic p : p \is monic → zcontents p = 1.
+ +
+Lemma dvdz_contents a p : (a %| zcontents p)%Z = (p \is a polyOver (dvdz a)).
+ +
+Lemma map_poly_divzK a p :
+ p \is a polyOver (dvdz a) → a *: map_poly (divz^~ a) p = p.
+ +
+Lemma polyOver_dvdzP a p :
+ reflect (∃ q, p = a *: q) (p \is a polyOver (dvdz a)).
+ +
+Definition zprimitive p := map_poly (divz^~ (zcontents p)) p.
+ +
+Lemma zpolyEprim p : p = zcontents p *: zprimitive p.
+ +
+Lemma zprimitive0 : zprimitive 0 = 0.
+ +
+Lemma zprimitive_eq0 p : (zprimitive p == 0) = (p == 0).
+ +
+Lemma size_zprimitive p : size (zprimitive p) = size p.
+ +
+Lemma sgz_lead_primitive p : sgz (lead_coef (zprimitive p)) = (p != 0).
+ +
+Lemma zcontents_primitive p : zcontents (zprimitive p) = (p != 0).
+ +
+Lemma zprimitive_id p : zprimitive (zprimitive p) = zprimitive p.
+ +
+Lemma zprimitive_monic p : p \in monic → zprimitive p = p.
+ +
+Lemma zprimitiveZ a p : a != 0 → zprimitive (a *: p) = zprimitive p.
+ +
+Lemma zprimitive_min p a q :
+ p != 0 → p = a *: q →
+ {b | sgz b = sgz (lead_coef q) & q = b *: zprimitive p}.
+ +
+Lemma zprimitive_irr p a q :
+ p != 0 → zprimitive p = a *: q → a = sgz (lead_coef q).
+ +
+Lemma zcontentsM p q : zcontents (p × q) = zcontents p × zcontents q.
+ +
+Lemma zprimitiveM p q : zprimitive (p × q) = zprimitive p × zprimitive q.
+ +
+Lemma dvdpP_int p q : p %| q → {r | q = zprimitive p × r}.
+ +
+ +
+Lemma size_rat_int_poly p : size (pZtoQ p) = size p.
+ +
+Lemma rat_poly_scale (p : {poly rat}) :
+ {q : {poly int} & {a | a != 0 & p = a%:~R^-1 *: pZtoQ q}}.
+ +
+Lemma dvdp_rat_int p q : (pZtoQ p %| pZtoQ q) = (p %| q).
+ +
+Lemma dvdpP_rat_int p q :
+ p %| pZtoQ q →
+ {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 × r}}.
+ +
+End ZpolyScale.
+ +
+
+
++Definition zchinese r1 r2 :=
+ r1 × m2 × (egcdz m1 m2).2 + r2 × m1 × (egcdz m1 m2).1.
+ +
+Lemma zchinese_modl r1 r2 : (zchinese r1 r2 = r1 %[mod m1])%Z.
+ +
+Lemma zchinese_modr r1 r2 : (zchinese r1 r2 = r2 %[mod m2])%Z.
+ +
+Lemma zchinese_mod x : (x = zchinese (x %% m1)%Z (x %% m2)%Z %[mod m1 × m2])%Z.
+ +
+End Chinese.
+ +
+Section ZpolyScale.
+ +
+Definition zcontents p :=
+ sgz (lead_coef p) × \big[gcdn/0%N]_(i < size p) `|(p`_i)%R|%N.
+ +
+Lemma sgz_contents p : sgz (zcontents p) = sgz (lead_coef p).
+ +
+Lemma zcontents_eq0 p : (zcontents p == 0) = (p == 0).
+ +
+Lemma zcontents0 : zcontents 0 = 0.
+ +
+Lemma zcontentsZ a p : zcontents (a *: p) = a × zcontents p.
+ +
+Lemma zcontents_monic p : p \is monic → zcontents p = 1.
+ +
+Lemma dvdz_contents a p : (a %| zcontents p)%Z = (p \is a polyOver (dvdz a)).
+ +
+Lemma map_poly_divzK a p :
+ p \is a polyOver (dvdz a) → a *: map_poly (divz^~ a) p = p.
+ +
+Lemma polyOver_dvdzP a p :
+ reflect (∃ q, p = a *: q) (p \is a polyOver (dvdz a)).
+ +
+Definition zprimitive p := map_poly (divz^~ (zcontents p)) p.
+ +
+Lemma zpolyEprim p : p = zcontents p *: zprimitive p.
+ +
+Lemma zprimitive0 : zprimitive 0 = 0.
+ +
+Lemma zprimitive_eq0 p : (zprimitive p == 0) = (p == 0).
+ +
+Lemma size_zprimitive p : size (zprimitive p) = size p.
+ +
+Lemma sgz_lead_primitive p : sgz (lead_coef (zprimitive p)) = (p != 0).
+ +
+Lemma zcontents_primitive p : zcontents (zprimitive p) = (p != 0).
+ +
+Lemma zprimitive_id p : zprimitive (zprimitive p) = zprimitive p.
+ +
+Lemma zprimitive_monic p : p \in monic → zprimitive p = p.
+ +
+Lemma zprimitiveZ a p : a != 0 → zprimitive (a *: p) = zprimitive p.
+ +
+Lemma zprimitive_min p a q :
+ p != 0 → p = a *: q →
+ {b | sgz b = sgz (lead_coef q) & q = b *: zprimitive p}.
+ +
+Lemma zprimitive_irr p a q :
+ p != 0 → zprimitive p = a *: q → a = sgz (lead_coef q).
+ +
+Lemma zcontentsM p q : zcontents (p × q) = zcontents p × zcontents q.
+ +
+Lemma zprimitiveM p q : zprimitive (p × q) = zprimitive p × zprimitive q.
+ +
+Lemma dvdpP_int p q : p %| q → {r | q = zprimitive p × r}.
+ +
+ +
+Lemma size_rat_int_poly p : size (pZtoQ p) = size p.
+ +
+Lemma rat_poly_scale (p : {poly rat}) :
+ {q : {poly int} & {a | a != 0 & p = a%:~R^-1 *: pZtoQ q}}.
+ +
+Lemma dvdp_rat_int p q : (pZtoQ p %| pZtoQ q) = (p %| q).
+ +
+Lemma dvdpP_rat_int p q :
+ p %| pZtoQ q →
+ {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 × r}}.
+ +
+End ZpolyScale.
+ +
+
+ Integral spans.
+
+
+
+
+Lemma int_Smith_normal_form m n (M : 'M[int]_(m, n)) :
+ {L : 'M[int]_m & L \in unitmx &
+ {R : 'M[int]_n & R \in unitmx &
+ {d : seq int | sorted dvdz d &
+ M = L ×m (\matrix_(i, j) (d`_i *+ (i == j :> nat))) ×m R}}}.
+ +
+Definition inIntSpan (V : zmodType) m (s : m.-tuple V) v :=
+ ∃ a : int ^ m, v = \sum_(i < m) s`_i *~ a i.
+ +
+Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v :
+ decidable (inIntSpan s v).
+ +
+
++Lemma int_Smith_normal_form m n (M : 'M[int]_(m, n)) :
+ {L : 'M[int]_m & L \in unitmx &
+ {R : 'M[int]_n & R \in unitmx &
+ {d : seq int | sorted dvdz d &
+ M = L ×m (\matrix_(i, j) (d`_i *+ (i == j :> nat))) ×m R}}}.
+ +
+Definition inIntSpan (V : zmodType) m (s : m.-tuple V) v :=
+ ∃ a : int ^ m, v = \sum_(i < m) s`_i *~ a i.
+ +
+Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v :
+ decidable (inIntSpan s v).
+ +
+