From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.algebra.zmodp.html | 185 ++++++++++++++++---------------
1 file changed, 98 insertions(+), 87 deletions(-)
(limited to 'docs/htmldoc/mathcomp.algebra.zmodp.html')
diff --git a/docs/htmldoc/mathcomp.algebra.zmodp.html b/docs/htmldoc/mathcomp.algebra.zmodp.html
index f4141db..f8d448b 100644
--- a/docs/htmldoc/mathcomp.algebra.zmodp.html
+++ b/docs/htmldoc/mathcomp.algebra.zmodp.html
@@ -21,7 +21,6 @@
@@ -94,10 +93,10 @@
-
Variable p' :
nat.
+
Variable p' :
nat.
-
Implicit Types x y z :
'I_p.
+
Implicit Types x y z :
'I_p.
@@ -107,8 +106,8 @@
@@ -117,12 +116,12 @@
Operations
@@ -133,23 +132,23 @@
@@ -160,58 +159,58 @@
-
Lemma Zp_mul1z :
left_id Zp1 Zp_mul.
+
Lemma Zp_mul1z :
left_id Zp1 Zp_mul.
-
Lemma Zp_mulC :
commutative Zp_mul.
+
Lemma Zp_mulC :
commutative Zp_mul.
-
Lemma Zp_mulz1 :
right_id Zp1 Zp_mul.
+
Lemma Zp_mulz1 :
right_id Zp1 Zp_mul.
-
Lemma Zp_mulA :
associative Zp_mul.
+
Lemma Zp_mulA :
associative Zp_mul.
-
Lemma Zp_mul_addr :
right_distributive Zp_mul Zp_add.
+
Lemma Zp_mul_addr :
right_distributive Zp_mul Zp_add.
-
Lemma Zp_mul_addl :
left_distributive Zp_mul Zp_add.
+
Lemma Zp_mul_addl :
left_distributive Zp_mul Zp_add.
-
Lemma Zp_mulVz x :
coprime p x → Zp_mul (
Zp_inv x)
x = Zp1.
+
Lemma Zp_mulVz x :
coprime p x → Zp_mul (
Zp_inv x)
x = Zp1.
-
Lemma Zp_mulzV x :
coprime p x → Zp_mul x (
Zp_inv x)
= Zp1.
+
Lemma Zp_mulzV x :
coprime p x → Zp_mul x (
Zp_inv x)
= Zp1.
-
Lemma Zp_intro_unit x y :
Zp_mul y x = Zp1 → coprime p x.
+
Lemma Zp_intro_unit x y :
Zp_mul y x = Zp1 → coprime p x.
-
Lemma Zp_inv_out x :
~~ coprime p x → Zp_inv x = x.
+
Lemma Zp_inv_out x :
~~ coprime p x → Zp_inv x = x.
-
Lemma Zp_mulrn x n :
x *+ n = inZp (
x × n).
+
Lemma Zp_mulrn x n :
x *+ n = inZp (
x × n).
Import GroupScope.
-
Lemma Zp_mulgC : @
commutative 'I_p _ mulg.
+
Lemma Zp_mulgC : @
commutative 'I_p _ mulg.
-
Lemma Zp_abelian :
abelian [set: 'I_p].
+
Lemma Zp_abelian :
abelian [set: 'I_p].
-
Lemma Zp_expg x n :
x ^+ n = inZp (
x × n).
+
Lemma Zp_expg x n :
x ^+ n = inZp (
x × n).
-
Lemma Zp1_expgz x :
Zp1 ^+ x = x.
+
Lemma Zp1_expgz x :
Zp1 ^+ x = x.
-
Lemma Zp_cycle :
setT = <[Zp1]>.
+
Lemma Zp_cycle :
setT = <[Zp1]>.
-
Lemma order_Zp1 :
#[Zp1] = p.
+
Lemma order_Zp1 :
#[Zp1] = p.
End ZpDef.
@@ -219,123 +218,125 @@
-
Lemma ord1 :
all_equal_to (0
: 'I_1).
+
Lemma ord1 :
all_equal_to (0
: 'I_1).
-
Lemma lshift0 m n :
lshift m (0
: 'I_n.+1)
= (0
: 'I_(n + m).+1).
+
Lemma lshift0 m n :
lshift m (0
: 'I_n.+1)
= (0
: 'I_(n + m).+1).
-
Lemma rshift1 n : @
rshift 1
n =1 lift (0
: 'I_n.+1).
+
Lemma rshift1 n : @
rshift 1
n =1 lift (0
: 'I_n.+1).
Lemma split1 n i :
-
split (
i : 'I_(1
+ n))
= oapp (@
inr _ _) (
inl _ 0) (
unlift 0
i).
+
split (
i : 'I_(1
+ n))
= oapp (@
inr _ _) (
inl _ 0) (
unlift 0
i).
Lemma big_ord1 R idx (
op : @
Monoid.law R idx)
F :
-
\big[op/idx]_(i < 1
) F i = F 0.
+
\big[op/idx]_(i < 1
) F i = F 0.
Lemma big_ord1_cond R idx (
op : @
Monoid.law R idx)
P F :
-
\big[op/idx]_(i < 1
| P i) F i = if P 0
then F 0
else idx.
+
\big[op/idx]_(i < 1
| P i) F i = if P 0
then F 0
else idx.
Section ZpRing.
-
Variable p' :
nat.
+
Variable p' :
nat.
-
Lemma Zp_nontrivial :
Zp1 != 0
:> 'I_p.
+
Lemma Zp_nontrivial :
Zp1 != 0
:> 'I_p.
Definition Zp_ringMixin :=
ComRingMixin (@
Zp_mulA _) (@
Zp_mulC _) (@
Zp_mul1z _) (@
Zp_mul_addl _)
Zp_nontrivial.
-
Canonical Zp_ringType :=
Eval hnf in RingType 'I_p Zp_ringMixin.
-
Canonical Zp_finRingType :=
Eval hnf in [finRingType of 'I_p].
-
Canonical Zp_comRingType :=
Eval hnf in ComRingType 'I_p (@
Zp_mulC _).
-
Canonical Zp_finComRingType :=
Eval hnf in [finComRingType of 'I_p].
+
Canonical Zp_ringType :=
Eval hnf in RingType 'I_p Zp_ringMixin.
+
Canonical Zp_finRingType :=
Eval hnf in [finRingType of 'I_p].
+
Canonical Zp_comRingType :=
Eval hnf in ComRingType 'I_p (@
Zp_mulC _).
+
Canonical Zp_finComRingType :=
Eval hnf in [finComRingType of 'I_p].
Definition Zp_unitRingMixin :=
ComUnitRingMixin (@
Zp_mulVz _) (@
Zp_intro_unit _) (@
Zp_inv_out _).
-
Canonical Zp_unitRingType :=
Eval hnf in UnitRingType 'I_p Zp_unitRingMixin.
-
Canonical Zp_finUnitRingType :=
Eval hnf in [finUnitRingType of 'I_p].
-
Canonical Zp_comUnitRingType :=
Eval hnf in [comUnitRingType of 'I_p].
-
Canonical Zp_finComUnitRingType :=
Eval hnf in [finComUnitRingType of 'I_p].
+
Canonical Zp_unitRingType :=
Eval hnf in UnitRingType 'I_p Zp_unitRingMixin.
+
Canonical Zp_finUnitRingType :=
Eval hnf in [finUnitRingType of 'I_p].
+
Canonical Zp_comUnitRingType :=
Eval hnf in [comUnitRingType of 'I_p].
+
Canonical Zp_finComUnitRingType :=
Eval hnf in [finComUnitRingType of 'I_p].
-
Lemma Zp_nat n :
n%:R = inZp n :> 'I_p.
+
Lemma Zp_nat n :
n%:R = inZp n :> 'I_p.
-
Lemma natr_Zp (
x :
'I_p) :
x%:R = x.
+
Lemma natr_Zp (
x :
'I_p) :
x%:R = x.
-
Lemma natr_negZp (
x :
'I_p) :
(- x)%:R = - x.
+
Lemma natr_negZp (
x :
'I_p) :
(- x)%:R = - x.
Import GroupScope.
-
Lemma unit_Zp_mulgC : @
commutative {unit 'I_p} _ mulg.
+
Lemma unit_Zp_mulgC : @
commutative {unit 'I_p} _ mulg.
-
Lemma unit_Zp_expg (
u :
{unit 'I_p})
n :
-
val (
u ^+ n)
= inZp (
val u ^ n)
:> 'I_p.
+
Lemma unit_Zp_expg (
u :
{unit 'I_p})
n :
+
val (
u ^+ n)
= inZp (
val u ^ n)
:> 'I_p.
End ZpRing.
-
Definition Zp_trunc p :=
p.-2.
+
Definition Zp_trunc p :=
p.-2.
-
Notation "''Z_' p" :=
'I_(Zp_trunc p).+2
+
Notation "''Z_' p" :=
'I_(Zp_trunc p).+2
(
at level 8,
p at level 2,
format "''Z_' p") :
type_scope.
-
Notation "''F_' p" :=
'Z_(pdiv p)
+
Notation "''F_' p" :=
'Z_(pdiv p)
(
at level 8,
p at level 2,
format "''F_' p") :
type_scope.
+
+
Section Groups.
-
Variable p :
nat.
+
Variable p :
nat.
-
Definition Zp :=
if p > 1
then [set: 'Z_p] else 1%
g.
-
Definition units_Zp :=
[set: {unit 'Z_p}].
+
Definition Zp :=
if p > 1
then [set: 'Z_p] else 1%
g.
+
Definition units_Zp :=
[set: {unit 'Z_p}].
-
Lemma Zp_cast :
p > 1
→ (Zp_trunc p).+2 = p.
+
Lemma Zp_cast :
p > 1
→ (Zp_trunc p).+2 = p.
-
Lemma val_Zp_nat (
p_gt1 :
p > 1)
n :
(n%:R : 'Z_p) = (
n %% p)%
N :> nat.
+
Lemma val_Zp_nat (
p_gt1 :
p > 1)
n :
(n%:R : 'Z_p) = (
n %% p)%
N :> nat.
-
Lemma Zp_nat_mod (
p_gt1 :
p > 1)
m :
(m %% p)%:R = m%:R :> 'Z_p.
+
Lemma Zp_nat_mod (
p_gt1 :
p > 1)
m :
(m %% p)%:R = m%:R :> 'Z_p.
-
Lemma char_Zp :
p > 1
→ p%:R = 0
:> 'Z_p.
+
Lemma char_Zp :
p > 1
→ p%:R = 0
:> 'Z_p.
-
Lemma unitZpE x :
p > 1
→ ((x%:R : 'Z_p) \is a GRing.unit) = coprime p x.
+
Lemma unitZpE x :
p > 1
→ ((x%:R : 'Z_p) \is a GRing.unit) = coprime p x.
Lemma Zp_group_set :
group_set Zp.
Canonical Zp_group :=
Group Zp_group_set.
-
Lemma card_Zp :
p > 0
→ #|Zp| = p.
+
Lemma card_Zp :
p > 0
→ #|Zp| = p.
-
Lemma mem_Zp x :
p > 1
→ x \in Zp.
+
Lemma mem_Zp x :
p > 1
→ x \in Zp.
-
Canonical units_Zp_group :=
[group of units_Zp].
+
Canonical units_Zp_group :=
[group of units_Zp].
-
Lemma card_units_Zp :
p > 0
→ #|units_Zp| = totient p.
+
Lemma card_units_Zp :
p > 0
→ #|units_Zp| = totient p.
Lemma units_Zp_abelian :
abelian units_Zp.
@@ -358,7 +359,7 @@
Open Scope ring_scope.
-
Variable p :
nat.
+
Variable p :
nat.
Section F_prime.
@@ -367,48 +368,58 @@
Hypothesis p_pr :
prime p.
-
Lemma Fp_Zcast :
(Zp_trunc (
pdiv p)
).+2 = (Zp_trunc p).+2.
+
Lemma Fp_Zcast :
(Zp_trunc (
pdiv p)
).+2 = (Zp_trunc p).+2.
-
Lemma Fp_cast :
(Zp_trunc (
pdiv p)
).+2 = p.
+
Lemma Fp_cast :
(Zp_trunc (
pdiv p)
).+2 = p.
-
Lemma card_Fp :
#|'F_p| = p.
+
Lemma card_Fp :
#|'F_p| = p.
-
Lemma val_Fp_nat n :
(n%:R : 'F_p) = (
n %% p)%
N :> nat.
+
Lemma val_Fp_nat n :
(n%:R : 'F_p) = (
n %% p)%
N :> nat.
-
Lemma Fp_nat_mod m :
(m %% p)%:R = m%:R :> 'F_p.
+
Lemma Fp_nat_mod m :
(m %% p)%:R = m%:R :> 'F_p.
-
Lemma char_Fp :
p \in [char 'F_p].
+
Lemma char_Fp :
p \in [char 'F_p].
-
Lemma char_Fp_0 :
p%:R = 0
:> 'F_p.
+
Lemma char_Fp_0 :
p%:R = 0
:> 'F_p.
-
Lemma unitFpE x :
((x%:R : 'F_p) \is a GRing.unit) = coprime p x.
+
Lemma unitFpE x :
((x%:R : 'F_p) \is a GRing.unit) = coprime p x.
End F_prime.
-
Lemma Fp_fieldMixin :
GRing.Field.mixin_of [the unitRingType of 'F_p].
+
Lemma Fp_fieldMixin :
GRing.Field.mixin_of [the unitRingType of 'F_p].
Definition Fp_idomainMixin :=
FieldIdomainMixin Fp_fieldMixin.
-
Canonical Fp_idomainType :=
Eval hnf in IdomainType 'F_p Fp_idomainMixin.
-
Canonical Fp_finIdomainType :=
Eval hnf in [finIdomainType of 'F_p].
-
Canonical Fp_fieldType :=
Eval hnf in FieldType 'F_p Fp_fieldMixin.
-
Canonical Fp_finFieldType :=
Eval hnf in [finFieldType of 'F_p].
+
Canonical Fp_idomainType :=
Eval hnf in IdomainType 'F_p Fp_idomainMixin.
+
Canonical Fp_finIdomainType :=
Eval hnf in [finIdomainType of 'F_p].
+
Canonical Fp_fieldType :=
Eval hnf in FieldType 'F_p Fp_fieldMixin.
+
Canonical Fp_finFieldType :=
Eval hnf in [finFieldType of 'F_p].
Canonical Fp_decFieldType :=
-
Eval hnf in [decFieldType of 'F_p for Fp_finFieldType].
+
Eval hnf in [decFieldType of 'F_p for Fp_finFieldType].
End PrimeField.
+
+
+
Canonical Zp_countZmodType m :=
[countZmodType of 'I_m.+1].
+
Canonical Zp_countRingType m :=
[countRingType of 'I_m.+2].
+
Canonical Zp_countComRingType m :=
[countComRingType of 'I_m.+2].
+
Canonical Zp_countUnitRingType m :=
[countUnitRingType of 'I_m.+2].
+
Canonical Zp_countComUnitRingType m :=
[countComUnitRingType of 'I_m.+2].
+
Canonical Fp_countIdomainType p :=
[countIdomainType of 'F_p].
+
Canonical Fp_countFieldType p :=
[countFieldType of 'F_p].
+
Canonical Fp_countDecFieldType p :=
[countDecFieldType of 'F_p].
--
cgit v1.2.3