@@ -85,31 +84,31 @@
-
Notation "n %:Z" := (
Posz n)
+
Notation "n %:Z" := (
Posz n)
(
at level 2,
left associativity,
format "n %:Z",
only parsing) :
int_scope.
-
Notation "n %:Z" := (
Posz n)
+
Notation "n %:Z" := (
Posz n)
(
at level 2,
left associativity,
format "n %:Z",
only parsing) :
ring_scope.
-
Notation "n = m :> 'in' 't'" := (
Posz n = Posz m)
+
Notation "n = m :> 'in' 't'" := (
Posz n = Posz m)
(
at level 70,
m at next level,
format "n = m :> 'in' 't'") :
ring_scope.
-
Notation "n == m :> 'in' 't'" := (
Posz n == Posz m)
+
Notation "n == m :> 'in' 't'" := (
Posz n == Posz m)
(
at level 70,
m at next level,
format "n == m :> 'in' 't'") :
ring_scope.
-
Notation "n != m :> 'in' 't'" := (
Posz n != Posz m)
+
Notation "n != m :> 'in' 't'" := (
Posz n != Posz m)
(
at level 70,
m at next level,
format "n != m :> 'in' 't'") :
ring_scope.
-
Notation "n <> m :> 'in' 't'" := (
Posz n ≠ Posz m)
+
Notation "n <> m :> 'in' 't'" := (
Posz n ≠ Posz m)
(
at level 70,
m at next level,
format "n <> m :> 'in' 't'") :
ring_scope.
-
Definition natsum_of_int (
m :
int) :
nat + nat :=
-
match m with Posz p ⇒
inl _ p |
Negz n ⇒
inr _ n end.
+
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.
+
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.
+
Lemma natsum_of_intK :
cancel natsum_of_int int_of_natsum.
Definition int_eqMixin :=
CanEqMixin natsum_of_intK.
@@ -120,7 +119,7 @@
Canonical int_countType :=
Eval hnf in CountType int int_countMixin.
-
Lemma eqz_nat (
m n :
nat) :
(m%:Z == n%:Z) = (m == n).
+
Lemma eqz_nat (
m n :
nat) :
(m%:Z == n%:Z) = (m == n).
Module intZmod.
@@ -129,83 +128,83 @@
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')
+ |
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
+
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
+ |
Posz n ⇒
if n is (
n'.+1)%
N then Negz n' else Posz 0
+ |
Negz n ⇒
Posz (
n.+1)%
N
end.
-
Lemma PoszD :
{morph Posz : m n / (
m + n)%
N >-> m + n}.
+
Lemma PoszD :
{morph Posz : m n / (
m + n)%
N >-> m + n}.
-
Lemma NegzE (
n :
nat) :
Negz n = - n.+1.
+
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.
+
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.
-
CoInductive 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).
+
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 addzC :
commutative addz.
-
Lemma add0z :
left_id 0
addz.
+
Lemma add0z :
left_id 0
addz.
-
Lemma oppzK :
involutive oppz.
+
Lemma oppzK :
involutive oppz.
-
Lemma oppz_add :
{morph oppz : m n / m + n}.
+
Lemma oppz_add :
{morph oppz : m n / m + n}.
-
Lemma add1Pz (
n :
int) : 1
+ (n - 1
) = n.
+
Lemma add1Pz (
n :
int) : 1
+ (n - 1
) = n.
-
Lemma subSz1 (
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 addSnz (
m :
nat) (
n :
int) :
(m.+1%
N) + n = 1
+ (m + n).
-
Lemma addSz (
m n :
int) :
(1
+ m) + 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 addPz (
m n :
int) :
(m - 1
) + n = (m + n) - 1.
-
Lemma addzA :
associative addz.
+
Lemma addzA :
associative addz.
-
Lemma addNz :
left_inverse (0
:int)
oppz addz.
+
Lemma addNz :
left_inverse (0
:int)
oppz addz.
-
Lemma predn_int (
n :
nat) : 0
< n → n.-1%:Z = n - 1.
+
Lemma predn_int (
n :
nat) : 0
< n → n.-1%:Z = n - 1.
Definition Mixin :=
ZmodMixin addzA addzC add0z addNz.
@@ -226,38 +225,38 @@
-
Lemma PoszD :
{morph Posz : n m / (
n + m)%
N >-> n + m}.
+
Lemma PoszD :
{morph Posz : n m / (
n + m)%
N >-> n + m}.
-
Lemma NegzE (
n :
nat) :
Negz n = -(n.+1)%:Z.
+
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.
+
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.
-
CoInductive int_spec (
x :
int) :
int → Type :=
+
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).
+|
ZintPos n :
int_spec x n.+1
+|
ZintNeg n :
int_spec x (
- (n.+1)%:Z).
Lemma intP x :
int_spec x x.
-
Definition oppz_add := (@
opprD [zmodType of int]).
+
Definition oppz_add := (@
opprD [zmodType of int]).
-
Lemma subzn (
m n :
nat) : (
n ≤ m)%
N → m%:Z - n%:Z = (
m - n)%
N.
+
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.
+
Lemma subzSS (
m n :
nat) :
m.+1%:Z - n.+1%:Z = m%:Z - n%:Z.
End intZmoduleTheory.
@@ -271,43 +270,43 @@
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
+ |
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.
-
Lemma mul0z :
left_zero 0
*%Z.
+
Lemma mul0z :
left_zero 0
*%Z.
-
Lemma mulzC :
commutative mulz.
+
Lemma mulzC :
commutative mulz.
-
Lemma mulz0 :
right_zero 0
*%Z.
+
Lemma mulz0 :
right_zero 0
*%Z.
-
Lemma mulzN (
m n :
int) : (
m × (- n))%
Z = - (
m × n)%
Z.
+
Lemma mulzN (
m n :
int) : (
m × (- n))%
Z = - (
m × n)%
Z.
-
Lemma mulNz (
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 mulzA :
associative mulz.
-
Lemma mul1z :
left_id 1%
Z mulz.
+
Lemma mul1z :
left_id 1%
Z mulz.
-
Lemma mulzS (
x :
int) (
n :
nat) : (
x × n.+1%:Z)%
Z = x + (
x × n)%
Z.
+
Lemma mulzS (
x :
int) (
n :
nat) : (
x × n.+1%:Z)%
Z = x + (
x × n)%
Z.
-
Lemma mulz_addl :
left_distributive mulz (
+%R).
+
Lemma mulz_addl :
left_distributive mulz (
+%R).
-
Lemma nonzero1z : 1%
Z != 0.
+
Lemma nonzero1z : 1%
Z != 0.
Definition comMixin :=
ComRingMixin mulzA mulzC mul1z mulz_addl nonzero1z.
@@ -327,13 +326,13 @@
Implicit Types m n :
int.
-
Lemma PoszM :
{morph Posz : n m / (
n × m)%
N >-> n × m}.
+
Lemma PoszM :
{morph Posz : n m / (
n × m)%
N >-> n × m}.
-
Lemma intS (
n :
nat) :
n.+1%:Z = 1
+ n%:Z.
+
Lemma intS (
n :
nat) :
n.+1%:Z = 1
+ n%:Z.
-
Lemma predn_int (
n :
nat) : (0
< n)%
N → n.-1%:Z = n%:Z - 1.
+
Lemma predn_int (
n :
nat) : (0
< n)%
N → n.-1%:Z = n%:Z - 1.
End intRingTheory.
@@ -344,23 +343,23 @@
Implicit Types m n :
int.
-
Definition unitz :=
[qualify a n : int | (n == 1
) || (n == -1
)].
+
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 mulVz :
{in unitz, left_inverse 1%
R invz *%R}.
-
Lemma mulzn_eq1 m (
n :
nat) :
(m × n == 1
) = (m == 1
) && (n == 1%
N).
+
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 unitzPl m n :
n × m = 1
→ m \is a unitz.
-
Lemma invz_out :
{in [predC unitz], invz =1 id}.
+
Lemma invz_out :
{in [predC unitz], invz =1 id}.
-
Lemma idomain_axiomz m n :
m × n = 0
→ (m == 0
) || (n == 0
).
+
Lemma idomain_axiomz m n :
m × n = 0
→ (m == 0
) || (n == 0
).
Definition comMixin :=
ComUnitRingMixin mulVz unitzPl invz_out.
@@ -372,13 +371,21 @@
Canonical int_unitRingType :=
Eval hnf in UnitRingType int intUnitRing.comMixin.
-
Canonical int_comUnitRing :=
Eval hnf in [comUnitRingType of int].
+
Canonical int_comUnitRing :=
Eval hnf in [comUnitRingType of int].
Canonical int_iDomain :=
Eval hnf in IdomainType int intUnitRing.idomain_axiomz.
-
Definition absz m :=
match m with Posz p ⇒
p |
Negz n ⇒
n.+1 end.
-
Notation "m - n" :=
+
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.
@@ -391,51 +398,51 @@
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
+ |
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
+ |
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_norm_add x y :
lez (
normz (
x + y)) (
normz x + normz y).
+
Fact lez_norm_add x y :
lez (
normz (
x + y)) (
normz x + normz y).
-
Fact ltz_add x y :
ltz 0
x → ltz 0
y → ltz 0 (
x + y).
+
Fact ltz_add x y :
ltz 0
x → ltz 0
y → ltz 0 (
x + y).
-
Fact eq0_normz x :
normz x = 0
→ x = 0.
+
Fact eq0_normz x :
normz x = 0
→ x = 0.
-
Fact lez_total x y :
lez x y || lez y x.
+
Fact lez_total x y :
lez x y || lez y x.
-
Lemma abszN (
n :
nat) :
absz (
- n%:Z)
= n.
+
Lemma abszN (
n :
nat) :
absz (
- n%:Z)
= n.
-
Fact normzM :
{morph (fun n ⇒
normz n) : x y / x × y}.
+
Fact normzM :
{morph (fun n ⇒
normz n) : x y / x × y}.
-
Lemma subz_ge0 m n :
lez 0 (
n - m)
= lez m n.
+
Lemma subz_ge0 m n :
lez 0 (
n - m)
= lez m n.
-
Fact lez_def x y :
(lez x y) = (normz (
y - x)
== y - x).
+
Fact lez_def x y :
(lez x y) = (normz (
y - x)
== y - x).
-
Fact ltz_def x y :
(ltz x y) = (y != x) && (lez x y).
+
Fact ltz_def x y :
(ltz x y) = (y != x) && (lez x y).
Definition Mixin :=
-
NumMixin lez_norm_add ltz_add eq0_normz (
in2W lez_total)
normzM
+
NumMixin lez_norm_add ltz_add eq0_normz (
in2W lez_total)
normzM
lez_def ltz_def.
@@ -450,57 +457,57 @@
Section intOrderedTheory.
-
Implicit Types m n p :
nat.
+
Implicit Types m n p :
nat.
Implicit Types x y z :
int.
-
Lemma lez_nat m n :
(m ≤ n :> int) = (
m ≤ n)%
N.
+
Lemma lez_nat m n :
(m ≤ n :> int) = (
m ≤ n)%
N.
-
Lemma ltz_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).
+
Definition ltez_nat :=
(lez_nat, ltz_nat).
-
Lemma leNz_nat m n : (
- m%:Z ≤ n).
+
Lemma leNz_nat m n : (
- m%:Z ≤ n).
-
Lemma ltNz_nat m n :
(- m%:Z < n) = (m != 0%
N) || (n != 0%
N).
+
Lemma ltNz_nat m n :
(- m%:Z < n) = (m != 0%
N) || (n != 0%
N).
-
Definition lteNz_nat :=
(leNz_nat, ltNz_nat).
+
Definition lteNz_nat :=
(leNz_nat, ltNz_nat).
-
Lemma lezN_nat m n :
(m%:Z ≤ - n%:Z) = (m == 0%
N) && (n == 0%
N).
+
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 ltzN_nat m n :
(m%:Z < - n%:Z) = false.
-
Lemma le0z_nat n : 0
≤ n :> int.
+
Lemma le0z_nat n : 0
≤ n :> int.
-
Lemma lez0_nat n :
n ≤ 0
:> int = (n == 0%
N :> nat).
+
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).
+
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 gtz0_ge1 x :
(0
< x) = (1
≤ x).
-
Lemma lez_add1r x y :
(1
+ x ≤ y) = (x < y).
+
Lemma lez_add1r x y :
(1
+ x ≤ y) = (x < y).
-
Lemma lez_addr1 x y :
(x + 1
≤ y) = (x < y).
+
Lemma lez_addr1 x y :
(x + 1
≤ y) = (x < y).
-
Lemma ltz_add1r x y :
(x < 1
+ y) = (x ≤ y).
+
Lemma ltz_add1r x y :
(x < 1
+ y) = (x ≤ y).
-
Lemma ltz_addr1 x y :
(x < y + 1
) = (x ≤ y).
+
Lemma ltz_addr1 x y :
(x < y + 1
) = (x ≤ y).
End intOrderedTheory.
@@ -514,25 +521,25 @@
definition of intmul
-
Definition intmul (
R :
zmodType) (
x :
R) (
n :
int) :=
nosimpl
+
Definition intmul (
R :
zmodType) (
x :
R) (
n :
int) :=
nosimpl
match n with
- |
Posz n ⇒ (
x *+ n)%
R
- |
Negz n ⇒ (
x *- (n.+1))%
R
+ |
Posz n ⇒ (
x *+ n)%
R
+ |
Negz n ⇒ (
x *- (n.+1))%
R
end.
-
Notation "*~%R" := (@
intmul _) (
at level 0,
format " *~%R") :
ring_scope.
-
Notation "x *~ n" := (
intmul x n)
+
Notation "*~%R" := (@
intmul _) (
at level 0,
format " *~%R") :
ring_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
+
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 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.
+
Lemma nmulrn (
R :
zmodType) (
x :
R) (
n :
nat) :
x *- n = x *~ - n%:Z.
Section ZintLmod.
@@ -548,66 +555,66 @@
Implicit Types x y z :
M.
-
Fact mulrzA_C m n x :
(x *~ n) *~ m = x *~ (m × n).
+
Fact mulrzA_C m n x :
(x *~ n) *~ m = x *~ (m × n).
-
Fact mulrzAC 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 mulr1z (
x :
M) :
x *~ 1
= x.
-
Fact mulrzDr m :
{morph ( *~%R^~ m : M → M) : x y / x + y}.
+
Fact mulrzDr 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.
+
Lemma mulrzBl_nat (
m n :
nat)
x :
x *~ (m%:Z - n%:Z) = x *~ m - x *~ n.
-
Fact mulrzDl x :
{morph *~%R x : m n / m + n}.
+
Fact mulrzDl x :
{morph *~%R x : m n / m + n}.
Definition Mint_LmodMixin :=
- @
LmodMixin _ [zmodType of M] (
fun n x ⇒
x *~ n)
+ @
LmodMixin _ [zmodType of M] (
fun n x ⇒
x *~ n)
mulrzA_C mulr1z mulrzDr mulrzDl.
-
Canonical Mint_LmodType :=
LmodType int M^z Mint_LmodMixin.
+
Canonical Mint_LmodType :=
LmodType int M^z Mint_LmodMixin.
-
Lemma scalezrE n x :
n *: (x : M^z) = x *~ n.
+
Lemma scalezrE n x :
n *: (x : M^z) = x *~ n.
-
Lemma mulrzA x m n :
x *~ (m × n) = x *~ m *~ n.
+
Lemma mulrzA x m n :
x *~ (m × n) = x *~ m *~ n.
-
Lemma mulr0z x :
x *~ 0
= 0.
+
Lemma mulr0z x :
x *~ 0
= 0.
-
Lemma mul0rz n : 0
*~ n = 0
:> M.
+
Lemma mul0rz n : 0
*~ n = 0
:> M.
-
Lemma mulrNz x n :
x *~ (- n) = - (x *~ n).
+
Lemma mulrNz x n :
x *~ (- n) = - (x *~ n).
-
Lemma mulrN1z x :
x *~ (- 1
) = - x.
+
Lemma mulrN1z x :
x *~ (- 1
) = - x.
-
Lemma mulNrz x n :
(- x) *~ n = - (x *~ n).
+
Lemma mulNrz x n :
(- x) *~ n = - (x *~ n).
-
Lemma mulrzBr x m n :
x *~ (m - n) = x *~ m - 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 mulrzBl x y n :
(x - y) *~ n = x *~ n - y *~ n.
-
Lemma mulrz_nat (
n :
nat)
x :
x *~ n%:R = x *+ 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_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.
+
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).
@@ -616,14 +623,14 @@
End ZintLmod.
-
Lemma ffunMzE (
I :
finType) (
M :
zmodType) (
f :
{ffun I → M})
z x :
- (
f *~ z)
x = f x *~ z.
+
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 intz (
n :
int) :
n%:~R = n.
-
Lemma natz (
n :
nat) :
n%:R = n%:Z :> int.
+
Lemma natz (
n :
nat) :
n%:R = n%:Z :> int.
Section RintMod.
@@ -636,47 +643,47 @@
Implicit Types x y z :
R.
-
Lemma mulrzAl n x y :
(x *~ n) × y = (x × y) *~ n.
+
Lemma mulrzAl n x y :
(x *~ n) × y = (x × y) *~ n.
-
Lemma mulrzAr n x y :
x × (y *~ n) = (x × y) *~ n.
+
Lemma mulrzAr n x y :
x × (y *~ n) = (x × y) *~ n.
-
Lemma mulrzl x n :
n%:~R × x = x *~ n.
+
Lemma mulrzl x n :
n%:~R × x = x *~ n.
-
Lemma mulrzr x n :
x × n%:~R = x *~ n.
+
Lemma mulrzr x n :
x × n%:~R = x *~ n.
-
Lemma mulNrNz n x :
(-x) *~ (-n) = x *~ n.
+
Lemma mulNrNz n x :
(-x) *~ (-n) = x *~ n.
-
Lemma mulrbz x (
b :
bool) :
x *~ b = (if b then x else 0
).
+
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 intrD m n :
(m + n)%:~R = m%:~R + n%:~R :> R.
-
Lemma intrM 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)).
+
Lemma intmul1_is_rmorphism :
rmorphism (
*~%R (1 : R)).
Canonical intmul1_rmorphism :=
RMorphism intmul1_is_rmorphism.
-
Lemma mulr2z n :
n *~ 2
= n + n.
+
Lemma mulr2z n :
n *~ 2
= n + n.
End RintMod.
-
Lemma mulrzz m n :
m *~ n = m × n.
+
Lemma mulrzz m n :
m *~ n = m × n.
-
Lemma mulz2 n :
n × 2
%:Z = n + n.
+
Lemma mulz2 n :
n × 2
%:Z = n + n.
-
Lemma mul2z n : 2
%:Z × n = n + n.
+
Lemma mul2z n : 2
%:Z × n = n + n.
Section LMod.
@@ -691,27 +698,27 @@
Implicit Types u v w :
V.
-
Lemma scaler_int n v :
n%:~R *: v = v *~ n.
+
Lemma scaler_int n v :
n%:~R *: v = v *~ n.
-
Lemma scalerMzl a v n :
(a *: v) *~ n = (a *~ n) *: v.
+
Lemma scalerMzl a v n :
(a *: v) *~ n = (a *~ n) *: v.
-
Lemma scalerMzr a v n :
(a *: v) *~ n = a *: (v *~ n).
+
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.
+
Lemma mulrz_int (
M :
zmodType) (
n :
int) (
x :
M) :
x *~ n%:~R = x *~ n.
Section MorphTheory.
Section Additive.
-
Variables (
U V :
zmodType) (
f :
{additive U → V}).
+
Variables (
U V :
zmodType) (
f :
{additive U → V}).
-
Lemma raddfMz n :
{morph f : x / x *~ n}.
+
Lemma raddfMz n :
{morph f : x / x *~ n}.
End Additive.
@@ -720,13 +727,13 @@
Section Multiplicative.
-
Variables (
R S :
ringType) (
f :
{rmorphism R → S}).
+
Variables (
R S :
ringType) (
f :
{rmorphism R → S}).
-
Lemma rmorphMz :
∀ n,
{morph f : x / x *~ n}.
+
Lemma rmorphMz :
∀ n,
{morph f : x / x *~ n}.
-
Lemma rmorph_int :
∀ n,
f n%:~R = n%:~R.
+
Lemma rmorph_int :
∀ n,
f n%:~R = n%:~R.
End Multiplicative.
@@ -736,16 +743,16 @@
Variable R :
ringType.
-
Variables (
U V :
lmodType R) (
f :
{linear U → V}).
+
Variables (
U V :
lmodType R) (
f :
{linear U → V}).
-
Lemma linearMn :
∀ n,
{morph f : x / x *~ n}.
+
Lemma linearMn :
∀ n,
{morph f : x / x *~ n}.
End Linear.
-
Lemma raddf_int_scalable (
aV rV :
lmodType int) (
f :
{additive aV → rV}) :
+
Lemma raddf_int_scalable (
aV rV :
lmodType int) (
f :
{additive aV → rV}) :
scalable f.
@@ -755,10 +762,10 @@
Variable R :
ringType.
-
Lemma commrMz (
x y :
R)
n :
GRing.comm x y → GRing.comm x (
y *~ n).
+
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.
+
Lemma commr_int (
x :
R)
n :
GRing.comm x n%:~R.
End Zintmul1rMorph.
@@ -770,12 +777,12 @@
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 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.
+
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.
@@ -788,16 +795,16 @@
Implicit Types x y :
R.
-
Variable p :
nat.
-
Hypothesis charFp :
p \in [char R].
+
Variable p :
nat.
+
Hypothesis charFp :
p \in [char R].
-
Lemma Frobenius_autMz x n :
(x *~ n)^f = x^f *~ n.
+
Lemma Frobenius_autMz x n :
(x *~ n)^f = x^f *~ n.
-
Lemma Frobenius_aut_int n :
(n%:~R)^f = n%:~R.
+
Lemma Frobenius_aut_int n :
(n%:~R)^f = n%:~R.
End Frobenius.
@@ -816,7 +823,7 @@
Implicit Types x y :
R.
-
Lemma rmorphzP (
f :
{rmorphism int → R}) :
f =1 ( *~%R 1).
+
Lemma rmorphzP (
f :
{rmorphism int → R}) :
f =1 ( *~%R 1).
@@ -825,149 +832,149 @@
intmul and ler/ltr