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.field.finfield.html | 177 +++++++++++++++--------------- 1 file changed, 88 insertions(+), 89 deletions(-) (limited to 'docs/htmldoc/mathcomp.field.finfield.html') diff --git a/docs/htmldoc/mathcomp.field.finfield.html b/docs/htmldoc/mathcomp.field.finfield.html index c6454db..398b5de 100644 --- a/docs/htmldoc/mathcomp.field.finfield.html +++ b/docs/htmldoc/mathcomp.field.finfield.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -90,10 +89,10 @@ Variable R : finRingType.

-Lemma finRing_nontrivial : [set: R] != 1%g.
+Lemma finRing_nontrivial : [set: R] != 1%g.

-Lemma finRing_gt1 : 1 < #|R|.
+Lemma finRing_gt1 : 1 < #|R|.

End FinRing.
@@ -105,26 +104,26 @@ Variable F : finFieldType.

-Lemma card_finField_unit : #|[set: {unit F}]| = #|F|.-1.
+Lemma card_finField_unit : #|[set: {unit F}]| = #|F|.-1.

-Definition finField_unit x (nz_x : x != 0) :=
-  FinRing.unit F (etrans (unitfE x) nz_x).
+Definition finField_unit x (nz_x : x != 0) :=
+  FinRing.unit F (etrans (unitfE x) nz_x).

-Lemma expf_card x : x ^+ #|F| = x :> F.
+Lemma expf_card x : x ^+ #|F| = x :> F.

-Lemma finField_genPoly : 'X^#|F| - 'X = \prod_x ('X - x%:P) :> {poly F}.
+Lemma finField_genPoly : 'X^#|F| - 'X = \prod_x ('X - x%:P) :> {poly F}.

-Lemma finCharP : {p | prime p & p \in [char F]}.
+Lemma finCharP : {p | prime p & p \in [char F]}.

-Lemma finField_is_abelem : is_abelem [set: F].
+Lemma finField_is_abelem : is_abelem [set: F].

-Lemma card_finCharP p n : #|F| = (p ^ n)%N → prime p → p \in [char F].
+Lemma card_finCharP p n : #|F| = (p ^ n)%N → prime p → p \in [char F].

End FinField.
@@ -140,23 +139,23 @@
Variable cvT : Vector.class_of F T.
-Let vT := Vector.Pack (Phant F) cvT T.
+Let vT := Vector.Pack (Phant F) cvT.

-Lemma card_vspace (V : {vspace vT}) : #|V| = (#|F| ^ \dim V)%N.
+Lemma card_vspace (V : {vspace vT}) : #|V| = (#|F| ^ \dim V)%N.

-Lemma card_vspacef : #|{: vT}%VS| = #|T|.
+Lemma card_vspacef : #|{: vT}%VS| = #|T|.

End Vector.

Variable caT : Falgebra.class_of F T.
-Let aT := Falgebra.Pack (Phant F) caT T.
+Let aT := Falgebra.Pack (Phant F) caT.

-Lemma card_vspace1 : #|(1%VS : {vspace aT})| = #|F|.
+Lemma card_vspace1 : #|(1%VS : {vspace aT})| = #|F|.

End CardVspace.
@@ -185,9 +184,9 @@ Canonical fieldExt_finType fT := FinType fT (VectFinMixin fT).

-Canonical Falg_finRingType aT := [finRingType of aT].
-Canonical fieldExt_finRingType fT := [finRingType of fT].
-Canonical fieldExt_finFieldType fT := [finFieldType of fT].
+Canonical Falg_finRingType aT := [finRingType of aT].
+Canonical fieldExt_finRingType fT := [finRingType of fT].
+Canonical fieldExt_finFieldType fT := [finFieldType of fT].

Lemma finField_splittingField_axiom fT : SplittingField.axiom fT.
@@ -206,7 +205,7 @@ Section PrimeChar.

-Variable p : nat.
+Variable p : nat.

Section PrimeCharRing.
@@ -215,49 +214,49 @@ Variable R0 : ringType.

-Definition PrimeCharType of p \in [char R0] : predArgType := R0.
+Definition PrimeCharType of p \in [char R0] : predArgType := R0.

-Hypothesis charRp : p \in [char R0].
-Implicit Types (a b : 'F_p) (x y : R).
+Hypothesis charRp : p \in [char R0].
+Implicit Types (a b : 'F_p) (x y : R).

-Canonical primeChar_eqType := [eqType of R].
-Canonical primeChar_choiceType := [choiceType of R].
-Canonical primeChar_zmodType := [zmodType of R].
-Canonical primeChar_ringType := [ringType of R].
+Canonical primeChar_eqType := [eqType of R].
+Canonical primeChar_choiceType := [choiceType of R].
+Canonical primeChar_zmodType := [zmodType of R].
+Canonical primeChar_ringType := [ringType of R].

-Definition primeChar_scale a x := a%:R × x.
+Definition primeChar_scale a x := a%:R × x.

-Let natrFp n : (inZp n : 'F_p)%:R = n%:R :> R.
+Let natrFp n : (inZp n : 'F_p)%:R = n%:R :> R.

-Lemma primeChar_scaleA a b x : a ×p: (b ×p: x) = (a × b) ×p: x.
+Lemma primeChar_scaleA a b x : a ×p: (b ×p: x) = (a × b) ×p: x.

-Lemma primeChar_scale1 : left_id 1 primeChar_scale.
+Lemma primeChar_scale1 : left_id 1 primeChar_scale.

-Lemma primeChar_scaleDr : right_distributive primeChar_scale +%R.
+Lemma primeChar_scaleDr : right_distributive primeChar_scale +%R.

-Lemma primeChar_scaleDl x : {morph primeChar_scale^~ x: a b / a + b}.
+Lemma primeChar_scaleDl x : {morph primeChar_scale^~ x: a b / a + b}.

Definition primeChar_lmodMixin :=
  LmodMixin primeChar_scaleA primeChar_scale1
            primeChar_scaleDr primeChar_scaleDl.
-Canonical primeChar_lmodType := LmodType 'F_p R primeChar_lmodMixin.
+Canonical primeChar_lmodType := LmodType 'F_p R primeChar_lmodMixin.

-Lemma primeChar_scaleAl : GRing.Lalgebra.axiom ( *%R : R → R → R).
- Canonical primeChar_LalgType := LalgType 'F_p R primeChar_scaleAl.
+Lemma primeChar_scaleAl : GRing.Lalgebra.axiom ( *%R : R → R → R).
+ Canonical primeChar_LalgType := LalgType 'F_p R primeChar_scaleAl.

Lemma primeChar_scaleAr : GRing.Algebra.axiom primeChar_LalgType.
- Canonical primeChar_algType := AlgType 'F_p R primeChar_scaleAr.
+ Canonical primeChar_algType := AlgType 'F_p R primeChar_scaleAr.

End PrimeCharRing.
@@ -266,87 +265,87 @@
Canonical primeChar_unitRingType (R : unitRingType) charRp :=
-  [unitRingType of type R charRp].
+  [unitRingType of type R charRp].
Canonical primeChar_unitAlgType (R : unitRingType) charRp :=
-  [unitAlgType 'F_p of type R charRp].
+  [unitAlgType 'F_p of type R charRp].
Canonical primeChar_comRingType (R : comRingType) charRp :=
-  [comRingType of type R charRp].
+  [comRingType of type R charRp].
Canonical primeChar_comUnitRingType (R : comUnitRingType) charRp :=
-  [comUnitRingType of type R charRp].
+  [comUnitRingType of type R charRp].
Canonical primeChar_idomainType (R : idomainType) charRp :=
-  [idomainType of type R charRp].
+  [idomainType of type R charRp].
Canonical primeChar_fieldType (F : fieldType) charFp :=
-  [fieldType of type F charFp].
+  [fieldType of type F charFp].

Section FinRing.

-Variables (R0 : finRingType) (charRp : p \in [char R0]).
+Variables (R0 : finRingType) (charRp : p \in [char R0]).

-Canonical primeChar_finType := [finType of R].
-Canonical primeChar_finZmodType := [finZmodType of R].
-Canonical primeChar_baseGroupType := [baseFinGroupType of R for +%R].
-Canonical primeChar_groupType := [finGroupType of R for +%R].
-Canonical primeChar_finRingType := [finRingType of R].
-Canonical primeChar_finLmodType := [finLmodType 'F_p of R].
-Canonical primeChar_finLalgType := [finLalgType 'F_p of R].
-Canonical primeChar_finAlgType := [finAlgType 'F_p of R].
+Canonical primeChar_finType := [finType of R].
+Canonical primeChar_finZmodType := [finZmodType of R].
+Canonical primeChar_baseGroupType := [baseFinGroupType of R for +%R].
+Canonical primeChar_groupType := [finGroupType of R for +%R].
+Canonical primeChar_finRingType := [finRingType of R].
+Canonical primeChar_finLmodType := [finLmodType 'F_p of R].
+Canonical primeChar_finLalgType := [finLalgType 'F_p of R].
+Canonical primeChar_finAlgType := [finAlgType 'F_p of R].

Let pr_p : prime p.

-Lemma primeChar_abelem : p.-abelem [set: R].
+Lemma primeChar_abelem : p.-abelem [set: R].

-Lemma primeChar_pgroup : p.-group [set: R].
+Lemma primeChar_pgroup : p.-group [set: R].

-Lemma order_primeChar x : x != 0 :> R → #[x]%g = p.
+Lemma order_primeChar x : x != 0 :> R → #[x]%g = p.

-Let n := logn p #|R|.
+Let n := logn p #|R|.

-Lemma card_primeChar : #|R| = (p ^ n)%N.
+Lemma card_primeChar : #|R| = (p ^ n)%N.

Lemma primeChar_vectAxiom : Vector.axiom n (primeChar_lmodType charRp).

Definition primeChar_vectMixin := Vector.Mixin primeChar_vectAxiom.
-Canonical primeChar_vectType := VectType 'F_p R primeChar_vectMixin.
+Canonical primeChar_vectType := VectType 'F_p R primeChar_vectMixin.

-Lemma primeChar_dimf : \dim {:primeChar_vectType} = n.
+Lemma primeChar_dimf : \dim {:primeChar_vectType} = n.

End FinRing.

Canonical primeChar_finUnitRingType (R : finUnitRingType) charRp :=
-  [finUnitRingType of type R charRp].
+  [finUnitRingType of type R charRp].
Canonical primeChar_finUnitAlgType (R : finUnitRingType) charRp :=
-  [finUnitAlgType 'F_p of type R charRp].
+  [finUnitAlgType 'F_p of type R charRp].
Canonical primeChar_FalgType (R : finUnitRingType) charRp :=
-  [FalgType 'F_p of type R charRp].
+  [FalgType 'F_p of type R charRp].
Canonical primeChar_finComRingType (R : finComRingType) charRp :=
-  [finComRingType of type R charRp].
+  [finComRingType of type R charRp].
Canonical primeChar_finComUnitRingType (R : finComUnitRingType) charRp :=
-  [finComUnitRingType of type R charRp].
+  [finComUnitRingType of type R charRp].
Canonical primeChar_finIdomainType (R : finIdomainType) charRp :=
-  [finIdomainType of type R charRp].
+  [finIdomainType of type R charRp].

Section FinField.

-Variables (F0 : finFieldType) (charFp : p \in [char F0]).
+Variables (F0 : finFieldType) (charFp : p \in [char F0]).

-Canonical primeChar_finFieldType := [finFieldType of F].
+Canonical primeChar_finFieldType := [finFieldType of F].
@@ -354,8 +353,8 @@ of the Canonical fieldType of F cannot be computed syntactically.
-Canonical primeChar_fieldExtType := [fieldExtType 'F_p of F for F0].
-Canonical primeChar_splittingFieldType := FinSplittingFieldType 'F_p F.
+Canonical primeChar_fieldExtType := [fieldExtType 'F_p of F for F0].
+Canonical primeChar_splittingFieldType := FinSplittingFieldType 'F_p F.

End FinField.
@@ -377,37 +376,37 @@ do not want to impose the FinVector instance here.
-Let order (L : vectType F) (K : {vspace L}) := (#|F| ^ \dim K)%N.
+Let order (L : vectType F) (K : {vspace L}) := (#|F| ^ \dim K)%N.

Section FinGalois.

Variable L : splittingFieldType F.
-Implicit Types (a b : F) (x y : L) (K E : {subfield L}).
+Implicit Types (a b : F) (x y : L) (K E : {subfield L}).

-Let galL K : galois K {:L}.
+Let galL K : galois K {:L}.

Fact galLgen K :
-  {alpha | generator 'Gal({:L} / K) alpha & ∀ x, alpha x = x ^+ order K}.
+  {alpha | generator 'Gal({:L} / K) alpha & ∀ x, alpha x = x ^+ order K}.

-Lemma finField_galois K E : (K ≤ E)%VS → galois K E.
+Lemma finField_galois K E : (K ≤ E)%VS → galois K E.

Lemma finField_galois_generator K E :
-   (K ≤ E)%VS →
- {alpha | generator 'Gal(E / K) alpha
-        & {in E, ∀ x, alpha x = x ^+ order K}}.
+   (K ≤ E)%VS →
+ {alpha | generator 'Gal(E / K) alpha
+        & {in E, ∀ x, alpha x = x ^+ order K}}.

End FinGalois.

-Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L}) a :
-  (a \in K) = (a ^+ order K == a).
+Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L}) a :
+  (a \in K) = (a ^+ order K == a).

End FinSplittingField.
@@ -438,15 +437,15 @@
Let map_poly_extField (F : fieldType) (L : fieldExtType F) :=
-  map_poly (in_alg L) : {poly F} → {poly L}.
+  map_poly (in_alg L) : {poly F} → {poly L}.

-Lemma FinSplittingFieldFor (F : finFieldType) (p : {poly F}) :
-  p != 0 → {L : splittingFieldType F | splittingFieldFor 1 p^%:A {:L}}.
+Lemma FinSplittingFieldFor (F : finFieldType) (p : {poly F}) :
+  p != 0 → {L : splittingFieldType F | splittingFieldFor 1 p^%:A {:L}}.

-Lemma PrimePowerField p k (m := (p ^ k)%N) :
-  prime p → 0 < k → {Fm : finFieldType | p \in [char Fm] & #|Fm| = m}.
+Lemma PrimePowerField p k (m := (p ^ k)%N) :
+  prime p → 0 < k → {Fm : finFieldType | p \in [char Fm] & #|Fm| = m}.

End FinFieldExists.
@@ -466,7 +465,7 @@ Implicit Types x y : R.

-Let lregR x : x != 0 → GRing.lreg x.
+Let lregR x : x != 0 → GRing.lreg x.

Lemma finDomain_field : GRing.Field.mixin_of R.
@@ -478,7 +477,7 @@ This is Witt's proof of Wedderburn's little theorem.
-Theorem finDomain_mulrC : @commutative R R *%R.
+Theorem finDomain_mulrC : @commutative R R *%R.

Definition FinDomainFieldType : finFieldType :=
@@ -488,12 +487,12 @@   let dom_class := @GRing.IntegralDomain.Class R com_unit_class domR in
  let field_class := @GRing.Field.Class R dom_class finDomain_field in
  let finfield_class := @FinRing.Field.Class R field_class fin_unit_class in
-  FinRing.Field.Pack finfield_class R.
+  FinRing.Field.Pack finfield_class.

-Definition FinDomainSplittingFieldType p (charRp : p \in [char R]) :=
+Definition FinDomainSplittingFieldType p (charRp : p \in [char R]) :=
   let RoverFp := @primeChar_splittingFieldType p FinDomainFieldType charRp in
-   [splittingFieldType 'F_p of R for RoverFp].
+   [splittingFieldType 'F_p of R for RoverFp].

End FinDomain.
-- cgit v1.2.3