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.algnum.html | 206 ++++++++++++++++---------------- 1 file changed, 102 insertions(+), 104 deletions(-) (limited to 'docs/htmldoc/mathcomp.field.algnum.html') diff --git a/docs/htmldoc/mathcomp.field.algnum.html b/docs/htmldoc/mathcomp.field.algnum.html index ea7733e..fe44530 100644 --- a/docs/htmldoc/mathcomp.field.algnum.html +++ b/docs/htmldoc/mathcomp.field.algnum.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.

@@ -69,7 +68,7 @@

-Local Hint Resolve (@intr_inj _ : injective ZtoC).
+Local Hint Resolve (intr_inj : injective ZtoC) : core.

@@ -79,33 +78,33 @@
Lemma algC_PET (s : seq algC) :
-  {z | ∃ a : nat ^ size s, z = \sum_(i < size s) s`_i *+ a i
-     & ∃ ps, s = [seq (pQtoC p).[z] | p <- ps]}.
+  {z | ∃ a : nat ^ size s, z = \sum_(i < size s) s`_i *+ a i
+     & ∃ ps, s = [seq (pQtoC p).[z] | p <- ps]}.

Canonical subfx_unitAlgType (F L : fieldType) iota (z : L) p :=
-  Eval hnf in [unitAlgType F of subFExtend iota z p].
+  Eval hnf in [unitAlgType F of subFExtend iota z p].

Lemma num_field_exists (s : seq algC) :
-  {Qs : fieldExtType rat & {QsC : {rmorphism Qs → algC}
-   & {s1 : seq Qs | map QsC s1 = s & <<1 & s1>>%VS = fullv}}}.
+  {Qs : fieldExtType rat & {QsC : {rmorphism Qs → algC}
+   & {s1 : seq Qs | map QsC s1 = s & <<1 & s1>>%VS = fullv}}}.

Definition in_Crat_span s x :=
-  ∃ a : rat ^ size s, x = \sum_i QtoC (a i) × s`_i.
+  ∃ a : rat ^ size s, x = \sum_i QtoC (a i) × s`_i.

-Fact Crat_span_subproof s x : decidable (in_Crat_span s x).
+Fact Crat_span_subproof s x : decidable (in_Crat_span s x).

-Definition Crat_span s : pred algC := Crat_span_subproof s.
-Lemma Crat_spanP s x : reflect (in_Crat_span s x) (x \in Crat_span s).
- Fact Crat_span_key s : pred_key (Crat_span s).
-Canonical Crat_span_keyed s := KeyedPred (Crat_span_key s).
+Definition Crat_span s : pred algC := Crat_span_subproof s.
+Lemma Crat_spanP s x : reflect (in_Crat_span s x) (x \in Crat_span s).
+ Fact Crat_span_key s : pred_key (Crat_span s).
+Canonical Crat_span_keyed s := KeyedPred (Crat_span_key s).

-Lemma mem_Crat_span s : {subset s ≤ Crat_span s}.
+Lemma mem_Crat_span s : {subset s ≤ Crat_span s}.

Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s).
@@ -120,14 +119,14 @@ Implicit Type rR : unitRingType.

-Lemma alg_num_field (Qz : fieldExtType rat) a : a%:A = ratr a :> Qz.
+Lemma alg_num_field (Qz : fieldExtType rat) a : a%:A = ratr a :> Qz.

-Lemma rmorphZ_num (Qz : fieldExtType rat) rR (f : {rmorphism Qz → rR}) a x :
-  f (a *: x) = ratr a × f x.
+Lemma rmorphZ_num (Qz : fieldExtType rat) rR (f : {rmorphism Qz → rR}) a x :
+  f (a *: x) = ratr a × f x.

-Lemma fmorph_numZ (Qz1 Qz2 : fieldExtType rat) (f : {rmorphism Qz1 → Qz2}) :
+Lemma fmorph_numZ (Qz1 Qz2 : fieldExtType rat) (f : {rmorphism Qz1 → Qz2}) :
  scalable f.
Definition NumLRmorphism Qz1 Qz2 f := AddLRMorphism (@fmorph_numZ Qz1 Qz2 f).
@@ -138,13 +137,13 @@ Section NumFieldProj.

-Variables (Qn : fieldExtType rat) (QnC : {rmorphism Qn → algC}).
+Variables (Qn : fieldExtType rat) (QnC : {rmorphism Qn → algC}).

-Lemma Crat_spanZ b a : {in Crat_span b, ∀ x, ratr a × x \in Crat_span b}.
+Lemma Crat_spanZ b a : {in Crat_span b, ∀ x, ratr a × x \in Crat_span b}.

-Lemma Crat_spanM b : {in Crat & Crat_span b, ∀ a x, a × x \in Crat_span b}.
+Lemma Crat_spanM b : {in Crat & Crat_span b, ∀ a x, a × x \in Crat_span b}.

@@ -154,24 +153,24 @@ would require a limit construction.
-Lemma num_field_proj : {CtoQn | CtoQn 0 = 0 & cancel QnC CtoQn}.
+Lemma num_field_proj : {CtoQn | CtoQn 0 = 0 & cancel QnC CtoQn}.

-Lemma restrict_aut_to_num_field (nu : {rmorphism algC → algC}) :
-    (∀ x, ∃ y, nu (QnC x) = QnC y) →
-  {nu0 : {lrmorphism Qn → Qn} | {morph QnC : x / nu0 x >-> nu x}}.
+Lemma restrict_aut_to_num_field (nu : {rmorphism algC → algC}) :
+    (∀ x, ∃ y, nu (QnC x) = QnC y) →
+  {nu0 : {lrmorphism Qn → Qn} | {morph QnC : x / nu0 x >-> nu x}}.

-Lemma map_Qnum_poly (nu : {rmorphism algC → algC}) p :
-  p \in polyOver 1%VS → map_poly (nu \o QnC) p = (map_poly QnC p).
+Lemma map_Qnum_poly (nu : {rmorphism algC → algC}) p :
+  p \in polyOver 1%VS → map_poly (nu \o QnC) p = (map_poly QnC p).

End NumFieldProj.

Lemma restrict_aut_to_normal_num_field (Qn : splittingFieldType rat)
-  (QnC : {rmorphism Qn → algC})(nu : {rmorphism algC → algC}) :
-    {nu0 : {lrmorphism Qn → Qn} | {morph QnC : x / nu0 x >-> nu x}}.
+  (QnC : {rmorphism Qn → algC})(nu : {rmorphism algC → algC}) :
+    {nu0 : {lrmorphism Qn → Qn} | {morph QnC : x / nu0 x >-> nu x}}.

@@ -182,21 +181,21 @@

-Lemma dec_Cint_span (V : vectType algC) m (s : m.-tuple V) v :
-  decidable (inIntSpan s v).
+Lemma dec_Cint_span (V : vectType algC) m (s : m.-tuple V) v :
+  decidable (inIntSpan s v).

-Definition Cint_span (s : seq algC) : pred algC :=
-  fun x ⇒ dec_Cint_span (in_tuple [seq \row_(i < 1) y | y <- s]) (\row_i x).
-Fact Cint_span_key s : pred_key (Cint_span s).
-Canonical Cint_span_keyed s := KeyedPred (Cint_span_key s).
+Definition Cint_span (s : seq algC) : pred algC :=
+  fun x ⇒ dec_Cint_span (in_tuple [seq \row_(i < 1) y | y <- s]) (\row_i x).
+Fact Cint_span_key s : pred_key (Cint_span s).
+Canonical Cint_span_keyed s := KeyedPred (Cint_span_key s).

-Lemma Cint_spanP n (s : n.-tuple algC) x :
-  reflect (inIntSpan s x) (x \in Cint_span s).
+Lemma Cint_spanP n (s : n.-tuple algC) x :
+  reflect (inIntSpan s x) (x \in Cint_span s).

-Lemma mem_Cint_span s : {subset s ≤ Cint_span s}.
+Lemma mem_Cint_span s : {subset s ≤ Cint_span s}.

Lemma Cint_span_zmod_closed s : zmod_closed (Cint_span s).
@@ -212,8 +211,8 @@
Lemma extend_algC_subfield_aut (Qs : fieldExtType rat)
-  (QsC : {rmorphism Qs → algC}) (phi : {rmorphism Qs → Qs}) :
-  {nu : {rmorphism algC → algC} | {morph QsC : x / phi x >-> nu x}}.
+  (QsC : {rmorphism Qs → algC}) (phi : {rmorphism Qs → Qs}) :
+  {nu : {rmorphism algC → algC} | {morph QsC : x / phi x >-> nu x}}.

@@ -223,8 +222,8 @@
Lemma Qn_aut_exists k n :
-    coprime k n →
-  {u : {rmorphism algC → algC} | ∀ z, z ^+ n = 1 → u z = z ^+ k}.
+    coprime k n →
+  {u : {rmorphism algC → algC} | ∀ z, z ^+ n = 1 → u z = z ^+ k}.

@@ -235,37 +234,36 @@

-Definition Aint : pred_class :=
-  fun x : algC ⇒ minCpoly x \is a polyOver Cint.
-Fact Aint_key : pred_key Aint.
-Canonical Aint_keyed := KeyedPred Aint_key.
+Definition Aint : {pred algC} := fun x ⇒ minCpoly x \is a polyOver Cint.
+Fact Aint_key : pred_key Aint.
+Canonical Aint_keyed := KeyedPred Aint_key.

Lemma root_monic_Aint p x :
-  root p x → p \is monic → p \is a polyOver Cint → x \in Aint.
+  root p x → p \is monic → p \is a polyOver Cint → x \in Aint.

-Lemma Cint_rat_Aint z : z \in Crat → z \in Aint → z \in Cint.
+Lemma Cint_rat_Aint z : z \in Crat → z \in Aint → z \in Cint.

-Lemma Aint_Cint : {subset Cint ≤ Aint}.
+Lemma Aint_Cint : {subset Cint ≤ Aint}.

-Lemma Aint_int x : x%:~R \in Aint.
+Lemma Aint_int x : x%:~R \in Aint.

-Lemma Aint0 : 0 \in Aint.
-Lemma Aint1 : 1 \in Aint.
-Hint Resolve Aint0 Aint1.
+Lemma Aint0 : 0 \in Aint.
+Lemma Aint1 : 1 \in Aint.
+Hint Resolve Aint0 Aint1 : core.

-Lemma Aint_unity_root n x : (n > 0)%N → n.-unity_root x → x \in Aint.
+Lemma Aint_unity_root n x : (n > 0)%N → n.-unity_root x → x \in Aint.

-Lemma Aint_prim_root n z : n.-primitive_root z → z \in Aint.
+Lemma Aint_prim_root n z : n.-primitive_root z → z \in Aint.

-Lemma Aint_Cnat : {subset Cnat ≤ Aint}.
+Lemma Aint_Cnat : {subset Cnat ≤ Aint}.

@@ -275,13 +273,13 @@
Lemma Aint_subring_exists (X : seq algC) :
-    {subset X ≤ Aint} →
-  {S : pred algC &
+    {subset X ≤ Aint} →
+  {S : pred algC &
     (*a*) subring_closed S
-  ∧ (*b*) {subset X ≤ S}
-   & (*c*) {Y : {n : nat & n.-tuple algC} &
-                {subset tagged Y ≤ S}
-              & ∀ x, reflect (inIntSpan (tagged Y) x) (x \in S)}}.
+  ∧ (*b*) {subset X ≤ S}
+   & (*c*) {Y : {n : nat & n.-tuple algC} &
+                {subset tagged Y ≤ S}
+              & ∀ x, reflect (inIntSpan (tagged Y) x) (x \in S)}}.

Section AlgIntSubring.
@@ -296,9 +294,9 @@ This is Isaacs, Theorem (3.4).
-Theorem fin_Csubring_Aint S n (Y : n.-tuple algC) :
-     mulr_closed S → (∀ x, reflect (inIntSpan Y x) (x \in S)) →
-  {subset S ≤ Aint}.
+Theorem fin_Csubring_Aint S n (Y : n.-tuple algC) :
+     mulr_closed S → (∀ x, reflect (inIntSpan Y x) (x \in S)) →
+  {subset S ≤ Aint}.

@@ -320,18 +318,18 @@ End AlgIntSubring.

-Lemma Aint_aut (nu : {rmorphism algC → algC}) x :
-  (nu x \in Aint) = (x \in Aint).
+Lemma Aint_aut (nu : {rmorphism algC → algC}) x :
+  (nu x \in Aint) = (x \in Aint).

-Definition dvdA (e : Algebraics.divisor) : pred_class :=
-  fun z : algC ⇒ if e == 0 then z == 0 else z / e \in Aint.
-Fact dvdA_key e : pred_key (dvdA e).
-Canonical dvdA_keyed e := KeyedPred (dvdA_key e).
+Definition dvdA (e : Algebraics.divisor) : {pred algC} :=
+  fun z ⇒ if e == 0 then z == 0 else z / e \in Aint.
+Fact dvdA_key e : pred_key (dvdA e).
+Canonical dvdA_keyed e := KeyedPred (dvdA_key e).
Delimit Scope algC_scope with A.
Delimit Scope algC_expanded_scope with Ax.
-Notation "e %| x" := (x \in dvdA e) : algC_expanded_scope.
-Notation "e %| x" := (@in_mem Algebraics.divisor x (mem (dvdA e))) : algC_scope.
+Notation "e %| x" := (x \in dvdA e) : algC_expanded_scope.
+Notation "e %| x" := (@in_mem Algebraics.divisor x (mem (dvdA e))) : algC_scope.

Fact dvdA_zmod_closed e : zmod_closed (dvdA e).
@@ -340,82 +338,82 @@ Canonical dvdA_zmodPred e := ZmodPred (dvdA_zmod_closed e).

-Definition eqAmod (e x y : Algebraics.divisor) := (e %| x - y)%A.
-Notation "x == y %[mod e ]" := (eqAmod e x y) : algC_scope.
-Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope.
+Definition eqAmod (e x y : Algebraics.divisor) := (e %| x - y)%A.
+Notation "x == y %[mod e ]" := (eqAmod e x y) : algC_scope.
+Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope.

-Lemma eqAmod_refl e x : (x == x %[mod e])%A.
- Hint Resolve eqAmod_refl.
+Lemma eqAmod_refl e x : (x == x %[mod e])%A.
+ Hint Resolve eqAmod_refl : core.

-Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A.
+Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A.

Lemma eqAmod_trans e y x z :
-  (x == y %[mod e] → y == z %[mod e] → x == z %[mod e])%A.
+  (x == y %[mod e] → y == z %[mod e] → x == z %[mod e])%A.

Lemma eqAmod_transl e x y z :
-  (x == y %[mod e])%A → (x == z %[mod e])%A = (y == z %[mod e])%A.
+  (x == y %[mod e])%A → (x == z %[mod e])%A = (y == z %[mod e])%A.

Lemma eqAmod_transr e x y z :
-  (x == y %[mod e])%A → (z == x %[mod e])%A = (z == y %[mod e])%A.
+  (x == y %[mod e])%A → (z == x %[mod e])%A = (z == y %[mod e])%A.

-Lemma eqAmod0 e x : (x == 0 %[mod e])%A = (e %| x)%A.
+Lemma eqAmod0 e x : (x == 0 %[mod e])%A = (e %| x)%A.

-Lemma eqAmodN e x y : (- x == y %[mod e])%A = (x == - y %[mod e])%A.
+Lemma eqAmodN e x y : (- x == y %[mod e])%A = (x == - y %[mod e])%A.

-Lemma eqAmodDr e x y z : (y + x == z + x %[mod e])%A = (y == z %[mod e])%A.
+Lemma eqAmodDr e x y z : (y + x == z + x %[mod e])%A = (y == z %[mod e])%A.

-Lemma eqAmodDl e x y z : (x + y == x + z %[mod e])%A = (y == z %[mod e])%A.
+Lemma eqAmodDl e x y z : (x + y == x + z %[mod e])%A = (y == z %[mod e])%A.

Lemma eqAmodD e x1 x2 y1 y2 :
-  (x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 + y1 == x2 + y2 %[mod e])%A.
+  (x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 + y1 == x2 + y2 %[mod e])%A.

-Lemma eqAmodm0 e : (e == 0 %[mod e])%A.
- Hint Resolve eqAmodm0.
+Lemma eqAmodm0 e : (e == 0 %[mod e])%A.
+ Hint Resolve eqAmodm0 : core.

Lemma eqAmodMr e :
-  {in Aint, ∀ z x y, x == y %[mod e] → x × z == y × z %[mod e]}%A.
+  {in Aint, ∀ z x y, x == y %[mod e] → x × z == y × z %[mod e]}%A.

Lemma eqAmodMl e :
-  {in Aint, ∀ z x y, x == y %[mod e] → z × x == z × y %[mod e]}%A.
+  {in Aint, ∀ z x y, x == y %[mod e] → z × x == z × y %[mod e]}%A.

-Lemma eqAmodMl0 e : {in Aint, ∀ x, x × e == 0 %[mod e]}%A.
+Lemma eqAmodMl0 e : {in Aint, ∀ x, x × e == 0 %[mod e]}%A.

-Lemma eqAmodMr0 e : {in Aint, ∀ x, e × x == 0 %[mod e]}%A.
+Lemma eqAmodMr0 e : {in Aint, ∀ x, e × x == 0 %[mod e]}%A.

-Lemma eqAmod_addl_mul e : {in Aint, ∀ x y, x × e + y == y %[mod e]}%A.
+Lemma eqAmod_addl_mul e : {in Aint, ∀ x y, x × e + y == y %[mod e]}%A.

-Lemma eqAmodM e : {in Aint &, ∀ x1 y2 x2 y1,
-  x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 × y1 == x2 × y2 %[mod e]}%A.
+Lemma eqAmodM e : {in Aint &, ∀ x1 y2 x2 y1,
+  x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 × y1 == x2 × y2 %[mod e]}%A.

Lemma eqAmod_rat :
-  {in Crat & &, ∀ e m n, (m == n %[mod e])%A = (m == n %[mod e])%C}.
+  {in Crat & &, ∀ e m n, (m == n %[mod e])%A = (m == n %[mod e])%C}.

-Lemma eqAmod0_rat : {in Crat &, ∀ e n, (n == 0 %[mod e])%A = (e %| n)%C}.
+Lemma eqAmod0_rat : {in Crat &, ∀ e n, (n == 0 %[mod e])%A = (e %| n)%C}.

-Lemma eqAmod_nat (e m n : nat) : (m == n %[mod e])%A = (m == n %[mod e])%N.
+Lemma eqAmod_nat (e m n : nat) : (m == n %[mod e])%A = (m == n %[mod e])%N.

-Lemma eqAmod0_nat (e m : nat) : (m == 0 %[mod e])%A = (e %| m)%N.
+Lemma eqAmod0_nat (e m : nat) : (m == 0 %[mod e])%A = (e %| m)%N.

@@ -428,16 +426,16 @@
Definition orderC x :=
  let p := minCpoly x in
-  oapp val 0%N [pick n : 'I_(2 × size p ^ 2) | p == intrp 'Phi_n].
+  oapp val 0%N [pick n : 'I_(2 × size p ^ 2) | p == intrp 'Phi_n].

-Notation "#[ x ]" := (orderC x) : C_scope.
+Notation "#[ x ]" := (orderC x) : C_scope.

-Lemma exp_orderC x : x ^+ #[x]%C = 1.
+Lemma exp_orderC x : x ^+ #[x]%C = 1.

-Lemma dvdn_orderC x n : (#[x]%C %| n)%N = (x ^+ n == 1).
+Lemma dvdn_orderC x n : (#[x]%C %| n)%N = (x ^+ n == 1).
-- cgit v1.2.3