htmldoc regenerated

1 files changed, 10 insertions, 11 deletions

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 @@
 <div class="code">
 <span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
 &nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</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>
@@ -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 @@
 
 <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/>
-&nbsp;&nbsp;<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/>
+&nbsp;&nbsp;<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/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/>
-&nbsp;&nbsp;<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/>
+<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/>
+&nbsp;&nbsp;<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/>
-&nbsp;&nbsp;<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/>
+&nbsp;&nbsp;<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/>
-&nbsp;&nbsp;(<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/>
-&nbsp;&nbsp;&nbsp;&nbsp;<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/>
-&nbsp;&nbsp;<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">&amp;</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/>
+&nbsp;&nbsp;(<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/>
+&nbsp;&nbsp;&nbsp;&nbsp;<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/>
+&nbsp;&nbsp;<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">&amp;</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/>
@@ -164,8 +163,8 @@
 
 <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/>
-&nbsp;&nbsp;<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">&amp;</span></a><br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<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">&amp;</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/>
+&nbsp;&nbsp;<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">&amp;</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<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">&amp;</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>