From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- .../mathcomp.field.algebraics_fundamentals.html | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) (limited to 'docs/htmldoc/mathcomp.field.algebraics_fundamentals.html') diff --git a/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html b/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html index d4379d5..4a5005e 100644 --- a/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html +++ b/docs/htmldoc/mathcomp.field.algebraics_fundamentals.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.

@@ -41,7 +40,7 @@ algebraics as a subfield. To avoid some duplication a few basic properties of the algebraics, such as the existence of minimal polynomials, that are required by the proof of the Theorem, are also proved here. - The main theorem of countalg.v supplies us directly with an algebraic + The main theorem of closed_field supplies us directly with an algebraic closure of the rationals (as the rationals are a countable field), so all we really need to construct is a conjugation automorphism that exchanges the two roots (i and -i) of X^2 + 1, and fixes a (real) subfield of @@ -139,21 +138,21 @@
Lemma rat_algebraic_archimedean (C : numFieldType) (QtoC : Qmorphism C) :
-  integralRange QtoC → Num.archimedean_axiom C.
+  integralRange QtoC → Num.archimedean_axiom C.

-Definition decidable_embedding sT T (f : sT → T) :=
-  ∀ y, decidable (∃ x, y = f x).
+Definition decidable_embedding sT T (f : sT → T) :=
+  ∀ y, decidable (∃ x, y = f x).

Lemma rat_algebraic_decidable (C : fieldType) (QtoC : Qmorphism C) :
-  integralRange QtoC → decidable_embedding QtoC.
+  integralRange QtoC → decidable_embedding QtoC.

Lemma minPoly_decidable_closure
-  (F : fieldType) (L : closedFieldType) (FtoL : {rmorphism F → L}) x :
-    decidable_embedding FtoL → integralOver FtoL x →
-  {p | [/\ p \is monic, root (p ^ FtoL) x & irreducible_poly p]}.
+  (F : fieldType) (L : closedFieldType) (FtoL : {rmorphism F → L}) x :
+    decidable_embedding FtoL → integralOver FtoL x →
+  {p | [/\ p \is monic, root (p ^ FtoL) x & irreducible_poly p]}.

Lemma alg_integral (F : fieldType) (L : fieldExtType F) :
@@ -164,8 +163,8 @@
Theorem Fundamental_Theorem_of_Algebraics :
-  {L : closedFieldType &
-     {conj : {rmorphism L → L} | involutive conj & ¬ conj =1 id}}.
+  {L : closedFieldType &
+     {conj : {rmorphism L → L} | involutive conj & ¬ conj =1 id}}.
-- cgit v1.2.3