diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.field.algebraics_fundamentals.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.field.algebraics_fundamentals.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.algebraics_fundamentals.html | 179 |
1 files changed, 179 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html b/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html new file mode 100644 index 0000000..d4379d5 --- /dev/null +++ b/docs/htmldoc/mathcomp.field.algebraics_fundamentals.html @@ -0,0 +1,179 @@ +<!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/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<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 countalg.v 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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#decidable"><span class="id" title="definition">decidable</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">p</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#e6408d45e92e642f7d1652448339ba09"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#e6408d45e92e642f7d1652448339ba09"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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#b033a3d34e421a2439563f5ffdab0b9b"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><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/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">L</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><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/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">&</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">{</span></a><span class="id" title="var">conj</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.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/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#611abc97cba304de784fa909dbdea1fa"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><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 |