diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.field.algebraics_fundamentals.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.field.algebraics_fundamentals.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.algebraics_fundamentals.html | 178 |
1 files changed, 0 insertions, 178 deletions
diff --git a/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html b/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html deleted file mode 100644 index 4a5005e..0000000 --- a/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html +++ /dev/null @@ -1,178 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.field.algebraics_fundamentals</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.field.algebraics_fundamentals</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - The main result in this file is the existence theorem that underpins the - construction of the algebraic numbers in file algC.v. This theorem simply - asserts the existence of an algebraically closed field with an - automorphism of order 2, and dubbed the Fundamental_Theorem_of_Algebraics - because it is essentially the Fundamental Theorem of Algebra for algebraic - numbers (the more familiar version for complex numbers can be derived by - continuity). - Although our proof does indeed construct exactly the algebraics, we - choose not to expose this in the statement of our Theorem. In algC.v we - construct the norm and partial order of the "complex field" introduced by - the Theorem; as these imply is has characteristic 0, we then get the - 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 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 - index 2. This does not require actually constructing this field: the - kHomExtend construction from galois.v supplies us with an automorphism - conj_n of the number field Q[z_n] = Q[x_n, i] for any x_n such that Q[x_n] - does not contain i (e.g., such that Q[x_n] is real). As conj_n will extend - conj_m when Q[x_n] contains x_m, it therefore suffices to construct a - sequence x_n such that - (1) For each n, Q[x_n] is a REAL field containing Q[x_m] for all m <= n. - (2) Each z in C belongs to Q[z_n] = Q[x_n, i] for large enough n. - This, of course, amounts to proving the Fundamental Theorem of Algebra. - Indeed, we use a constructive variant of Artin's algebraic proof of that - Theorem to replace (2) by - (3) Each monic polynomial over Q[x_m] whose constant term is -c^2 for some - c in Q[x_m] has a root in Q[x_n] for large enough n. - We then ensure (3) by setting Q[x_n+1] = Q[x_n, y] where y is the root of - of such a polynomial p found by dichotomy in some interval [0, b] with b - suitably large (such that p[b] >= 0), and p is obtained by decoding n into - a triple (m, p, c) that satisfies the conditions of (3) (taking x_n+1=x_n - if this is not the case), thereby ensuring that all such triples are - ultimately considered. - In more detail, the 600-line proof consists in six (uneven) parts: - (A) - Construction of number fields (~ 100 lines): in order to make use of - the theory developped in falgebra, fieldext, separable and galois we - construct a separate fielExtType Q z for the number field Q[z], with - z in C, the closure of rat supplied by countable_algebraic_closure. - The morphism (ofQ z) maps Q z to C, and the Primitive Element Theorem - lets us define a predicate sQ z characterizing the image of (ofQ z), - as well as a partial inverse (inQ z) to (ofQ z). - (B) - Construction of the real extension Q[x, y] (~ 230 lines): here y has - to be a root of a polynomial p over Q[x] satisfying the conditions of - (3), and Q[x] should be real and archimedean, which we represent by - a morphism from Q x to some archimedean field R, as the ssrnum and - fieldext structures are not compatible. The construction starts by - weakening the condition p[0] = -c^2 to p[0] <= 0 (in R), then reducing - to the case where p is the minimal polynomial over Q[x] of some y (in - some Q[w] that contains x and all roots of p). Then we only need to - construct a realFieldType structure for Q[t] = Q[x,y] (we don't even - need to show it is consistent with that of R). This amounts to fixing - the sign of all z != 0 in Q[t], consistently with arithmetic in Q[t]. - Now any such z is equal to q[y] for some q in Q[x] [X] coprime with p. - Then up + vq = 1 for Bezout coefficients u and v. As p is monic, there - is some b0 >= 0 in R such that p changes sign in ab0 = [0; b0]. As R - is archimedean, some iteration of the binary search for a root of p in - ab0 will yield an interval ab_n such that |up[d]| < 1/2 for d in ab_n. - Then |q[d]| > 1/2M > 0 for any upper bound M on |v[X]| in ab0, so q - cannot change sign in ab_n (as then root-finding in ab_n would yield a - d with |Mq[d]| < 1/2), so we can fix the sign of z to that of q in - ab_n. - (C) - Construction of the x_n and z_n (~50 lines): x n is obtained by - iterating (B), starting with x_0 = 0, and then (A) and the PET yield - z n. We establish (1) and (3), and that the minimal polynomial of the - preimage i n of i over the preimage R n of Q[x_n] is X^2 + 1. - (D) - Establish (2), i.e., prove the FTA (~180 lines). We must depart from - Artin's proof because deciding membership in the union of the Q[x_n] - requires the FTA, i.e., we cannot (yet) construct a maximal real - subfield of C. We work around this issue by first reducing to the case - where Q[z] is Galois over Q and contains i, then using induction over - the degree of z over Q[z n] (i.e., the degree of a monic polynomial - over Q[z_n] that has z as a root). We can assume that z is not in - Q[z_n]; then it suffices to find some y in Q[z_n, z] \ Q[z_n] that is - also in Q[z_m] for some m > n, as then we can apply induction with the - minimal polynomial of z over Q[z_n, y]. In any Galois extension Q[t] - of Q that contains both z and z_n, Q[x_n, z] = Q[z_n, z] is Galois - over both Q[x_n] and Q[z_n]. If Gal(Q[x_n,z] / Q[x_n]) isn't a 2-group - take one of its Sylow 2-groups P; the minimal polynomial p of any - generator of the fixed field F of P over Q[x_n] has odd degree, hence - by (3) - p[X]p[-X] and thus p has a root y in some Q[x_m], hence in - Q[z_m]. As F is normal, y is in F, with minimal polynomial p, and y - is not in Q[z_n] = Q[x_n, i] since p has odd degree. Otherwise, - Gal(Q[z_n,z] / Q[z_n]) is a proper 2-group, and has a maximal subgroup - P of index 2. The fixed field F of P has a generator w over Q[z_n] - with w^2 in Q[z_n] \ Q[x_n], i.e. w^2 = u + 2iv with v != 0. From (3) - X^4 - uX^2 - v^2 has a root x in some Q[x_m]; then x != 0 as v != 0, - hence w^2 = y^2 for y = x + iv/x in Q[z_m], and y generates F. - (E) - Construct conj and conclude (~40 lines): conj z is defined as - conj n z with the n provided by (2); since each conj m is a morphism - of order 2 and conj z = conj m z for any m >= n, it follows that conj - is also a morphism of order 2. - Note that (C), (D) and (E) only depend on Q[x_n] not containing i; the - order structure is not used (hence we need not prove that the ordering of - Q[x_m] is consistent with that of Q[x_n] for m >= n). -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span> <span class="id" title="var">GRing.Theory</span> <span class="id" title="var">Num.Theory</span>.<br/> -<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rat_algebraic_archimedean"><span class="id" title="lemma">rat_algebraic_archimedean</span></a> (<span class="id" title="var">C</span> : <a class="idref" href="mathcomp.algebra.ssrnum.html#Num.NumField.Exports.numFieldType"><span class="id" title="abbreviation">numFieldType</span></a>) (<span class="id" title="var">QtoC</span> : <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#Qmorphism"><span class="id" title="abbreviation">Qmorphism</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#C"><span class="id" title="variable">C</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.mxpoly.html#integralRange"><span class="id" title="definition">integralRange</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#QtoC"><span class="id" title="variable">QtoC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#Num.archimedean_axiom"><span class="id" title="definition">Num.archimedean_axiom</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#C"><span class="id" title="variable">C</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="decidable_embedding"><span class="id" title="definition">decidable_embedding</span></a> <span class="id" title="var">sT</span> <span class="id" title="var">T</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#T"><span class="id" title="variable">T</span></a>) :=<br/> - <span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#decidable"><span class="id" title="definition">decidable</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rat_algebraic_decidable"><span class="id" title="lemma">rat_algebraic_decidable</span></a> (<span class="id" title="var">C</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<span class="id" title="var">QtoC</span> : <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#Qmorphism"><span class="id" title="abbreviation">Qmorphism</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#C"><span class="id" title="variable">C</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.mxpoly.html#integralRange"><span class="id" title="definition">integralRange</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#QtoC"><span class="id" title="variable">QtoC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#decidable_embedding"><span class="id" title="definition">decidable_embedding</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#QtoC"><span class="id" title="variable">QtoC</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="minPoly_decidable_closure"><span class="id" title="lemma">minPoly_decidable_closure</span></a><br/> - (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<span class="id" title="var">L</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ClosedField.Exports.closedFieldType"><span class="id" title="abbreviation">closedFieldType</span></a>) (<span class="id" title="var">FtoL</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>) <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#decidable_embedding"><span class="id" title="definition">decidable_embedding</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#FtoL"><span class="id" title="variable">FtoL</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.mxpoly.html#integralOver"><span class="id" title="definition">integralOver</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#FtoL"><span class="id" title="variable">FtoL</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">{</span></a><span class="id" title="var">p</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c94c2df86ca03f22f8f8b739cd7e1e88"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c94c2df86ca03f22f8f8b739cd7e1e88"><span class="id" title="notation">is</span></a> <a class="idref" href="mathcomp.algebra.poly.html#monic"><span class="id" title="definition">monic</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.field.algebraics_fundamentals.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#FtoL"><span class="id" title="variable">FtoL</span></a>) <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Field.irreducible_poly"><span class="id" title="definition">irreducible_poly</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="alg_integral"><span class="id" title="lemma">alg_integral</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<span class="id" title="var">L</span> : <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#F"><span class="id" title="variable">F</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.mxpoly.html#integralRange"><span class="id" title="definition">integralRange</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Theory.in_alg"><span class="id" title="abbreviation">in_alg</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#L"><span class="id" title="variable">L</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">DefaultKeying</span> <span class="id" title="var">GRing.DefaultPred</span>.<br/> - -<br/> -<span class="id" title="keyword">Theorem</span> <a name="Fundamental_Theorem_of_Algebraics"><span class="id" title="lemma">Fundamental_Theorem_of_Algebraics</span></a> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">L</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ClosedField.Exports.closedFieldType"><span class="id" title="abbreviation">closedFieldType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">{</span></a><span class="id" title="var">conj</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#involutive"><span class="id" title="definition">involutive</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#conj"><span class="id" title="variable">conj</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="mathcomp.field.algebraics_fundamentals.html#conj"><span class="id" title="variable">conj</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}</span></a>.<br/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |