aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc/index_global_R.html
diff options
context:
space:
mode:
authorEnrico Tassi2019-05-22 13:43:08 +0200
committerEnrico Tassi2019-05-22 15:34:14 +0200
commit748d716efb2f2f75946c8386e441ce1789806a39 (patch)
treefe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_global_R.html
parent415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_R.html')
-rw-r--r--docs/htmldoc/index_global_R.html152
1 files changed, 62 insertions, 90 deletions
diff --git a/docs/htmldoc/index_global_R.html b/docs/htmldoc/index_global_R.html
index 78fa42e..85289b0 100644
--- a/docs/htmldoc/index_global_R.html
+++ b/docs/htmldoc/index_global_R.html
@@ -4,7 +4,7 @@
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
-<title>mathcomp.ssreflect.tuple</title>
+<title>mathcomp.test_suite.hierarchy_test</title>
</head>
<body>
@@ -47,7 +47,7 @@
<td><a href="index_global_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_global_*.html">other</a></td>
-<td>(23233 entries)</td>
+<td>(23836 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
@@ -79,14 +79,14 @@
<td><a href="index_notation_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_notation_*.html">other</a></td>
-<td>(1373 entries)</td>
+<td>(1409 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index_module_A.html">A</a></td>
<td><a href="index_module_B.html">B</a></td>
<td><a href="index_module_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_module_D.html">D</a></td>
<td><a href="index_module_E.html">E</a></td>
<td><a href="index_module_F.html">F</a></td>
<td><a href="index_module_G.html">G</a></td>
@@ -111,7 +111,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -143,7 +143,7 @@
<td><a href="index_variable_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3475 entries)</td>
+<td>(3574 entries)</td>
</tr>
<tr>
<td>Library Index</td>
@@ -175,7 +175,7 @@
<td><a href="index_library_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(89 entries)</td>
+<td>(90 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
@@ -207,7 +207,7 @@
<td><a href="index_lemma_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(11853 entries)</td>
+<td>(12096 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
@@ -239,7 +239,7 @@
<td><a href="index_constructor_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(359 entries)</td>
+<td>(368 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
@@ -271,7 +271,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -303,14 +303,14 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(103 entries)</td>
+<td>(107 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index_projection_A.html">A</a></td>
<td><a href="index_projection_B.html">B</a></td>
<td><a href="index_projection_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_projection_D.html">D</a></td>
<td><a href="index_projection_E.html">E</a></td>
<td><a href="index_projection_F.html">F</a></td>
<td><a href="index_projection_G.html">G</a></td>
@@ -335,7 +335,7 @@
<td><a href="index_projection_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(266 entries)</td>
+<td>(273 entries)</td>
</tr>
<tr>
<td>Section Index</td>
@@ -367,7 +367,7 @@
<td><a href="index_section_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(1118 entries)</td>
+<td>(1140 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
@@ -399,7 +399,7 @@
<td><a href="index_abbreviation_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(691 entries)</td>
+<td>(728 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
@@ -431,14 +431,14 @@
<td><a href="index_definition_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3461 entries)</td>
+<td>(3596 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index_record_A.html">A</a></td>
<td>B</td>
<td><a href="index_record_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_record_D.html">D</a></td>
<td><a href="index_record_E.html">E</a></td>
<td><a href="index_record_F.html">F</a></td>
<td><a href="index_record_G.html">G</a></td>
@@ -463,14 +463,13 @@
<td><a href="index_record_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(185 entries)</td>
+<td>(189 entries)</td>
</tr>
</table>
<hr/><a name="global_R"></a><h2>R </h2>
<a href="mathcomp.field.finfield.html#R">R</a> [abbreviation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/>
<a href="mathcomp.field.finfield.html#R">R</a> [abbreviation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/>
<a href="mathcomp.character.mxabelem.html#r">r</a> [abbreviation, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rabstrX">rabstrX</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.fingroup.action.html#ract">ract</a> [definition, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
<a href="mathcomp.fingroup.action.html#ractE">ractE</a> [lemma, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
<a href="mathcomp.fingroup.action.html#ractpermE">ractpermE</a> [lemma, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
@@ -480,7 +479,6 @@
<a href="mathcomp.field.algC.html#raddfZ_Cint">raddfZ_Cint</a> [lemma, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
<a href="mathcomp.field.algC.html#raddfZ_Cnat">raddfZ_Cnat</a> [lemma, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#raddf_int_scalable">raddf_int_scalable</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.field.closed_field.html#ramulXnT">ramulXnT</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.fingroup.action.html#range">range</a> [abbreviation, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
<a href="mathcomp.solvable.abelian.html#rank">rank</a> [definition, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
<a href="mathcomp.solvable.abelian.html#rankJ">rankJ</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
@@ -608,6 +606,9 @@
<a href="mathcomp.ssreflect.path.html#rcons_path">rcons_path</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
<a href="mathcomp.ssreflect.tuple.html#rcons_tupleP">rcons_tupleP</a> [lemma, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#rcons_uniq">rcons_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#rcons_injr">rcons_injr</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#rcons_injl">rcons_injl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#rcons_inj">rcons_inj</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#rcons_cat">rcons_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#rcons_cons">rcons_cons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.fingroup.fingroup.html#rcoset">rcoset</a> [definition, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
@@ -641,21 +642,13 @@
<a href="mathcomp.fingroup.fingroup.html#rcoset_inj">rcoset_inj</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
<a href="mathcomp.fingroup.fingroup.html#rcoset1">rcoset1</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
<a href="mathcomp.character.character.html#rdegree">rdegree</a> [projection, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rdivpT">rdivpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rdvdpT">rdvdpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#RealLeAxiom">RealLeAxiom</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#RealLeMixin">RealLeMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrnum.html#RealLtMixin">RealLtMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#realz">realz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.interval.html#real_lersif_normr">real_lersif_normr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
+<a href="mathcomp.algebra.interval.html#real_lersif_norml">real_lersif_norml</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#real_lersifN">real_lersifN</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.field.closed_field.html#redivpT">redivpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#redivpTP">redivpTP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#redivpT_qf">redivpT_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#redivp_rec_loopP">redivp_rec_loopP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#redivp_rec_loopT_qf">redivp_rec_loopT_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#redivp_rec_loopTP">redivp_rec_loopTP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#redivp_rec_loop">redivp_rec_loop</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#redivp_rec_loopT">redivp_rec_loopT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.ssreflect.bigop.html#reducebig">reducebig</a> [definition, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#reducible_Socle1">reducible_Socle1</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#reducible_Socle">reducible_Socle</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
@@ -676,7 +669,7 @@
<a href="mathcomp.fingroup.morphism.html#ReflectProp.Main.H">ReflectProp.Main.H</a> [variable, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
<a href="mathcomp.fingroup.morphism.html#ReflectProp.Main.isoGH">ReflectProp.Main.isoGH</a> [variable, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
<a href="mathcomp.fingroup.morphism.html#ReflectProp.rT">ReflectProp.rT</a> [variable, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
-<a href="mathcomp.fingroup.morphism.html#6202b790dcb0ea1946ff79ad4eb4448e">_ \isog _</a> [notation, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
+<a href="mathcomp.fingroup.morphism.html#15b170ccfc7a6d3581c701a5a0793622">_ \isog _</a> [notation, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
<a href="mathcomp.algebra.vector.html#RegularVectType">RegularVectType</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
<a href="mathcomp.algebra.vector.html#RegularVectType.R">RegularVectType.R</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
<a href="mathcomp.field.galois.html#regular_splittingAxiom">regular_splittingAxiom</a> [lemma, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
@@ -691,6 +684,7 @@
<a href="mathcomp.algebra.vector.html#regular_vect_iso">regular_vect_iso</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
<a href="mathcomp.field.falgebra.html#regular_fullv">regular_fullv</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
<a href="mathcomp.ssreflect.bigop.html#reindex">reindex</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/>
+<a href="mathcomp.fingroup.perm.html#reindex_perm">reindex_perm</a> [abbreviation, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
<a href="mathcomp.fingroup.gproduct.html#reindex_bigcprod">reindex_bigcprod</a> [lemma, in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
<a href="mathcomp.character.character.html#reindex_irr_class">reindex_irr_class</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.inertia.html#reindex_cfclass">reindex_cfclass</a> [lemma, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
@@ -711,6 +705,7 @@
<a href="mathcomp.ssreflect.fingraph.html#RelAdjunction.sym_e">RelAdjunction.sym_e</a> [variable, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
<a href="mathcomp.ssreflect.fingraph.html#RelAdjunction.T">RelAdjunction.T</a> [variable, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
<a href="mathcomp.ssreflect.fingraph.html#RelAdjunction.T'">RelAdjunction.T'</a> [variable, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
+<a href="mathcomp.ssreflect.ssrbool.html#relpre">relpre</a> [definition, in <a href="mathcomp.ssreflect.ssrbool.html">mathcomp.ssreflect.ssrbool</a>]<br/>
<a href="mathcomp.ssreflect.fingraph.html#relU_sym">relU_sym</a> [lemma, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
<a href="mathcomp.ssreflect.path.html#rel_base">rel_base</a> [definition, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
<a href="mathcomp.ssreflect.fingraph.html#rel_adjunction">rel_adjunction</a> [abbreviation, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
@@ -850,7 +845,6 @@
<a href="mathcomp.character.character.html#Res_Iirr0">Res_Iirr0</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.character.html#Res_Iirr">Res_Iirr</a> [definition, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.character.html#Res_irr_neq0">Res_irr_neq0</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#Rev">Rev</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#rev">rev</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#revK">revK</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.path.html#rev_sorted">rev_sorted</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
@@ -869,7 +863,6 @@
<a href="mathcomp.ssreflect.fintype.html#rev_ordK">rev_ordK</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
<a href="mathcomp.ssreflect.fintype.html#rev_ord">rev_ord</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
<a href="mathcomp.ssreflect.fintype.html#rev_ord_proof">rev_ord_proof</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#Rev.T">Rev.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#rF">rF</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
<a href="mathcomp.solvable.alt.html#rfd">rfd</a> [definition, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
<a href="mathcomp.solvable.alt.html#rfdP">rfdP</a> [lemma, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
@@ -901,23 +894,7 @@
<a href="mathcomp.character.mxabelem.html#rG">rG</a> [abbreviation, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#rGB">rGB</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#rGB">rGB</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdpT">rgcdpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdpTP">rgcdpTP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdpTs">rgcdpTs</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdpTsP">rgcdpTsP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdpTs_qf">rgcdpTs_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdpT_qf">rgcdpT_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdp_loopT_qf">rgcdp_loopT_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdp_loopP">rgcdp_loopP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdp_loopT">rgcdp_loopT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgcdp_loop">rgcdp_loop</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.solvable.alt.html#rgd">rgd</a> [definition, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgdcopT">rgdcopT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgdcopTP">rgdcopTP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgdcopT_qf">rgdcopT_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgdcop_recT_qf">rgdcop_recT_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgdcop_recTP">rgdcop_recTP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rgdcop_recT">rgdcop_recT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.solvable.alt.html#rgdP">rgdP</a> [lemma, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
<a href="mathcomp.solvable.alt.html#rgd_fun">rgd_fun</a> [definition, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#rGf">rGf</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
@@ -1067,7 +1044,6 @@
<a href="mathcomp.character.mxrepresentation.html#rker_normal">rker_normal</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#rker_norm">rker_norm</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
<a href="mathcomp.character.mxabelem.html#rker_abelem">rker_abelem</a> [lemma, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rmodpT">rmodpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#rmorphMz">rmorphMz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#rmorphXz">rmorphXz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#rmorphzP">rmorphzP</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
@@ -1075,7 +1051,6 @@
<a href="mathcomp.algebra.poly.html#rmorph_unity_root">rmorph_unity_root</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.algebra.poly.html#rmorph_root">rmorph_root</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#rmorph_int">rmorph_int</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rmulpT">rmulpT</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.algebra.poly.html#root">root</a> [definition, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.ssreflect.fingraph.html#root">root</a> [definition, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
<a href="mathcomp.algebra.poly.html#rootC">rootC</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
@@ -1087,6 +1062,7 @@
<a href="mathcomp.algebra.poly.html#rootPf">rootPf</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.algebra.poly.html#rootPt">rootPt</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.ssreflect.fingraph.html#roots">roots</a> [definition, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
+<a href="mathcomp.algebra.poly.html#roots_geq_poly_eq0">roots_geq_poly_eq0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.ssreflect.fingraph.html#roots_root">roots_root</a> [lemma, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
<a href="mathcomp.algebra.poly.html#rootX">rootX</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.algebra.poly.html#rootZ">rootZ</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
@@ -1117,6 +1093,8 @@
<a href="mathcomp.ssreflect.seq.html#RotCompLemmas.T">RotCompLemmas.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#rotK">rotK</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#rotr">rotr</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#RotRcons">RotRcons</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#RotRcons.T">RotRcons.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#rotrK">rotrK</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#RotrLemmas">RotrLemmas</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#RotrLemmas.n0">RotrLemmas.n0</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
@@ -1255,22 +1233,22 @@
<a href="mathcomp.algebra.mxalgebra.html#RowSpaceTheory.SumExpr.Binary.S2">RowSpaceTheory.SumExpr.Binary.S2</a> [variable, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
<a href="mathcomp.algebra.mxalgebra.html#RowSpaceTheory.SumExpr.Nary">RowSpaceTheory.SumExpr.Nary</a> [section, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
<a href="mathcomp.algebra.mxalgebra.html#RowSpaceTheory.unitmx1F">RowSpaceTheory.unitmx1F</a> [variable, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ef798e67335a7fc58f8072263210ea96">_ :\: _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#21ad23dcb443b600284c1cd39a51fde1">\bigcap_ ( _ | _ ) _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#2caeadd15d44390ff4fc0106b8e96c32">_ :&: _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#99ebe9d9a74694e8687b6f8adc097de4">\sum_ ( _ <- _ | _ ) _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#267fe5cb19a4f9c37deb7c452a25ccb6">\sum_ ( _ | _ ) _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#46b28b862ebc4bda38b5188071e2f20c">_ + _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#839dc9de43c30e3fb6956e22c14c882a"><< _ >> (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#0cba8965977f5f50b779d6c4f6af1d2d">_ :=: _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#90d7b09f0c2effdccb449f69b6bb8499">_ < _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#650edb4f13965b5befa677e688f789d4">_ == _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#bc975efff53c5c935fca6f64bf4f7825">_ <= _ <= _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#92e34d658f9a1b6a4d0f8de14c29c81c">_ <= _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#36107ffb18a8bbc5966401cfe543371b">_ ^C (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#3cf4ddd1c78e2b0890c629753f41711f">\rank _ (nat_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#93ce48d079482e776b2a4aab92a63444">'M_ _ (type_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#88dd4b2c2e6318afa7008df815f99a1a">'M_ ( _ , _ ) (type_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#558e7d7f1cdeac24f358810e8b2a6c90">_ :\: _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#0144fb51819f0f8c24047b11c3b903bc">\bigcap_ ( _ | _ ) _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#9b2c1db5d2375a5b8d3548a4a995de32">_ :&: _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#2060ffb6da9b0d74639202e23e21e2ba">\sum_ ( _ <- _ | _ ) _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#e3eadb2258a983802424aabe03eb3fa5">\sum_ ( _ | _ ) _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#fc376d0ef5d57f2ced00029c73bfae3e">_ + _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#5678c2522c46860f8f34d965719dc347"><< _ >> (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#60865e2842769a434fa149a87581dd5d">_ :=: _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#cf4c296714679a4f3b1759a3b0e27ede">_ < _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#b38dda025cba8c04feef5c1eeec2b3bb">_ == _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#5b65eca33ef6c8565fff5760d6ca1f24">_ <= _ <= _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#7aa19237bd672944c59049593f9cf504">_ <= _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#2bba6607cd5441a3a280283039979ef6">_ ^C (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#c9e4b28fe217104569228ddbd881731d">\rank _ (nat_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#5f150f70ed272d7494c263afd1ab08fa">'M_ _ (type_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
+<a href="mathcomp.algebra.mxalgebra.html#86216ed4d3483e6fad890671e5a52e3b">'M_ ( _ , _ ) (type_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
<a href="mathcomp.algebra.mxalgebra.html#rowV0P">rowV0P</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
<a href="mathcomp.algebra.mxalgebra.html#rowV0Pn">rowV0Pn</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#row_full_dom_hom">row_full_dom_hom</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
@@ -1326,8 +1304,6 @@
<a href="mathcomp.algebra.matrix.html#row'_const">row'_const</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
<a href="mathcomp.algebra.matrix.html#row0">row0</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
<a href="mathcomp.algebra.matrix.html#row1">row1</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rpoly">rpoly</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rpoly_map_mul">rpoly_map_mul</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#rpred">rpred</a> [section, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#rpredMz">rpredMz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#rpredXsign">rpredXsign</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
@@ -1346,9 +1322,6 @@
<a href="mathcomp.algebra.poly.html#rreg_size">rreg_size</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.algebra.poly.html#rreg_lead0">rreg_lead0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
<a href="mathcomp.algebra.poly.html#rreg_lead">rreg_lead</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rscalpT">rscalpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rseq_poly_map">rseq_poly_map</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rseq_poly">rseq_poly</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.ssreflect.fintype.html#rshift">rshift</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
<a href="mathcomp.ssreflect.fintype.html#rshift_subproof">rshift_subproof</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
<a href="mathcomp.algebra.zmodp.html#rshift1">rshift1</a> [lemma, in <a href="mathcomp.algebra.zmodp.html">mathcomp.algebra.zmodp</a>]<br/>
@@ -1394,7 +1367,6 @@
<a href="mathcomp.character.mxabelem.html#rstab_abelem">rstab_abelem</a> [lemma, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/>
<a href="mathcomp.algebra.matrix.html#rsubmx">rsubmx</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
<a href="mathcomp.algebra.matrix.html#rsubmx_key">rsubmx_key</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.field.closed_field.html#rsumpT">rsumpT</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.fingroup.fingroup.html#rT">rT</a> [abbreviation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#rU">rU</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#rU'">rU'</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
@@ -1527,7 +1499,7 @@
<td><a href="index_global_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_global_*.html">other</a></td>
-<td>(23233 entries)</td>
+<td>(23836 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
@@ -1559,14 +1531,14 @@
<td><a href="index_notation_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_notation_*.html">other</a></td>
-<td>(1373 entries)</td>
+<td>(1409 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index_module_A.html">A</a></td>
<td><a href="index_module_B.html">B</a></td>
<td><a href="index_module_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_module_D.html">D</a></td>
<td><a href="index_module_E.html">E</a></td>
<td><a href="index_module_F.html">F</a></td>
<td><a href="index_module_G.html">G</a></td>
@@ -1591,7 +1563,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -1623,7 +1595,7 @@
<td><a href="index_variable_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3475 entries)</td>
+<td>(3574 entries)</td>
</tr>
<tr>
<td>Library Index</td>
@@ -1655,7 +1627,7 @@
<td><a href="index_library_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(89 entries)</td>
+<td>(90 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
@@ -1687,7 +1659,7 @@
<td><a href="index_lemma_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(11853 entries)</td>
+<td>(12096 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
@@ -1719,7 +1691,7 @@
<td><a href="index_constructor_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(359 entries)</td>
+<td>(368 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
@@ -1751,7 +1723,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -1783,14 +1755,14 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(103 entries)</td>
+<td>(107 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index_projection_A.html">A</a></td>
<td><a href="index_projection_B.html">B</a></td>
<td><a href="index_projection_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_projection_D.html">D</a></td>
<td><a href="index_projection_E.html">E</a></td>
<td><a href="index_projection_F.html">F</a></td>
<td><a href="index_projection_G.html">G</a></td>
@@ -1815,7 +1787,7 @@
<td><a href="index_projection_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(266 entries)</td>
+<td>(273 entries)</td>
</tr>
<tr>
<td>Section Index</td>
@@ -1847,7 +1819,7 @@
<td><a href="index_section_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(1118 entries)</td>
+<td>(1140 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
@@ -1879,7 +1851,7 @@
<td><a href="index_abbreviation_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(691 entries)</td>
+<td>(728 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
@@ -1911,14 +1883,14 @@
<td><a href="index_definition_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3461 entries)</td>
+<td>(3596 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index_record_A.html">A</a></td>
<td>B</td>
<td><a href="index_record_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_record_D.html">D</a></td>
<td><a href="index_record_E.html">E</a></td>
<td><a href="index_record_F.html">F</a></td>
<td><a href="index_record_G.html">G</a></td>
@@ -1943,7 +1915,7 @@
<td><a href="index_record_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(185 entries)</td>
+<td>(189 entries)</td>
</tr>
</table>
</div>
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-08 04:03:31 +0000