Library mathcomp.algebra.ssrint
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import fintype finfun bigop order ssralg countalg ssrnum.
From mathcomp Require Import poly.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import fintype finfun bigop order ssralg countalg ssrnum.
From mathcomp Require Import poly.
This file develops a basic theory of signed integers, defining:
int == the type of signed integers, with two constructors Posz for
non-negative integers and Negz for negative integers. It
supports the realDomainType interface (and its parents).
n%:Z == explicit cast from nat to int (:= Posz n); displayed as n.
However (Posz m = Posz n) is displayed as (m = n :> int)
(and so are ==, != and <>)
Lemma NegzE : turns (Negz n) into - n.+1%:Z.
<number> == <number> as an int, with <number> an optional minus sign
followed by a sequence of digits. This notation is in
int_scope (delimited with %Z).
x *~ m == m times x, with m : int;
convertible to x *+ n if m is Posz n
convertible to x *- n.+1 if m is Negz n.
m%:~R == the image of m : int in a generic ring (:= 1 *~ m).
x ^ m == x to the m, with m : int;
convertible to x ^+ n if m is Posz n
convertible to x ^- n.+1 if m is Negz n.
sgz x == sign of x : R,
equals (0 : int) if and only x == 0,
equals (1 : int) if x is positive
and (-1 : int) otherwise.
`|m|%N == the n : nat such that `|m|%R = n%:Z, for m : int.
`|m - n|%N == the distance between m and n; the '-' is specialized to
the int type, so m and n can be either of type nat or int
thanks to the Posz coercion; m and n are however parsed in
the %N scope. The IntDist submodule provides this notation
and the corresponding theory independently of the rest of
of the int and ssralg libraries (and notations).
Warning: due to the declaration of Posz as a coercion, two terms might be
displayed the same while not being convertible, for instance:
(Posz (x - y)) and (Posz x) - (Posz y) for x, y : nat.
Set Implicit Arguments.
Declare Scope int_scope.
Declare Scope distn_scope.
Declare Scope rat_scope.
Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z").
Reserved Notation "n = m :> 'int'"
(at level 70, m at next level, format "n = m :> 'int'").
Reserved Notation "n == m :> 'int'"
(at level 70, m at next level, format "n == m :> 'int'").
Reserved Notation "n != m :> 'int'"
(at level 70, m at next level, format "n != m :> 'int'").
Reserved Notation "n <> m :> 'int'"
(at level 70, m at next level, format "n <> m :> 'int'").
Import Order.TTheory GRing.Theory Num.Theory.
Delimit Scope int_scope with Z.
Local Open Scope int_scope.
Defining int
This must be deferred to module DistInt to work around the design flaws of
the Coq module system.
Coercion Posz : nat >-> int.
Notation "n %:Z" := (Posz n) (only parsing) : int_scope.
Notation "n %:Z" := (Posz n) (only parsing) : ring_scope.
Notation "n = m :> 'int'" := (@eq int n%Z m%Z) (only parsing) : ring_scope.
Notation "n = m :> 'int'" := (Posz n = Posz m) (only printing) : ring_scope.
Notation "n == m :> 'int'" := ((n%Z : int) == (m%Z : int)) (only parsing)
: ring_scope.
Notation "n == m :> 'int'" := (Posz n == Posz m) (only printing) : ring_scope.
Notation "n != m :> 'int'" := ((n%Z : int) != (m%Z : int)) (only parsing)
: ring_scope.
Notation "n != m :> 'int'" := (Posz n != Posz m) (only printing) : ring_scope.
Notation "n <> m :> 'int'" := (not (@eq int n%Z m%Z)) (only parsing)
: ring_scope.
Notation "n <> m :> 'int'" := (Posz n ≠ Posz m) (only printing) : ring_scope.
Definition parse_int (x : Number.int) : int :=
match x with
| Number.IntDecimal (Decimal.Pos u) ⇒ Posz (Nat.of_uint u)
| Number.IntDecimal (Decimal.Neg u) ⇒ Negz (Nat.of_uint u).-1
| Number.IntHexadecimal (Hexadecimal.Pos u) ⇒ Posz (Nat.of_hex_uint u)
| Number.IntHexadecimal (Hexadecimal.Neg u) ⇒ Negz (Nat.of_hex_uint u).-1
end.
Definition print_int (x : int) : Number.int :=
match x with
| Posz n ⇒ Number.IntDecimal (Decimal.Pos (Nat.to_uint n))
| Negz n ⇒ Number.IntDecimal (Decimal.Neg (Nat.to_uint n.+1))
end.
Number Notation int parse_int print_int : int_scope.
Definition natsum_of_int (m : int) : nat + nat :=
match m with Posz p ⇒ inl _ p | Negz n ⇒ inr _ n end.
Definition int_of_natsum (m : nat + nat) :=
match m with inl p ⇒ Posz p | inr n ⇒ Negz n end.
Lemma natsum_of_intK : cancel natsum_of_int int_of_natsum.
Definition int_eqMixin := CanEqMixin natsum_of_intK.
Definition int_countMixin := CanCountMixin natsum_of_intK.
Definition int_choiceMixin := CountChoiceMixin int_countMixin.
Canonical int_eqType := Eval hnf in EqType int int_eqMixin.
Canonical int_choiceType := Eval hnf in ChoiceType int int_choiceMixin.
Canonical int_countType := Eval hnf in CountType int int_countMixin.
Lemma eqz_nat (m n : nat) : (m%:Z == n%:Z) = (m == n).
Module intZmod.
Section intZmod.
Definition addz (m n : int) :=
match m, n with
| Posz m', Posz n' ⇒ Posz (m' + n')
| Negz m', Negz n' ⇒ Negz (m' + n').+1
| Posz m', Negz n' ⇒ if n' < m' then Posz (m' - n'.+1) else Negz (n' - m')
| Negz n', Posz m' ⇒ if n' < m' then Posz (m' - n'.+1) else Negz (n' - m')
end.
Definition oppz m := nosimpl
match m with
| Posz n ⇒ if n is (n'.+1)%N then Negz n' else Posz 0
| Negz n ⇒ Posz (n.+1)%N
end.
Local Notation "-%Z" := (@oppz) : int_scope.
Local Notation "- x" := (oppz x) : int_scope.
Local Notation "+%Z" := (@addz) : int_scope.
Local Notation "x + y" := (addz x y) : int_scope.
Local Notation "x - y" := (x + - y) : int_scope.
Lemma PoszD : {morph Posz : m n / (m + n)%N >-> m + n}.
Local Coercion Posz : nat >-> int.
Lemma NegzE (n : nat) : Negz n = - n.+1.
Lemma int_rect (P : int → Type) :
P 0 → (∀ n : nat, P n → P (n.+1))
→ (∀ n : nat, P (- n) → P (- (n.+1)))
→ ∀ n : int, P n.
Definition int_rec := int_rect.
Definition int_ind := int_rect.
Variant int_spec (x : int) : int → Type :=
| ZintNull of x = 0 : int_spec x 0
| ZintPos n of x = n.+1 : int_spec x n.+1
| ZintNeg n of x = - (n.+1)%:Z : int_spec x (- n.+1).
Lemma intP x : int_spec x x.
Lemma addzC : commutative addz.
Lemma add0z : left_id 0 addz.
Lemma oppzK : involutive oppz.
Lemma oppzD : {morph oppz : m n / m + n}.
Lemma add1Pz (n : int) : 1 + (n - 1) = n.
Lemma subSz1 (n : int) : 1 + n - 1 = n.
Lemma addSnz (m : nat) (n : int) : (m.+1%N) + n = 1 + (m + n).
Lemma addSz (m n : int) : (1 + m) + n = 1 + (m + n).
Lemma addPz (m n : int) : (m - 1) + n = (m + n) - 1.
Lemma addzA : associative addz.
Lemma addNz : left_inverse (0:int) oppz addz.
Lemma predn_int (n : nat) : 0 < n → n.-1%:Z = n - 1.
Definition Mixin := ZmodMixin addzA addzC add0z addNz.
End intZmod.
End intZmod.
Canonical int_ZmodType := ZmodType int intZmod.Mixin.
Local Open Scope ring_scope.
Section intZmoduleTheory.
Local Coercion Posz : nat >-> int.
Lemma PoszD : {morph Posz : n m / (n + m)%N >-> n + m}.
Lemma NegzE (n : nat) : Negz n = -(n.+1)%:Z.
Lemma int_rect (P : int → Type) :
P 0 → (∀ n : nat, P n → P (n.+1)%N)
→ (∀ n : nat, P (- (n%:Z)) → P (- (n.+1%N%:Z)))
→ ∀ n : int, P n.
Definition int_rec := int_rect.
Definition int_ind := int_rect.
Variant int_spec (x : int) : int → Type :=
| ZintNull : int_spec x 0
| ZintPos n : int_spec x n.+1
| ZintNeg n : int_spec x (- (n.+1)%:Z).
Lemma intP x : int_spec x x.
Definition oppzD := (@opprD [zmodType of int]).
Lemma subzn (m n : nat) : (n ≤ m)%N → m%:Z - n%:Z = (m - n)%N.
Lemma subzSS (m n : nat) : m.+1%:Z - n.+1%:Z = m%:Z - n%:Z.
End intZmoduleTheory.
#[deprecated(since="mathcomp 1.17.0", note="Use oppzD instead.")]
Notation oppz_add := oppzD.
Module intRing.
Section intRing.
Local Coercion Posz : nat >-> int.
Definition mulz (m n : int) :=
match m, n with
| Posz m', Posz n' ⇒ (m' × n')%N%:Z
| Negz m', Negz n' ⇒ (m'.+1%N × n'.+1%N)%N%:Z
| Posz m', Negz n' ⇒ - (m' × (n'.+1%N))%N%:Z
| Negz n', Posz m' ⇒ - (m' × (n'.+1%N))%N%:Z
end.
Local Notation "*%Z" := (@mulz) : int_scope.
Local Notation "x * y" := (mulz x y) : int_scope.
Lemma mul0z : left_zero 0 *%Z.
Lemma mulzC : commutative mulz.
Lemma mulz0 : right_zero 0 *%Z.
Lemma mulzN (m n : int) : (m × (- n))%Z = - (m × n)%Z.
Lemma mulNz (m n : int) : ((- m) × n)%Z = - (m × n)%Z.
Lemma mulzA : associative mulz.
Lemma mul1z : left_id 1%Z mulz.
Lemma mulzS (x : int) (n : nat) : (x × n.+1%:Z)%Z = x + (x × n)%Z.
Lemma mulz_addl : left_distributive mulz (+%R).
Lemma nonzero1z : 1%Z != 0.
Definition comMixin := ComRingMixin mulzA mulzC mul1z mulz_addl nonzero1z.
End intRing.
End intRing.
Canonical int_Ring := Eval hnf in RingType int intRing.comMixin.
Canonical int_comRing := Eval hnf in ComRingType int intRing.mulzC.
Section intRingTheory.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma PoszM : {morph Posz : n m / (n × m)%N >-> n × m}.
Lemma intS (n : nat) : n.+1%:Z = 1 + n%:Z.
Lemma predn_int (n : nat) : (0 < n)%N → n.-1%:Z = n%:Z - 1.
End intRingTheory.
Module intUnitRing.
Section intUnitRing.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Definition unitz := [qualify a n : int | (n == 1) || (n == -1)].
Definition invz n : int := n.
Lemma mulVz : {in unitz, left_inverse 1%R invz *%R}.
Lemma mulzn_eq1 m (n : nat) : (m × n == 1) = (m == 1) && (n == 1%N).
Lemma unitzPl m n : n × m = 1 → m \is a unitz.
Lemma invz_out : {in [predC unitz], invz =1 id}.
Lemma idomain_axiomz m n : m × n = 0 → (m == 0) || (n == 0).
Definition comMixin := ComUnitRingMixin mulVz unitzPl invz_out.
End intUnitRing.
End intUnitRing.
Canonical int_unitRingType :=
Eval hnf in UnitRingType int intUnitRing.comMixin.
Canonical int_comUnitRing := Eval hnf in [comUnitRingType of int].
Canonical int_idomainType :=
Eval hnf in IdomainType int intUnitRing.idomain_axiomz.
Canonical int_countZmodType := [countZmodType of int].
Canonical int_countRingType := [countRingType of int].
Canonical int_countComRingType := [countComRingType of int].
Canonical int_countUnitRingType := [countUnitRingType of int].
Canonical int_countComUnitRingType := [countComUnitRingType of int].
Canonical int_countIdomainType := [countIdomainType of int].
Definition absz m := match m with Posz p ⇒ p | Negz n ⇒ n.+1 end.
Notation "m - n" :=
(@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
Arguments absz m%distn_scope.
Local Notation "`| m |" := (absz m) : nat_scope.
Module intOrdered.
Section intOrdered.
Implicit Types m n p : int.
Local Coercion Posz : nat >-> int.
Local Notation normz m := (absz m)%:Z.
Definition lez m n :=
match m, n with
| Posz m', Posz n' ⇒ (m' ≤ n')%N
| Posz m', Negz n' ⇒ false
| Negz m', Posz n' ⇒ true
| Negz m', Negz n' ⇒ (n' ≤ m')%N
end.
Definition ltz m n :=
match m, n with
| Posz m', Posz n' ⇒ (m' < n')%N
| Posz m', Negz n' ⇒ false
| Negz m', Posz n' ⇒ true
| Negz m', Negz n' ⇒ (n' < m')%N
end.
Fact lez_add m n : lez 0 m → lez 0 n → lez 0 (m + n).
Fact lez_mul m n : lez 0 m → lez 0 n → lez 0 (m × n).
Fact lez_anti m : lez 0 m → lez m 0 → m = 0.
Lemma subz_ge0 m n : lez 0 (n - m) = lez m n.
Fact lez_total m n : lez m n || lez n m.
Fact normzN m : normz (- m) = normz m.
Fact gez0_norm m : lez 0 m → normz m = m.
Fact ltz_def m n : (ltz m n) = (n != m) && (lez m n).
Definition Mixin : realLeMixin int_idomainType :=
RealLeMixin
lez_add lez_mul lez_anti subz_ge0 (lez_total 0) normzN gez0_norm ltz_def.
End intOrdered.
End intOrdered.
Canonical int_porderType := POrderType ring_display int intOrdered.Mixin.
Canonical int_latticeType := LatticeType int intOrdered.Mixin.
Canonical int_distrLatticeType := DistrLatticeType int intOrdered.Mixin.
Canonical int_orderType := OrderType int intOrdered.lez_total.
Canonical int_numDomainType := NumDomainType int intOrdered.Mixin.
Canonical int_normedZmodType := NormedZmodType int int intOrdered.Mixin.
Canonical int_realDomainType := [realDomainType of int].
Section intOrderedTheory.
Local Coercion Posz : nat >-> int.
Implicit Types m n p : nat.
Implicit Types x y z : int.
Lemma lez_nat m n : (m ≤ n :> int) = (m ≤ n)%N.
Lemma ltz_nat m n : (m < n :> int) = (m < n)%N.
Definition ltez_nat := (lez_nat, ltz_nat).
Lemma leNz_nat m n : (- m%:Z ≤ n).
Lemma ltNz_nat m n : (- m%:Z < n) = (m != 0%N) || (n != 0%N).
Definition lteNz_nat := (leNz_nat, ltNz_nat).
Lemma lezN_nat m n : (m%:Z ≤ - n%:Z) = (m == 0%N) && (n == 0%N).
Lemma ltzN_nat m n : (m%:Z < - n%:Z) = false.
Lemma le0z_nat n : 0 ≤ n :> int.
Lemma lez0_nat n : n ≤ 0 :> int = (n == 0%N :> nat).
Definition ltezN_nat := (lezN_nat, ltzN_nat).
Definition ltez_natE := (ltez_nat, lteNz_nat, ltezN_nat, le0z_nat, lez0_nat).
Lemma gtz0_ge1 x : (0 < x) = (1 ≤ x).
Lemma lez1D x y : (1 + x ≤ y) = (x < y).
Lemma lezD1 x y : (x + 1 ≤ y) = (x < y).
Lemma ltz1D x y : (x < 1 + y) = (x ≤ y).
Lemma ltzD1 x y : (x < y + 1) = (x ≤ y).
End intOrderedTheory.
#[deprecated(since="mathcomp 1.17.0", note="Use lez1D instead.")]
Notation lez_add1r := lez1D.
#[deprecated(since="mathcomp 1.17.0", note="Use lezD1 instead.")]
Notation lez_addr1 := lezD1.
#[deprecated(since="mathcomp 1.17.0", note="Use ltz1D instead.")]
Notation ltz_add1r := ltz1D.
#[deprecated(since="mathcomp 1.17.0", note="Use ltzD1 instead.")]
Notation ltz_addr1 := ltzD1.
Bind Scope ring_scope with int.
definition of intmul
Definition intmul (R : zmodType) (x : R) (n : int) := nosimpl
match n with
| Posz n ⇒ (x *+ n)%R
| Negz n ⇒ (x *- (n.+1))%R
end.
Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : fun_scope.
Notation "x *~ n" := (intmul x n)
(at level 40, left associativity, format "x *~ n") : ring_scope.
Notation intr := ( *~%R 1).
Notation "n %:~R" := (1 *~ n)%R
(at level 2, left associativity, format "n %:~R") : ring_scope.
Lemma pmulrn (R : zmodType) (x : R) (n : nat) : x *+ n = x *~ n%:Z.
Lemma nmulrn (R : zmodType) (x : R) (n : nat) : x *- n = x *~ - n%:Z.
Section ZintLmod.
Definition zmodule (M : Type) : Type := M.
Local Notation "M ^z" := (zmodule M) (at level 2, format "M ^z") : type_scope.
Local Coercion Posz : nat >-> int.
Variable M : zmodType.
Implicit Types m n : int.
Implicit Types x y z : M.
Fact mulrzA_C m n x : (x *~ n) *~ m = x *~ (m × n).
Fact mulrzAC m n x : (x *~ n) *~ m = (x *~ m) *~ n.
Fact mulr1z (x : M) : x *~ 1 = x.
Fact mulrzDl_tmp m : {morph ( *~%R^~ m : M → M) : x y / x + y}.
Lemma mulrzBl_nat (m n : nat) x : x *~ (m%:Z - n%:Z) = x *~ m - x *~ n.
Fact mulrzDr_tmp x : {morph *~%R x : m n / m + n}.
Definition Mint_LmodMixin :=
@LmodMixin _ [zmodType of M] (fun n x ⇒ x *~ n)
mulrzA_C mulr1z mulrzDl_tmp mulrzDr_tmp.
Canonical Mint_LmodType := LmodType int M^z Mint_LmodMixin.
Lemma scalezrE n x : n *: (x : M^z) = x *~ n.
Lemma mulrzA x m n : x *~ (m × n) = x *~ m *~ n.
Lemma mulr0z x : x *~ 0 = 0.
Lemma mul0rz n : 0 *~ n = 0 :> M.
Lemma mulrNz x n : x *~ (- n) = - (x *~ n).
Lemma mulrN1z x : x *~ (- 1) = - x.
Lemma mulNrz x n : (- x) *~ n = - (x *~ n).
Lemma mulrzBr x m n : x *~ (m - n) = x *~ m - x *~ n.
Lemma mulrzBl x y n : (x - y) *~ n = x *~ n - y *~ n.
Lemma mulrz_nat (n : nat) x : x *~ n%:R = x *+ n.
Lemma mulrz_sumr : ∀ x I r (P : pred I) F,
x *~ (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x *~ F i.
Lemma mulrz_suml : ∀ n I r (P : pred I) (F : I → M),
(\sum_(i <- r | P i) F i) *~ n= \sum_(i <- r | P i) F i *~ n.
Canonical intmul_additive x := Additive (@mulrzBr x).
End ZintLmod.
#[deprecated(since="mathcomp 2.1.0", note="Use mulrzDr_tmp instead. mulrzDl will be renamed mulrzDr in the future.")]
Notation mulrzDl := mulrzDr_tmp.
#[deprecated(since="mathcomp 2.1.0", note="Use mulrzDl_tmp instead. mulrzDr will be renamed mulrzDl in the future.")]
Notation mulrzDr := mulrzDl_tmp.
Lemma ffunMzE (I : finType) (M : zmodType) (f : {ffun I → M}) z x :
(f *~ z) x = f x *~ z.
Lemma intz (n : int) : n%:~R = n.
Lemma natz (n : nat) : n%:R = n%:Z :> int.
Section RintMod.
Local Coercion Posz : nat >-> int.
Variable R : ringType.
Implicit Types m n : int.
Implicit Types x y z : R.
Lemma mulrzAl n x y : (x *~ n) × y = (x × y) *~ n.
Lemma mulrzAr n x y : x × (y *~ n) = (x × y) *~ n.
Lemma mulrzl x n : n%:~R × x = x *~ n.
Lemma mulrzr x n : x × n%:~R = x *~ n.
Lemma mulNrNz n x : (-x) *~ (-n) = x *~ n.
Lemma mulrbz x (b : bool) : x *~ b = (if b then x else 0).
Lemma intrD m n : (m + n)%:~R = m%:~R + n%:~R :> R.
Lemma intrM m n : (m × n)%:~R = m%:~R × n%:~R :> R.
Lemma intmul1_is_rmorphism : rmorphism ( *~%R (1 : R)).
Canonical intmul1_rmorphism := RMorphism intmul1_is_rmorphism.
Lemma mulr2z n : n *~ 2 = n + n.
End RintMod.
Lemma mulrzz m n : m *~ n = m × n.
Lemma mulz2 n : n × 2%:Z = n + n.
Lemma mul2z n : 2%:Z × n = n + n.
Section LMod.
Variable R : ringType.
Variable V : (lmodType R).
Local Coercion Posz : nat >-> int.
Implicit Types m n : int.
Implicit Types x y z : R.
Implicit Types u v w : V.
Lemma scaler_int n v : n%:~R *: v = v *~ n.
Lemma scalerMzl a v n : (a *: v) *~ n = (a *~ n) *: v.
Lemma scalerMzr a v n : (a *: v) *~ n = a *: (v *~ n).
End LMod.
Lemma mulrz_int (M : zmodType) (n : int) (x : M) : x *~ n%:~R = x *~ n.
Section MorphTheory.
Local Coercion Posz : nat >-> int.
Section Additive.
Variables (U V : zmodType) (f : {additive U → V}).
Lemma raddfMz n : {morph f : x / x *~ n}.
End Additive.
Section Multiplicative.
Variables (R S : ringType) (f : {rmorphism R → S}).
Lemma rmorphMz : ∀ n, {morph f : x / x *~ n}.
Lemma rmorph_int : ∀ n, f n%:~R = n%:~R.
End Multiplicative.
Section Linear.
Variable R : ringType.
Variables (U V : lmodType R) (f : {linear U → V}).
Lemma linearMn : ∀ n, {morph f : x / x *~ n}.
End Linear.
Lemma raddf_int_scalable (aV rV : lmodType int) (f : {additive aV → rV}) :
scalable f.
Section Zintmul1rMorph.
Variable R : ringType.
Lemma commrMz (x y : R) n : GRing.comm x y → GRing.comm x (y *~ n).
Lemma commr_int (x : R) n : GRing.comm x n%:~R.
End Zintmul1rMorph.
Section ZintBigMorphism.
Variable R : ringType.
Lemma sumMz : ∀ I r (P : pred I) F,
(\sum_(i <- r | P i) F i)%N%:~R = \sum_(i <- r | P i) ((F i)%:~R) :> R.
Lemma prodMz : ∀ I r (P : pred I) F,
(\prod_(i <- r | P i) F i)%N%:~R = \prod_(i <- r | P i) ((F i)%:~R) :> R.
End ZintBigMorphism.
Section Frobenius.
Variable R : ringType.
Implicit Types x y : R.
Variable p : nat.
Hypothesis charFp : p \in [char R].
Local Notation "x ^f" := (Frobenius_aut charFp x).
Lemma Frobenius_autMz x n : (x *~ n)^f = x^f *~ n.
Lemma Frobenius_aut_int n : (n%:~R)^f = n%:~R.
End Frobenius.
Section NumMorphism.
Section PO.
Variables (R : numDomainType).
Implicit Types n m : int.
Implicit Types x y : R.
Lemma rmorphzP (f : {rmorphism int → R}) : f =1 ( *~%R 1).
match n with
| Posz n ⇒ (x *+ n)%R
| Negz n ⇒ (x *- (n.+1))%R
end.
Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : fun_scope.
Notation "x *~ n" := (intmul x n)
(at level 40, left associativity, format "x *~ n") : ring_scope.
Notation intr := ( *~%R 1).
Notation "n %:~R" := (1 *~ n)%R
(at level 2, left associativity, format "n %:~R") : ring_scope.
Lemma pmulrn (R : zmodType) (x : R) (n : nat) : x *+ n = x *~ n%:Z.
Lemma nmulrn (R : zmodType) (x : R) (n : nat) : x *- n = x *~ - n%:Z.
Section ZintLmod.
Definition zmodule (M : Type) : Type := M.
Local Notation "M ^z" := (zmodule M) (at level 2, format "M ^z") : type_scope.
Local Coercion Posz : nat >-> int.
Variable M : zmodType.
Implicit Types m n : int.
Implicit Types x y z : M.
Fact mulrzA_C m n x : (x *~ n) *~ m = x *~ (m × n).
Fact mulrzAC m n x : (x *~ n) *~ m = (x *~ m) *~ n.
Fact mulr1z (x : M) : x *~ 1 = x.
Fact mulrzDl_tmp m : {morph ( *~%R^~ m : M → M) : x y / x + y}.
Lemma mulrzBl_nat (m n : nat) x : x *~ (m%:Z - n%:Z) = x *~ m - x *~ n.
Fact mulrzDr_tmp x : {morph *~%R x : m n / m + n}.
Definition Mint_LmodMixin :=
@LmodMixin _ [zmodType of M] (fun n x ⇒ x *~ n)
mulrzA_C mulr1z mulrzDl_tmp mulrzDr_tmp.
Canonical Mint_LmodType := LmodType int M^z Mint_LmodMixin.
Lemma scalezrE n x : n *: (x : M^z) = x *~ n.
Lemma mulrzA x m n : x *~ (m × n) = x *~ m *~ n.
Lemma mulr0z x : x *~ 0 = 0.
Lemma mul0rz n : 0 *~ n = 0 :> M.
Lemma mulrNz x n : x *~ (- n) = - (x *~ n).
Lemma mulrN1z x : x *~ (- 1) = - x.
Lemma mulNrz x n : (- x) *~ n = - (x *~ n).
Lemma mulrzBr x m n : x *~ (m - n) = x *~ m - x *~ n.
Lemma mulrzBl x y n : (x - y) *~ n = x *~ n - y *~ n.
Lemma mulrz_nat (n : nat) x : x *~ n%:R = x *+ n.
Lemma mulrz_sumr : ∀ x I r (P : pred I) F,
x *~ (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x *~ F i.
Lemma mulrz_suml : ∀ n I r (P : pred I) (F : I → M),
(\sum_(i <- r | P i) F i) *~ n= \sum_(i <- r | P i) F i *~ n.
Canonical intmul_additive x := Additive (@mulrzBr x).
End ZintLmod.
#[deprecated(since="mathcomp 2.1.0", note="Use mulrzDr_tmp instead. mulrzDl will be renamed mulrzDr in the future.")]
Notation mulrzDl := mulrzDr_tmp.
#[deprecated(since="mathcomp 2.1.0", note="Use mulrzDl_tmp instead. mulrzDr will be renamed mulrzDl in the future.")]
Notation mulrzDr := mulrzDl_tmp.
Lemma ffunMzE (I : finType) (M : zmodType) (f : {ffun I → M}) z x :
(f *~ z) x = f x *~ z.
Lemma intz (n : int) : n%:~R = n.
Lemma natz (n : nat) : n%:R = n%:Z :> int.
Section RintMod.
Local Coercion Posz : nat >-> int.
Variable R : ringType.
Implicit Types m n : int.
Implicit Types x y z : R.
Lemma mulrzAl n x y : (x *~ n) × y = (x × y) *~ n.
Lemma mulrzAr n x y : x × (y *~ n) = (x × y) *~ n.
Lemma mulrzl x n : n%:~R × x = x *~ n.
Lemma mulrzr x n : x × n%:~R = x *~ n.
Lemma mulNrNz n x : (-x) *~ (-n) = x *~ n.
Lemma mulrbz x (b : bool) : x *~ b = (if b then x else 0).
Lemma intrD m n : (m + n)%:~R = m%:~R + n%:~R :> R.
Lemma intrM m n : (m × n)%:~R = m%:~R × n%:~R :> R.
Lemma intmul1_is_rmorphism : rmorphism ( *~%R (1 : R)).
Canonical intmul1_rmorphism := RMorphism intmul1_is_rmorphism.
Lemma mulr2z n : n *~ 2 = n + n.
End RintMod.
Lemma mulrzz m n : m *~ n = m × n.
Lemma mulz2 n : n × 2%:Z = n + n.
Lemma mul2z n : 2%:Z × n = n + n.
Section LMod.
Variable R : ringType.
Variable V : (lmodType R).
Local Coercion Posz : nat >-> int.
Implicit Types m n : int.
Implicit Types x y z : R.
Implicit Types u v w : V.
Lemma scaler_int n v : n%:~R *: v = v *~ n.
Lemma scalerMzl a v n : (a *: v) *~ n = (a *~ n) *: v.
Lemma scalerMzr a v n : (a *: v) *~ n = a *: (v *~ n).
End LMod.
Lemma mulrz_int (M : zmodType) (n : int) (x : M) : x *~ n%:~R = x *~ n.
Section MorphTheory.
Local Coercion Posz : nat >-> int.
Section Additive.
Variables (U V : zmodType) (f : {additive U → V}).
Lemma raddfMz n : {morph f : x / x *~ n}.
End Additive.
Section Multiplicative.
Variables (R S : ringType) (f : {rmorphism R → S}).
Lemma rmorphMz : ∀ n, {morph f : x / x *~ n}.
Lemma rmorph_int : ∀ n, f n%:~R = n%:~R.
End Multiplicative.
Section Linear.
Variable R : ringType.
Variables (U V : lmodType R) (f : {linear U → V}).
Lemma linearMn : ∀ n, {morph f : x / x *~ n}.
End Linear.
Lemma raddf_int_scalable (aV rV : lmodType int) (f : {additive aV → rV}) :
scalable f.
Section Zintmul1rMorph.
Variable R : ringType.
Lemma commrMz (x y : R) n : GRing.comm x y → GRing.comm x (y *~ n).
Lemma commr_int (x : R) n : GRing.comm x n%:~R.
End Zintmul1rMorph.
Section ZintBigMorphism.
Variable R : ringType.
Lemma sumMz : ∀ I r (P : pred I) F,
(\sum_(i <- r | P i) F i)%N%:~R = \sum_(i <- r | P i) ((F i)%:~R) :> R.
Lemma prodMz : ∀ I r (P : pred I) F,
(\prod_(i <- r | P i) F i)%N%:~R = \prod_(i <- r | P i) ((F i)%:~R) :> R.
End ZintBigMorphism.
Section Frobenius.
Variable R : ringType.
Implicit Types x y : R.
Variable p : nat.
Hypothesis charFp : p \in [char R].
Local Notation "x ^f" := (Frobenius_aut charFp x).
Lemma Frobenius_autMz x n : (x *~ n)^f = x^f *~ n.
Lemma Frobenius_aut_int n : (n%:~R)^f = n%:~R.
End Frobenius.
Section NumMorphism.
Section PO.
Variables (R : numDomainType).
Implicit Types n m : int.
Implicit Types x y : R.
Lemma rmorphzP (f : {rmorphism int → R}) : f =1 ( *~%R 1).
intmul and ler/ltr
Lemma ler_pMz2r n (hn : 0 < n) : {mono *~%R^~ n :x y / x ≤ y :> R}.
Lemma ltr_pMz2r n (hn : 0 < n) : {mono *~%R^~ n : x y / x < y :> R}.
Lemma ler_nMz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x ≤ y :> R}.
Lemma ltr_nMz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x < y :> R}.
Lemma ler_wpMz2r n (hn : 0 ≤ n) : {homo *~%R^~ n : x y / x ≤ y :> R}.
Lemma ler_wnMz2r n (hn : n ≤ 0) : {homo *~%R^~ n : x y /~ x ≤ y :> R}.
Lemma mulrz_ge0 x n (x0 : 0 ≤ x) (n0 : 0 ≤ n) : 0 ≤ x *~ n.
Lemma mulrz_le0 x n (x0 : x ≤ 0) (n0 : n ≤ 0) : 0 ≤ x *~ n.
Lemma mulrz_ge0_le0 x n (x0 : 0 ≤ x) (n0 : n ≤ 0) : x *~ n ≤ 0.
Lemma mulrz_le0_ge0 x n (x0 : x ≤ 0) (n0 : 0 ≤ n) : x *~ n ≤ 0.
Lemma pmulrz_lgt0 x n (n0 : 0 < n) : 0 < x *~ n = (0 < x).
Lemma nmulrz_lgt0 x n (n0 : n < 0) : 0 < x *~ n = (x < 0).
Lemma pmulrz_llt0 x n (n0 : 0 < n) : x *~ n < 0 = (x < 0).
Lemma nmulrz_llt0 x n (n0 : n < 0) : x *~ n < 0 = (0 < x).
Lemma pmulrz_lge0 x n (n0 : 0 < n) : 0 ≤ x *~ n = (0 ≤ x).
Lemma nmulrz_lge0 x n (n0 : n < 0) : 0 ≤ x *~ n = (x ≤ 0).
Lemma pmulrz_lle0 x n (n0 : 0 < n) : x *~ n ≤ 0 = (x ≤ 0).
Lemma nmulrz_lle0 x n (n0 : n < 0) : x *~ n ≤ 0 = (0 ≤ x).
Lemma ler_wpMz2l x (hx : 0 ≤ x) : {homo *~%R x : x y / x ≤ y}.
Lemma ler_wnMz2l x (hx : x ≤ 0) : {homo *~%R x : x y /~ x ≤ y}.
Lemma ler_pMz2l x (hx : 0 < x) : {mono *~%R x : x y / x ≤ y}.
Lemma ler_nMz2l x (hx : x < 0) : {mono *~%R x : x y /~ x ≤ y}.
Lemma ltr_pMz2l x (hx : 0 < x) : {mono *~%R x : x y / x < y}.
Lemma ltr_nMz2l x (hx : x < 0) : {mono *~%R x : x y /~ x < y}.
Lemma pmulrz_rgt0 x n (x0 : 0 < x) : 0 < x *~ n = (0 < n).
Lemma nmulrz_rgt0 x n (x0 : x < 0) : 0 < x *~ n = (n < 0).
Lemma pmulrz_rlt0 x n (x0 : 0 < x) : x *~ n < 0 = (n < 0).
Lemma nmulrz_rlt0 x n (x0 : x < 0) : x *~ n < 0 = (0 < n).
Lemma pmulrz_rge0 x n (x0 : 0 < x) : 0 ≤ x *~ n = (0 ≤ n).
Lemma nmulrz_rge0 x n (x0 : x < 0) : 0 ≤ x *~ n = (n ≤ 0).
Lemma pmulrz_rle0 x n (x0 : 0 < x) : x *~ n ≤ 0 = (n ≤ 0).
Lemma nmulrz_rle0 x n (x0 : x < 0) : x *~ n ≤ 0 = (0 ≤ n).
Lemma mulrIz x (hx : x != 0) : injective ( *~%R x).
Lemma ler_int m n : (m%:~R ≤ n%:~R :> R) = (m ≤ n).
Lemma ltr_int m n : (m%:~R < n%:~R :> R) = (m < n).
Lemma eqr_int m n : (m%:~R == n%:~R :> R) = (m == n).
Lemma ler0z n : (0 ≤ n%:~R :> R) = (0 ≤ n).
Lemma ltr0z n : (0 < n%:~R :> R) = (0 < n).
Lemma lerz0 n : (n%:~R ≤ 0 :> R) = (n ≤ 0).
Lemma ltrz0 n : (n%:~R < 0 :> R) = (n < 0).
Lemma ler1z (n : int) : (1 ≤ n%:~R :> R) = (1 ≤ n).
Lemma ltr1z (n : int) : (1 < n%:~R :> R) = (1 < n).
Lemma lerz1 n : (n%:~R ≤ 1 :> R) = (n ≤ 1).
Lemma ltrz1 n : (n%:~R < 1 :> R) = (n < 1).
Lemma intr_eq0 n : (n%:~R == 0 :> R) = (n == 0).
Lemma mulrz_eq0 x n : (x *~ n == 0) = ((n == 0) || (x == 0)).
Lemma mulrz_neq0 x n : x *~ n != 0 = ((n != 0) && (x != 0)).
Lemma realz n : (n%:~R : R) \in Num.real.
Hint Resolve realz : core.
Definition intr_inj := @mulrIz 1 (oner_neq0 R).
End PO.
End NumMorphism.
End MorphTheory.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pMz2r instead.")]
Notation ler_pmulz2r := ler_pMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pMz2l instead.")]
Notation ler_pmulz2l := ler_pMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpMz2r instead.")]
Notation ler_wpmulz2r := ler_wpMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpMz2l instead.")]
Notation ler_wpmulz2l := ler_wpMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnMz2l instead.")]
Notation ler_wnmulz2l := ler_wnMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nMz2r instead.")]
Notation ler_nmulz2r := ler_nMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nMz2l instead.")]
Notation ler_nmulz2l := ler_nMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pMz2r instead.")]
Notation ltr_pmulz2r := ltr_pMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pMz2l instead.")]
Notation ltr_pmulz2l := ltr_pMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nMz2r instead.")]
Notation ltr_nmulz2r := ltr_nMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nMz2l instead.")]
Notation ltr_nmulz2l := ltr_nMz2l.
Arguments intr_inj {R} [x1 x2].
Definition exprz (R : unitRingType) (x : R) (n : int) := nosimpl
match n with
| Posz n ⇒ x ^+ n
| Negz n ⇒ x ^- (n.+1)
end.
Notation "x ^ n" := (exprz x n) : ring_scope.
Section ExprzUnitRing.
Variable R : unitRingType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma exprnP x (n : nat) : x ^+ n = x ^ n.
Lemma exprnN x (n : nat) : x ^- n = x ^ -n%:Z.
Lemma expr0z x : x ^ 0 = 1.
Lemma expr1z x : x ^ 1 = x.
Lemma exprN1 x : x ^ (-1) = x^-1.
Lemma invr_expz x n : (x ^ n)^-1 = x ^ (- n).
Lemma exprz_inv x n : (x^-1) ^ n = x ^ (- n).
Lemma exp1rz n : 1 ^ n = 1 :> R.
Lemma exprSz x (n : nat) : x ^ n.+1 = x × x ^ n.
Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n × x.
Fact exprzD_nat x (m n : nat) : x ^ (m%:Z + n) = x ^ m × x ^ n.
Fact exprzD_Nnat x (m n : nat) : x ^ (-m%:Z + -n%:Z) = x ^ (-m%:Z) × x ^ (-n%:Z).
Lemma exprzD_ss x m n : (0 ≤ m) && (0 ≤ n) || (m ≤ 0) && (n ≤ 0)
→ x ^ (m + n) = x ^ m × x ^ n.
Lemma exp0rz n : 0 ^ n = (n == 0)%:~R :> R.
Lemma commrXz x y n : GRing.comm x y → GRing.comm x (y ^ n).
Lemma exprMz_comm x y n : x \is a GRing.unit → y \is a GRing.unit →
GRing.comm x y → (x × y) ^ n = x ^ n × y ^ n.
Lemma commrXz_wmulls x y n :
0 ≤ n → GRing.comm x y → (x × y) ^ n = x ^ n × y ^ n.
Lemma unitrXz x n (ux : x \is a GRing.unit) : x ^ n \is a GRing.unit.
Lemma exprzDr x (ux : x \is a GRing.unit) m n : x ^ (m + n) = x ^ m × x ^ n.
Lemma exprz_exp x m n : (x ^ m) ^ n = (x ^ (m × n)).
Lemma exprzAC x m n : (x ^ m) ^ n = (x ^ n) ^ m.
Lemma exprz_out x n (nux : x \isn't a GRing.unit) (hn : 0 ≤ n) :
x ^ (- n) = x ^ n.
End ExprzUnitRing.
Section Exprz_Zint_UnitRing.
Variable R : unitRingType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma exprz_pMzl x m n : 0 ≤ n → (x *~ m) ^ n = x ^ n *~ (m ^ n).
Lemma exprz_pintl m n (hn : 0 ≤ n) : m%:~R ^ n = (m ^ n)%:~R :> R.
Lemma exprzMzl x m n (ux : x \is a GRing.unit) (um : m%:~R \is a @GRing.unit R):
(x *~ m) ^ n = (m%:~R ^ n) × x ^ n :> R.
Lemma expNrz x n : (- x) ^ n = (-1) ^ n × x ^ n :> R.
Lemma unitr_n0expz x n :
n != 0 → (x ^ n \is a GRing.unit) = (x \is a GRing.unit).
Lemma intrV (n : int) :
n \in [:: 0; 1; -1] → n%:~R ^-1 = n%:~R :> R.
Lemma rmorphXz (R' : unitRingType) (f : {rmorphism R → R'}) n :
{in GRing.unit, {morph f : x / x ^ n}}.
End Exprz_Zint_UnitRing.
Section ExprzIdomain.
Variable R : idomainType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma expfz_eq0 x n : (x ^ n == 0) = (n != 0) && (x == 0).
Lemma expfz_neq0 x n : x != 0 → x ^ n != 0.
Lemma exprzMl x y n (ux : x \is a GRing.unit) (uy : y \is a GRing.unit) :
(x × y) ^ n = x ^ n × y ^ n.
Lemma expfV (x : R) (i : int) : (x ^ i) ^-1 = (x ^-1) ^ i.
End ExprzIdomain.
Section ExprzField.
Variable F : fieldType.
Implicit Types x y : F.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma expfzDr x m n : x != 0 → x ^ (m + n) = x ^ m × x ^ n.
Lemma expfz_n0addr x m n : m + n != 0 → x ^ (m + n) = x ^ m × x ^ n.
Lemma expfzMl x y n : (x × y) ^ n = x ^ n × y ^ n.
Lemma fmorphXz (R : unitRingType) (f : {rmorphism F → R}) n :
{morph f : x / x ^ n}.
End ExprzField.
Section ExprzOrder.
Variable R : realFieldType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma ltr_pMz2r n (hn : 0 < n) : {mono *~%R^~ n : x y / x < y :> R}.
Lemma ler_nMz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x ≤ y :> R}.
Lemma ltr_nMz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x < y :> R}.
Lemma ler_wpMz2r n (hn : 0 ≤ n) : {homo *~%R^~ n : x y / x ≤ y :> R}.
Lemma ler_wnMz2r n (hn : n ≤ 0) : {homo *~%R^~ n : x y /~ x ≤ y :> R}.
Lemma mulrz_ge0 x n (x0 : 0 ≤ x) (n0 : 0 ≤ n) : 0 ≤ x *~ n.
Lemma mulrz_le0 x n (x0 : x ≤ 0) (n0 : n ≤ 0) : 0 ≤ x *~ n.
Lemma mulrz_ge0_le0 x n (x0 : 0 ≤ x) (n0 : n ≤ 0) : x *~ n ≤ 0.
Lemma mulrz_le0_ge0 x n (x0 : x ≤ 0) (n0 : 0 ≤ n) : x *~ n ≤ 0.
Lemma pmulrz_lgt0 x n (n0 : 0 < n) : 0 < x *~ n = (0 < x).
Lemma nmulrz_lgt0 x n (n0 : n < 0) : 0 < x *~ n = (x < 0).
Lemma pmulrz_llt0 x n (n0 : 0 < n) : x *~ n < 0 = (x < 0).
Lemma nmulrz_llt0 x n (n0 : n < 0) : x *~ n < 0 = (0 < x).
Lemma pmulrz_lge0 x n (n0 : 0 < n) : 0 ≤ x *~ n = (0 ≤ x).
Lemma nmulrz_lge0 x n (n0 : n < 0) : 0 ≤ x *~ n = (x ≤ 0).
Lemma pmulrz_lle0 x n (n0 : 0 < n) : x *~ n ≤ 0 = (x ≤ 0).
Lemma nmulrz_lle0 x n (n0 : n < 0) : x *~ n ≤ 0 = (0 ≤ x).
Lemma ler_wpMz2l x (hx : 0 ≤ x) : {homo *~%R x : x y / x ≤ y}.
Lemma ler_wnMz2l x (hx : x ≤ 0) : {homo *~%R x : x y /~ x ≤ y}.
Lemma ler_pMz2l x (hx : 0 < x) : {mono *~%R x : x y / x ≤ y}.
Lemma ler_nMz2l x (hx : x < 0) : {mono *~%R x : x y /~ x ≤ y}.
Lemma ltr_pMz2l x (hx : 0 < x) : {mono *~%R x : x y / x < y}.
Lemma ltr_nMz2l x (hx : x < 0) : {mono *~%R x : x y /~ x < y}.
Lemma pmulrz_rgt0 x n (x0 : 0 < x) : 0 < x *~ n = (0 < n).
Lemma nmulrz_rgt0 x n (x0 : x < 0) : 0 < x *~ n = (n < 0).
Lemma pmulrz_rlt0 x n (x0 : 0 < x) : x *~ n < 0 = (n < 0).
Lemma nmulrz_rlt0 x n (x0 : x < 0) : x *~ n < 0 = (0 < n).
Lemma pmulrz_rge0 x n (x0 : 0 < x) : 0 ≤ x *~ n = (0 ≤ n).
Lemma nmulrz_rge0 x n (x0 : x < 0) : 0 ≤ x *~ n = (n ≤ 0).
Lemma pmulrz_rle0 x n (x0 : 0 < x) : x *~ n ≤ 0 = (n ≤ 0).
Lemma nmulrz_rle0 x n (x0 : x < 0) : x *~ n ≤ 0 = (0 ≤ n).
Lemma mulrIz x (hx : x != 0) : injective ( *~%R x).
Lemma ler_int m n : (m%:~R ≤ n%:~R :> R) = (m ≤ n).
Lemma ltr_int m n : (m%:~R < n%:~R :> R) = (m < n).
Lemma eqr_int m n : (m%:~R == n%:~R :> R) = (m == n).
Lemma ler0z n : (0 ≤ n%:~R :> R) = (0 ≤ n).
Lemma ltr0z n : (0 < n%:~R :> R) = (0 < n).
Lemma lerz0 n : (n%:~R ≤ 0 :> R) = (n ≤ 0).
Lemma ltrz0 n : (n%:~R < 0 :> R) = (n < 0).
Lemma ler1z (n : int) : (1 ≤ n%:~R :> R) = (1 ≤ n).
Lemma ltr1z (n : int) : (1 < n%:~R :> R) = (1 < n).
Lemma lerz1 n : (n%:~R ≤ 1 :> R) = (n ≤ 1).
Lemma ltrz1 n : (n%:~R < 1 :> R) = (n < 1).
Lemma intr_eq0 n : (n%:~R == 0 :> R) = (n == 0).
Lemma mulrz_eq0 x n : (x *~ n == 0) = ((n == 0) || (x == 0)).
Lemma mulrz_neq0 x n : x *~ n != 0 = ((n != 0) && (x != 0)).
Lemma realz n : (n%:~R : R) \in Num.real.
Hint Resolve realz : core.
Definition intr_inj := @mulrIz 1 (oner_neq0 R).
End PO.
End NumMorphism.
End MorphTheory.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pMz2r instead.")]
Notation ler_pmulz2r := ler_pMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pMz2l instead.")]
Notation ler_pmulz2l := ler_pMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpMz2r instead.")]
Notation ler_wpmulz2r := ler_wpMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpMz2l instead.")]
Notation ler_wpmulz2l := ler_wpMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnMz2l instead.")]
Notation ler_wnmulz2l := ler_wnMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nMz2r instead.")]
Notation ler_nmulz2r := ler_nMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nMz2l instead.")]
Notation ler_nmulz2l := ler_nMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pMz2r instead.")]
Notation ltr_pmulz2r := ltr_pMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pMz2l instead.")]
Notation ltr_pmulz2l := ltr_pMz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nMz2r instead.")]
Notation ltr_nmulz2r := ltr_nMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nMz2l instead.")]
Notation ltr_nmulz2l := ltr_nMz2l.
Arguments intr_inj {R} [x1 x2].
Definition exprz (R : unitRingType) (x : R) (n : int) := nosimpl
match n with
| Posz n ⇒ x ^+ n
| Negz n ⇒ x ^- (n.+1)
end.
Notation "x ^ n" := (exprz x n) : ring_scope.
Section ExprzUnitRing.
Variable R : unitRingType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma exprnP x (n : nat) : x ^+ n = x ^ n.
Lemma exprnN x (n : nat) : x ^- n = x ^ -n%:Z.
Lemma expr0z x : x ^ 0 = 1.
Lemma expr1z x : x ^ 1 = x.
Lemma exprN1 x : x ^ (-1) = x^-1.
Lemma invr_expz x n : (x ^ n)^-1 = x ^ (- n).
Lemma exprz_inv x n : (x^-1) ^ n = x ^ (- n).
Lemma exp1rz n : 1 ^ n = 1 :> R.
Lemma exprSz x (n : nat) : x ^ n.+1 = x × x ^ n.
Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n × x.
Fact exprzD_nat x (m n : nat) : x ^ (m%:Z + n) = x ^ m × x ^ n.
Fact exprzD_Nnat x (m n : nat) : x ^ (-m%:Z + -n%:Z) = x ^ (-m%:Z) × x ^ (-n%:Z).
Lemma exprzD_ss x m n : (0 ≤ m) && (0 ≤ n) || (m ≤ 0) && (n ≤ 0)
→ x ^ (m + n) = x ^ m × x ^ n.
Lemma exp0rz n : 0 ^ n = (n == 0)%:~R :> R.
Lemma commrXz x y n : GRing.comm x y → GRing.comm x (y ^ n).
Lemma exprMz_comm x y n : x \is a GRing.unit → y \is a GRing.unit →
GRing.comm x y → (x × y) ^ n = x ^ n × y ^ n.
Lemma commrXz_wmulls x y n :
0 ≤ n → GRing.comm x y → (x × y) ^ n = x ^ n × y ^ n.
Lemma unitrXz x n (ux : x \is a GRing.unit) : x ^ n \is a GRing.unit.
Lemma exprzDr x (ux : x \is a GRing.unit) m n : x ^ (m + n) = x ^ m × x ^ n.
Lemma exprz_exp x m n : (x ^ m) ^ n = (x ^ (m × n)).
Lemma exprzAC x m n : (x ^ m) ^ n = (x ^ n) ^ m.
Lemma exprz_out x n (nux : x \isn't a GRing.unit) (hn : 0 ≤ n) :
x ^ (- n) = x ^ n.
End ExprzUnitRing.
Section Exprz_Zint_UnitRing.
Variable R : unitRingType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma exprz_pMzl x m n : 0 ≤ n → (x *~ m) ^ n = x ^ n *~ (m ^ n).
Lemma exprz_pintl m n (hn : 0 ≤ n) : m%:~R ^ n = (m ^ n)%:~R :> R.
Lemma exprzMzl x m n (ux : x \is a GRing.unit) (um : m%:~R \is a @GRing.unit R):
(x *~ m) ^ n = (m%:~R ^ n) × x ^ n :> R.
Lemma expNrz x n : (- x) ^ n = (-1) ^ n × x ^ n :> R.
Lemma unitr_n0expz x n :
n != 0 → (x ^ n \is a GRing.unit) = (x \is a GRing.unit).
Lemma intrV (n : int) :
n \in [:: 0; 1; -1] → n%:~R ^-1 = n%:~R :> R.
Lemma rmorphXz (R' : unitRingType) (f : {rmorphism R → R'}) n :
{in GRing.unit, {morph f : x / x ^ n}}.
End Exprz_Zint_UnitRing.
Section ExprzIdomain.
Variable R : idomainType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma expfz_eq0 x n : (x ^ n == 0) = (n != 0) && (x == 0).
Lemma expfz_neq0 x n : x != 0 → x ^ n != 0.
Lemma exprzMl x y n (ux : x \is a GRing.unit) (uy : y \is a GRing.unit) :
(x × y) ^ n = x ^ n × y ^ n.
Lemma expfV (x : R) (i : int) : (x ^ i) ^-1 = (x ^-1) ^ i.
End ExprzIdomain.
Section ExprzField.
Variable F : fieldType.
Implicit Types x y : F.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
Lemma expfzDr x m n : x != 0 → x ^ (m + n) = x ^ m × x ^ n.
Lemma expfz_n0addr x m n : m + n != 0 → x ^ (m + n) = x ^ m × x ^ n.
Lemma expfzMl x y n : (x × y) ^ n = x ^ n × y ^ n.
Lemma fmorphXz (R : unitRingType) (f : {rmorphism F → R}) n :
{morph f : x / x ^ n}.
End ExprzField.
Section ExprzOrder.
Variable R : realFieldType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> int.
ler and exprz
Lemma exprz_ge0 n x (hx : 0 ≤ x) : (0 ≤ x ^ n).
Lemma exprz_gt0 n x (hx : 0 < x) : (0 < x ^ n).
Definition exprz_gte0 := (exprz_ge0, exprz_gt0).
Lemma ler_wpiXz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
{in ≥ 0 &, {homo exprz x : x y /~ x ≤ y}}.
Lemma ler_wniXz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
{in < 0 &, {homo exprz x : x y /~ x ≤ y}}.
Fact ler_wpeXz2l x (x1 : 1 ≤ x) : {in ≥ 0 &, {homo exprz x : x y / x ≤ y}}.
Fact ler_wneXz2l x (x1 : 1 ≤ x) : {in ≤ 0 &, {homo exprz x : x y / x ≤ y}}.
Lemma ler_weXz2l x (x1 : 1 ≤ x) : {homo exprz x : x y / x ≤ y}.
Lemma pexprz_eq1 x n (x0 : 0 ≤ x) : (x ^ n == 1) = ((n == 0) || (x == 1)).
Lemma ieexprIz x (x0 : 0 < x) (nx1 : x != 1) : injective (exprz x).
Lemma ler_piXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in ≥ 0 &, {mono exprz x : x y /~ x ≤ y}}.
Lemma ltr_piXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in ≥ 0 &, {mono exprz x : x y /~ x < y}}.
Lemma ler_niXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono exprz x : x y /~ x ≤ y}}.
Lemma ltr_niXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono (exprz x) : x y /~ x < y}}.
Lemma ler_eXz2l x (x1 : 1 < x) : {mono exprz x : x y / x ≤ y}.
Lemma ltr_eXz2l x (x1 : 1 < x) : {mono exprz x : x y / x < y}.
Lemma ler_wpXz2r n (hn : 0 ≤ n) :
{in ≥ 0 & , {homo (@exprz R)^~ n : x y / x ≤ y}}.
Lemma ler_wnXz2r n (hn : n ≤ 0) :
{in > 0 & , {homo (@exprz R)^~ n : x y /~ x ≤ y}}.
Lemma pexpIrz n (n0 : n != 0) : {in ≥ 0 &, injective ((@exprz R)^~ n)}.
Lemma nexpIrz n (n0 : n != 0) : {in ≤ 0 &, injective ((@exprz R)^~ n)}.
Lemma ler_pXz2r n (hn : 0 < n) :
{in ≥ 0 & , {mono ((@exprz R)^~ n) : x y / x ≤ y}}.
Lemma ltr_pXz2r n (hn : 0 < n) :
{in ≥ 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}.
Lemma ler_nXz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x ≤ y}}.
Lemma ltr_nXz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x < y}}.
Lemma eqrXz2 n x y : n != 0 → 0 ≤ x → 0 ≤ y → (x ^ n == y ^ n) = (x == y).
End ExprzOrder.
Local Notation sgr := Num.sg.
Section Sgz.
Variable R : numDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Local Coercion Posz : nat >-> int.
Definition sgz x : int := if x == 0 then 0 else if x < 0 then -1 else 1.
Lemma sgz_def x : sgz x = (-1) ^+ (x < 0)%R *+ (x != 0).
Lemma sgrEz x : sgr x = (sgz x)%:~R.
Lemma gtr0_sgz x : 0 < x → sgz x = 1.
Lemma ltr0_sgz x : x < 0 → sgz x = -1.
Lemma sgz0 : sgz (0 : R) = 0.
Lemma sgz1 : sgz (1 : R) = 1.
Lemma sgzN1 : sgz (-1 : R) = -1.
Definition sgzE := (sgz0, sgz1, sgzN1).
Lemma sgz_sgr x : sgz (sgr x) = sgz x.
Lemma normr_sgz x : `|sgz x| = (x != 0).
Lemma normr_sg x : `|sgr x| = (x != 0)%:~R.
End Sgz.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnMz2r instead.")]
Notation ler_wnmulz2r := ler_wnMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpXz2r instead.")]
Notation ler_wpexpz2r := ler_wpXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnXz2r instead.")]
Notation ler_wnexpz2r := ler_wnXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pXz2r instead.")]
Notation ler_pexpz2r := ler_pXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pXz2r instead.")]
Notation ltr_pexpz2r := ltr_pXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nXz2r instead.")]
Notation ler_nexpz2r := ler_nXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nXz2r instead.")]
Notation ltr_nexpz2r := ltr_nXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpiXz2l instead.")]
Notation ler_wpiexpz2l := ler_wpiXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wniXz2l instead.")]
Notation ler_wniexpz2l := ler_wniXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpeXz2l instead.")]
Notation ler_wpeexpz2l := ler_wpeXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wneXz2l instead.")]
Notation ler_wneexpz2l := ler_wneXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_weXz2l instead.")]
Notation ler_weexpz2l := ler_weXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_piXz2l instead.")]
Notation ler_piexpz2l := ler_piXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_piXz2l instead.")]
Notation ltr_piexpz2l := ltr_piXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_niXz2l instead.")]
Notation ler_niexpz2l := ler_niXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_niXz2l instead.")]
Notation ltr_niexpz2l := ltr_niXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_eXz2l instead.")]
Notation ler_eexpz2l := ler_eXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_eXz2l instead.")]
Notation ltr_eexpz2l := ltr_eXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use eqrXz2 instead.")]
Notation eqr_expz2 := eqrXz2.
#[deprecated(since="mathcomp 1.17.0", note="Use exprz_pMzl instead.")]
Notation exprz_pmulzl := exprz_pMzl.
Section MoreSgz.
Variable R : numDomainType.
Lemma sgz_int m : sgz (m%:~R : R) = sgz m.
Lemma sgrz (n : int) : sgr n = sgz n.
Lemma intr_sg m : (sgr m)%:~R = sgr (m%:~R) :> R.
Lemma sgz_id (x : R) : sgz (sgz x) = sgz x.
End MoreSgz.
Section SgzReal.
Variable R : realDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Local Coercion Posz : nat >-> int.
Lemma sgz_cp0 x :
((sgz x == 1) = (0 < x)) ×
((sgz x == -1) = (x < 0)) ×
((sgz x == 0) = (x == 0)).
Variant sgz_val x : bool → bool → bool → bool → bool → bool
→ bool → bool → bool → bool → bool → bool
→ bool → bool → bool → bool → bool → bool
→ R → R → int → Set :=
| SgzNull of x = 0 : sgz_val x true true true true false false
true false false true false false true false false true false false 0 0 0
| SgzPos of x > 0 : sgz_val x false false true false false true
false false true false false true false false true false false true x 1 1
| SgzNeg of x < 0 : sgz_val x false true false false true false
false true false false true false false true false false true false (-x) (-1) (-1).
Lemma sgzP x :
sgz_val x (0 == x) (x ≤ 0) (0 ≤ x) (x == 0) (x < 0) (0 < x)
(0 == sgr x) (-1 == sgr x) (1 == sgr x)
(sgr x == 0) (sgr x == -1) (sgr x == 1)
(0 == sgz x) (-1 == sgz x) (1 == sgz x)
(sgz x == 0) (sgz x == -1) (sgz x == 1) `|x| (sgr x) (sgz x).
Lemma sgzN x : sgz (- x) = - sgz x.
Lemma mulz_sg x : sgz x × sgz x = (x != 0)%:~R.
Lemma mulz_sg_eq1 x y : (sgz x × sgz y == 1) = (x != 0) && (sgz x == sgz y).
Lemma mulz_sg_eqN1 x y : (sgz x × sgz y == -1) = (x != 0) && (sgz x == - sgz y).
Lemma exprz_gt0 n x (hx : 0 < x) : (0 < x ^ n).
Definition exprz_gte0 := (exprz_ge0, exprz_gt0).
Lemma ler_wpiXz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
{in ≥ 0 &, {homo exprz x : x y /~ x ≤ y}}.
Lemma ler_wniXz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
{in < 0 &, {homo exprz x : x y /~ x ≤ y}}.
Fact ler_wpeXz2l x (x1 : 1 ≤ x) : {in ≥ 0 &, {homo exprz x : x y / x ≤ y}}.
Fact ler_wneXz2l x (x1 : 1 ≤ x) : {in ≤ 0 &, {homo exprz x : x y / x ≤ y}}.
Lemma ler_weXz2l x (x1 : 1 ≤ x) : {homo exprz x : x y / x ≤ y}.
Lemma pexprz_eq1 x n (x0 : 0 ≤ x) : (x ^ n == 1) = ((n == 0) || (x == 1)).
Lemma ieexprIz x (x0 : 0 < x) (nx1 : x != 1) : injective (exprz x).
Lemma ler_piXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in ≥ 0 &, {mono exprz x : x y /~ x ≤ y}}.
Lemma ltr_piXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in ≥ 0 &, {mono exprz x : x y /~ x < y}}.
Lemma ler_niXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono exprz x : x y /~ x ≤ y}}.
Lemma ltr_niXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono (exprz x) : x y /~ x < y}}.
Lemma ler_eXz2l x (x1 : 1 < x) : {mono exprz x : x y / x ≤ y}.
Lemma ltr_eXz2l x (x1 : 1 < x) : {mono exprz x : x y / x < y}.
Lemma ler_wpXz2r n (hn : 0 ≤ n) :
{in ≥ 0 & , {homo (@exprz R)^~ n : x y / x ≤ y}}.
Lemma ler_wnXz2r n (hn : n ≤ 0) :
{in > 0 & , {homo (@exprz R)^~ n : x y /~ x ≤ y}}.
Lemma pexpIrz n (n0 : n != 0) : {in ≥ 0 &, injective ((@exprz R)^~ n)}.
Lemma nexpIrz n (n0 : n != 0) : {in ≤ 0 &, injective ((@exprz R)^~ n)}.
Lemma ler_pXz2r n (hn : 0 < n) :
{in ≥ 0 & , {mono ((@exprz R)^~ n) : x y / x ≤ y}}.
Lemma ltr_pXz2r n (hn : 0 < n) :
{in ≥ 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}.
Lemma ler_nXz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x ≤ y}}.
Lemma ltr_nXz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x < y}}.
Lemma eqrXz2 n x y : n != 0 → 0 ≤ x → 0 ≤ y → (x ^ n == y ^ n) = (x == y).
End ExprzOrder.
Local Notation sgr := Num.sg.
Section Sgz.
Variable R : numDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Local Coercion Posz : nat >-> int.
Definition sgz x : int := if x == 0 then 0 else if x < 0 then -1 else 1.
Lemma sgz_def x : sgz x = (-1) ^+ (x < 0)%R *+ (x != 0).
Lemma sgrEz x : sgr x = (sgz x)%:~R.
Lemma gtr0_sgz x : 0 < x → sgz x = 1.
Lemma ltr0_sgz x : x < 0 → sgz x = -1.
Lemma sgz0 : sgz (0 : R) = 0.
Lemma sgz1 : sgz (1 : R) = 1.
Lemma sgzN1 : sgz (-1 : R) = -1.
Definition sgzE := (sgz0, sgz1, sgzN1).
Lemma sgz_sgr x : sgz (sgr x) = sgz x.
Lemma normr_sgz x : `|sgz x| = (x != 0).
Lemma normr_sg x : `|sgr x| = (x != 0)%:~R.
End Sgz.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnMz2r instead.")]
Notation ler_wnmulz2r := ler_wnMz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpXz2r instead.")]
Notation ler_wpexpz2r := ler_wpXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnXz2r instead.")]
Notation ler_wnexpz2r := ler_wnXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pXz2r instead.")]
Notation ler_pexpz2r := ler_pXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pXz2r instead.")]
Notation ltr_pexpz2r := ltr_pXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nXz2r instead.")]
Notation ler_nexpz2r := ler_nXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nXz2r instead.")]
Notation ltr_nexpz2r := ltr_nXz2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpiXz2l instead.")]
Notation ler_wpiexpz2l := ler_wpiXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wniXz2l instead.")]
Notation ler_wniexpz2l := ler_wniXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpeXz2l instead.")]
Notation ler_wpeexpz2l := ler_wpeXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wneXz2l instead.")]
Notation ler_wneexpz2l := ler_wneXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_weXz2l instead.")]
Notation ler_weexpz2l := ler_weXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_piXz2l instead.")]
Notation ler_piexpz2l := ler_piXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_piXz2l instead.")]
Notation ltr_piexpz2l := ltr_piXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_niXz2l instead.")]
Notation ler_niexpz2l := ler_niXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_niXz2l instead.")]
Notation ltr_niexpz2l := ltr_niXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_eXz2l instead.")]
Notation ler_eexpz2l := ler_eXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_eXz2l instead.")]
Notation ltr_eexpz2l := ltr_eXz2l.
#[deprecated(since="mathcomp 1.17.0", note="Use eqrXz2 instead.")]
Notation eqr_expz2 := eqrXz2.
#[deprecated(since="mathcomp 1.17.0", note="Use exprz_pMzl instead.")]
Notation exprz_pmulzl := exprz_pMzl.
Section MoreSgz.
Variable R : numDomainType.
Lemma sgz_int m : sgz (m%:~R : R) = sgz m.
Lemma sgrz (n : int) : sgr n = sgz n.
Lemma intr_sg m : (sgr m)%:~R = sgr (m%:~R) :> R.
Lemma sgz_id (x : R) : sgz (sgz x) = sgz x.
End MoreSgz.
Section SgzReal.
Variable R : realDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Local Coercion Posz : nat >-> int.
Lemma sgz_cp0 x :
((sgz x == 1) = (0 < x)) ×
((sgz x == -1) = (x < 0)) ×
((sgz x == 0) = (x == 0)).
Variant sgz_val x : bool → bool → bool → bool → bool → bool
→ bool → bool → bool → bool → bool → bool
→ bool → bool → bool → bool → bool → bool
→ R → R → int → Set :=
| SgzNull of x = 0 : sgz_val x true true true true false false
true false false true false false true false false true false false 0 0 0
| SgzPos of x > 0 : sgz_val x false false true false false true
false false true false false true false false true false false true x 1 1
| SgzNeg of x < 0 : sgz_val x false true false false true false
false true false false true false false true false false true false (-x) (-1) (-1).
Lemma sgzP x :
sgz_val x (0 == x) (x ≤ 0) (0 ≤ x) (x == 0) (x < 0) (0 < x)
(0 == sgr x) (-1 == sgr x) (1 == sgr x)
(sgr x == 0) (sgr x == -1) (sgr x == 1)
(0 == sgz x) (-1 == sgz x) (1 == sgz x)
(sgz x == 0) (sgz x == -1) (sgz x == 1) `|x| (sgr x) (sgz x).
Lemma sgzN x : sgz (- x) = - sgz x.
Lemma mulz_sg x : sgz x × sgz x = (x != 0)%:~R.
Lemma mulz_sg_eq1 x y : (sgz x × sgz y == 1) = (x != 0) && (sgz x == sgz y).
Lemma mulz_sg_eqN1 x y : (sgz x × sgz y == -1) = (x != 0) && (sgz x == - sgz y).
Lemma muls_eqA x y z : sgr x != 0 ->
(sgr y * sgr z == sgr x) = ((sgr y * sgr x == sgr z) && (sgr z != 0)).
Proof. by do 3!case: sgrP=> _. Qed.
Lemma sgzM x y : sgz (x × y) = sgz x × sgz y.
Lemma sgzX (n : nat) x : sgz (x ^+ n) = (sgz x) ^+ n.
Lemma sgz_eq0 x : (sgz x == 0) = (x == 0).
Lemma sgz_odd (n : nat) x : x != 0 → (sgz x) ^+ n = (sgz x) ^+ (odd n).
Lemma sgz_gt0 x : (sgz x > 0) = (x > 0).
Lemma sgz_lt0 x : (sgz x < 0) = (x < 0).
Lemma sgz_ge0 x : (sgz x ≥ 0) = (x ≥ 0).
Lemma sgz_le0 x : (sgz x ≤ 0) = (x ≤ 0).
Lemma sgz_smul x y : sgz (y *~ (sgz x)) = (sgz x) × (sgz y).
Lemma sgrMz m x : sgr (x *~ m) = sgr x *~ sgr m.
End SgzReal.
Lemma sgz_eq (R R' : realDomainType) (x : R) (y : R') :
(sgz x == sgz y) = ((x == 0) == (y == 0)) && ((0 < x) == (0 < y)).
Lemma intr_sign (R : ringType) s : ((-1) ^+ s)%:~R = (-1) ^+ s :> R.
Section Absz.
Implicit Types m n p : int.
Open Scope nat_scope.
Local Coercion Posz : nat >-> int.
Lemma absz_nat (n : nat) : `|n| = n.
Lemma abszE (m : int) : `|m| = `|m|%R :> int.
Lemma absz0 : `|0%R| = 0.
Lemma abszN m : `|- m| = `|m|.
Lemma absz_eq0 m : (`|m| == 0) = (m == 0%R).
Lemma absz_gt0 m : (`|m| > 0) = (m != 0%R).
Lemma absz1 : `|1%R| = 1.
Lemma abszN1 : `|-1%R| = 1.
Lemma absz_id m : `|(`|m|)| = `|m|.
Lemma abszM m1 m2 : `|(m1 × m2)%R| = `|m1| × `|m2|.
Lemma abszX (n : nat) m : `|m ^+ n| = `|m| ^ n.
Lemma absz_sg m : `|sgr m| = (m != 0%R).
Lemma gez0_abs m : (0 ≤ m)%R → `|m| = m :> int.
Lemma gtz0_abs m : (0 < m)%R → `|m| = m :> int.
Lemma lez0_abs m : (m ≤ 0)%R → `|m| = - m :> int.
Lemma ltz0_abs m : (m < 0)%R → `|m| = - m :> int.
Lemma lez_abs m : m ≤ `|m|%N :> int.
Lemma absz_sign s : `|(-1) ^+ s| = 1.
Lemma abszMsign s m : `|((-1) ^+ s × m)%R| = `|m|.
Lemma mulz_sign_abs m : ((-1) ^+ (m < 0)%R × `|m|%:Z)%R = m.
Lemma mulz_Nsign_abs m : ((-1) ^+ (0 < m)%R × `|m|%:Z)%R = - m.
Lemma intEsign m : m = ((-1) ^+ (m < 0)%R × `|m|%:Z)%R.
Lemma abszEsign m : `|m|%:Z = ((-1) ^+ (m < 0)%R × m)%R.
Lemma intEsg m : m = (sgz m × `|m|%:Z)%R.
Lemma abszEsg m : (`|m|%:Z = sgz m × m)%R.
End Absz.
Section MoreAbsz.
Variable R : numDomainType.
Implicit Type i : int.
Lemma mulr_absz (x : R) i : x *+ `|i| = x *~ `|i|.
Lemma natr_absz i : `|i|%:R = `|i|%:~R :> R.
End MoreAbsz.
Module Export IntDist.
Notation "m - n" :=
(@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
Arguments absz m%distn_scope.
Notation "`| m |" := (absz m) : nat_scope.
Coercion Posz : nat >-> int.
Section Distn.
Open Scope nat_scope.
Implicit Type m : int.
Implicit Types n d : nat.
Lemma distnC m1 m2 : `|m1 - m2| = `|m2 - m1|.
Lemma distnDl d n1 n2 : `|d + n1 - (d + n2)| = `|n1 - n2|.
Lemma distnDr d n1 n2 : `|n1 + d - (n2 + d)| = `|n1 - n2|.
Lemma distnEr n1 n2 : n1 ≤ n2 → `|n1 - n2| = n2 - n1.
Lemma distnEl n1 n2 : n2 ≤ n1 → `|n1 - n2| = n1 - n2.
Lemma distn0 n : `|n - 0| = n.
Lemma dist0n n : `|0 - n| = n.
Lemma distnn m : `|m - m| = 0.
Lemma distn_eq0 n1 n2 : (`|n1 - n2| == 0) = (n1 == n2).
Lemma distnS n : `|n - n.+1| = 1.
Lemma distSn n : `|n.+1 - n| = 1.
Lemma distn_eq1 n1 n2 :
(`|n1 - n2| == 1) = (if n1 < n2 then n1.+1 == n2 else n1 == n2.+1).
Lemma leqD_dist m1 m2 m3 : `|m1 - m3| ≤ `|m1 - m2| + `|m2 - m3|.
Most of this proof generalizes to all real-ordered rings.
Lemma leqifD_distz m1 m2 m3 :
`|m1 - m3| ≤ `|m1 - m2| + `|m2 - m3|
?= iff (m1 ≤ m2 ≤ m3)%R || (m3 ≤ m2 ≤ m1)%R.
Lemma leqifD_dist n1 n2 n3 :
`|n1 - n3| ≤ `|n1 - n2| + `|n2 - n3|
?= iff (n1 ≤ n2 ≤ n3) || (n3 ≤ n2 ≤ n1).
Lemma sqrn_dist n1 n2 : `|n1 - n2| ^ 2 + 2 × (n1 × n2) = n1 ^ 2 + n2 ^ 2.
End Distn.
End IntDist.
#[deprecated(since="mathcomp 1.17.0", note="Use leqD_dist instead.")]
Notation leq_add_dist := leqD_dist.
#[deprecated(since="mathcomp 1.17.0", note="Use leqifD_distz instead.")]
Notation leqif_add_distz := leqifD_distz.
#[deprecated(since="mathcomp 1.17.0", note="Use leqifD_dist instead.")]
Notation leqif_add_dist := leqifD_dist.
Section NormInt.
Variable R : numDomainType.
Lemma intr_norm m : `|m|%:~R = `|m%:~R : R|.
Lemma normrMz m (x : R) : `|x *~ m| = `|x| *~ `|m|.
Lemma expN1r (i : int) : (-1 : R) ^ i = (-1) ^+ `|i|.
End NormInt.
Section PolyZintRing.
Variable R : ringType.
Implicit Types x y z: R.
Implicit Types m n : int.
Implicit Types i j k : nat.
Implicit Types p q r : {poly R}.
Lemma coefMrz p n i : (p *~ n)`_i = (p`_i *~ n).
Lemma polyCMz n : {morph (@polyC R) : c / c *~ n}.
Lemma hornerMz n p x : (p *~ n).[x] = p.[x] *~ n.
Lemma horner_int n x : (n%:~R : {poly R}).[x] = n%:~R.
Lemma derivMz n p : (p *~ n)^`() = p^`() *~ n.
Lemma mulpz p n : p *~ n = n%:~R *: p.
End PolyZintRing.
Section ZnatPred.
Definition Znat := [qualify a n : int | 0 ≤ n].
Fact Znat_key : pred_key Znat.
Canonical Znat_keyd := KeyedQualifier Znat_key.
Lemma Znat_def n : (n \is a Znat) = (0 ≤ n).
Lemma Znat_semiring_closed : semiring_closed Znat.
Canonical Znat_addrPred := AddrPred Znat_semiring_closed.
Canonical Znat_mulrPred := MulrPred Znat_semiring_closed.
Canonical Znat_semiringPred := SemiringPred Znat_semiring_closed.
Lemma ZnatP (m : int) : reflect (∃ n : nat, m = n) (m \is a Znat).
End ZnatPred.
Section rpred.
Lemma rpredMz M S (addS : @zmodPred M S) (kS : keyed_pred addS) m :
{in kS, ∀ u, u *~ m \in kS}.
Lemma rpred_int R S (ringS : @subringPred R S) (kS : keyed_pred ringS) m :
m%:~R \in kS.
Lemma rpredZint (R : ringType) (M : lmodType R) S
(addS : @zmodPred M S) (kS : keyed_pred addS) m :
{in kS, ∀ u, m%:~R *: u \in kS}.
Lemma rpredXz R S (divS : @divrPred R S) (kS : keyed_pred divS) m :
{in kS, ∀ x, x ^ m \in kS}.
Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x :
(x ^ ((-1) ^+ n) \in kS) = (x \in kS).
End rpred.
`|m1 - m3| ≤ `|m1 - m2| + `|m2 - m3|
?= iff (m1 ≤ m2 ≤ m3)%R || (m3 ≤ m2 ≤ m1)%R.
Lemma leqifD_dist n1 n2 n3 :
`|n1 - n3| ≤ `|n1 - n2| + `|n2 - n3|
?= iff (n1 ≤ n2 ≤ n3) || (n3 ≤ n2 ≤ n1).
Lemma sqrn_dist n1 n2 : `|n1 - n2| ^ 2 + 2 × (n1 × n2) = n1 ^ 2 + n2 ^ 2.
End Distn.
End IntDist.
#[deprecated(since="mathcomp 1.17.0", note="Use leqD_dist instead.")]
Notation leq_add_dist := leqD_dist.
#[deprecated(since="mathcomp 1.17.0", note="Use leqifD_distz instead.")]
Notation leqif_add_distz := leqifD_distz.
#[deprecated(since="mathcomp 1.17.0", note="Use leqifD_dist instead.")]
Notation leqif_add_dist := leqifD_dist.
Section NormInt.
Variable R : numDomainType.
Lemma intr_norm m : `|m|%:~R = `|m%:~R : R|.
Lemma normrMz m (x : R) : `|x *~ m| = `|x| *~ `|m|.
Lemma expN1r (i : int) : (-1 : R) ^ i = (-1) ^+ `|i|.
End NormInt.
Section PolyZintRing.
Variable R : ringType.
Implicit Types x y z: R.
Implicit Types m n : int.
Implicit Types i j k : nat.
Implicit Types p q r : {poly R}.
Lemma coefMrz p n i : (p *~ n)`_i = (p`_i *~ n).
Lemma polyCMz n : {morph (@polyC R) : c / c *~ n}.
Lemma hornerMz n p x : (p *~ n).[x] = p.[x] *~ n.
Lemma horner_int n x : (n%:~R : {poly R}).[x] = n%:~R.
Lemma derivMz n p : (p *~ n)^`() = p^`() *~ n.
Lemma mulpz p n : p *~ n = n%:~R *: p.
End PolyZintRing.
Section ZnatPred.
Definition Znat := [qualify a n : int | 0 ≤ n].
Fact Znat_key : pred_key Znat.
Canonical Znat_keyd := KeyedQualifier Znat_key.
Lemma Znat_def n : (n \is a Znat) = (0 ≤ n).
Lemma Znat_semiring_closed : semiring_closed Znat.
Canonical Znat_addrPred := AddrPred Znat_semiring_closed.
Canonical Znat_mulrPred := MulrPred Znat_semiring_closed.
Canonical Znat_semiringPred := SemiringPred Znat_semiring_closed.
Lemma ZnatP (m : int) : reflect (∃ n : nat, m = n) (m \is a Znat).
End ZnatPred.
Section rpred.
Lemma rpredMz M S (addS : @zmodPred M S) (kS : keyed_pred addS) m :
{in kS, ∀ u, u *~ m \in kS}.
Lemma rpred_int R S (ringS : @subringPred R S) (kS : keyed_pred ringS) m :
m%:~R \in kS.
Lemma rpredZint (R : ringType) (M : lmodType R) S
(addS : @zmodPred M S) (kS : keyed_pred addS) m :
{in kS, ∀ u, m%:~R *: u \in kS}.
Lemma rpredXz R S (divS : @divrPred R S) (kS : keyed_pred divS) m :
{in kS, ∀ x, x ^ m \in kS}.
Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x :
(x ^ ((-1) ^+ n) \in kS) = (x \in kS).
End rpred.