aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc/index_lemma_D.html
diff options
context:
space:
mode:
authorCyril Cohen2019-10-16 11:26:43 +0200
committerCyril Cohen2019-10-16 11:26:43 +0200
commit6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch)
tree1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/index_lemma_D.html
parentdd82aaeae7e9478efc178ce8430986649555b032 (diff)
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/index_lemma_D.html')
-rw-r--r--docs/htmldoc/index_lemma_D.html1413
1 files changed, 0 insertions, 1413 deletions
diff --git a/docs/htmldoc/index_lemma_D.html b/docs/htmldoc/index_lemma_D.html
deleted file mode 100644
index 811fcd8..0000000
--- a/docs/htmldoc/index_lemma_D.html
+++ /dev/null
@@ -1,1413 +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.test_suite.hierarchy_test</title>
-</head>
-
-<body>
-
-<div id="page">
-
-<div id="header">
-</div>
-
-<div id="main">
-
-<table>
-<tr>
-<td>Global Index</td>
-<td><a href="index_global_A.html">A</a></td>
-<td><a href="index_global_B.html">B</a></td>
-<td><a href="index_global_C.html">C</a></td>
-<td><a href="index_global_D.html">D</a></td>
-<td><a href="index_global_E.html">E</a></td>
-<td><a href="index_global_F.html">F</a></td>
-<td><a href="index_global_G.html">G</a></td>
-<td><a href="index_global_H.html">H</a></td>
-<td><a href="index_global_I.html">I</a></td>
-<td><a href="index_global_J.html">J</a></td>
-<td><a href="index_global_K.html">K</a></td>
-<td><a href="index_global_L.html">L</a></td>
-<td><a href="index_global_M.html">M</a></td>
-<td><a href="index_global_N.html">N</a></td>
-<td><a href="index_global_O.html">O</a></td>
-<td><a href="index_global_P.html">P</a></td>
-<td><a href="index_global_Q.html">Q</a></td>
-<td><a href="index_global_R.html">R</a></td>
-<td><a href="index_global_S.html">S</a></td>
-<td><a href="index_global_T.html">T</a></td>
-<td><a href="index_global_U.html">U</a></td>
-<td><a href="index_global_V.html">V</a></td>
-<td><a href="index_global_W.html">W</a></td>
-<td><a href="index_global_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_global_Z.html">Z</a></td>
-<td>_</td>
-<td><a href="index_global_*.html">other</a></td>
-<td>(23836 entries)</td>
-</tr>
-<tr>
-<td>Notation Index</td>
-<td><a href="index_notation_A.html">A</a></td>
-<td><a href="index_notation_B.html">B</a></td>
-<td><a href="index_notation_C.html">C</a></td>
-<td><a href="index_notation_D.html">D</a></td>
-<td><a href="index_notation_E.html">E</a></td>
-<td><a href="index_notation_F.html">F</a></td>
-<td><a href="index_notation_G.html">G</a></td>
-<td>H</td>
-<td><a href="index_notation_I.html">I</a></td>
-<td>J</td>
-<td><a href="index_notation_K.html">K</a></td>
-<td><a href="index_notation_L.html">L</a></td>
-<td><a href="index_notation_M.html">M</a></td>
-<td><a href="index_notation_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_notation_P.html">P</a></td>
-<td><a href="index_notation_Q.html">Q</a></td>
-<td><a href="index_notation_R.html">R</a></td>
-<td><a href="index_notation_S.html">S</a></td>
-<td>T</td>
-<td><a href="index_notation_U.html">U</a></td>
-<td><a href="index_notation_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_notation_Z.html">Z</a></td>
-<td>_</td>
-<td><a href="index_notation_*.html">other</a></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><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>
-<td>H</td>
-<td><a href="index_module_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td>L</td>
-<td><a href="index_module_M.html">M</a></td>
-<td><a href="index_module_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_module_P.html">P</a></td>
-<td><a href="index_module_Q.html">Q</a></td>
-<td><a href="index_module_R.html">R</a></td>
-<td><a href="index_module_S.html">S</a></td>
-<td>T</td>
-<td><a href="index_module_U.html">U</a></td>
-<td><a href="index_module_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td>Z</td>
-<td>_</td>
-<td>other</td>
-<td>(221 entries)</td>
-</tr>
-<tr>
-<td>Variable Index</td>
-<td><a href="index_variable_A.html">A</a></td>
-<td><a href="index_variable_B.html">B</a></td>
-<td><a href="index_variable_C.html">C</a></td>
-<td><a href="index_variable_D.html">D</a></td>
-<td><a href="index_variable_E.html">E</a></td>
-<td><a href="index_variable_F.html">F</a></td>
-<td><a href="index_variable_G.html">G</a></td>
-<td><a href="index_variable_H.html">H</a></td>
-<td><a href="index_variable_I.html">I</a></td>
-<td>J</td>
-<td><a href="index_variable_K.html">K</a></td>
-<td><a href="index_variable_L.html">L</a></td>
-<td><a href="index_variable_M.html">M</a></td>
-<td><a href="index_variable_N.html">N</a></td>
-<td><a href="index_variable_O.html">O</a></td>
-<td><a href="index_variable_P.html">P</a></td>
-<td><a href="index_variable_Q.html">Q</a></td>
-<td><a href="index_variable_R.html">R</a></td>
-<td><a href="index_variable_S.html">S</a></td>
-<td><a href="index_variable_T.html">T</a></td>
-<td><a href="index_variable_U.html">U</a></td>
-<td><a href="index_variable_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_variable_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(3574 entries)</td>
-</tr>
-<tr>
-<td>Library Index</td>
-<td><a href="index_library_A.html">A</a></td>
-<td><a href="index_library_B.html">B</a></td>
-<td><a href="index_library_C.html">C</a></td>
-<td><a href="index_library_D.html">D</a></td>
-<td><a href="index_library_E.html">E</a></td>
-<td><a href="index_library_F.html">F</a></td>
-<td><a href="index_library_G.html">G</a></td>
-<td><a href="index_library_H.html">H</a></td>
-<td><a href="index_library_I.html">I</a></td>
-<td><a href="index_library_J.html">J</a></td>
-<td>K</td>
-<td>L</td>
-<td><a href="index_library_M.html">M</a></td>
-<td><a href="index_library_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_library_P.html">P</a></td>
-<td><a href="index_library_Q.html">Q</a></td>
-<td><a href="index_library_R.html">R</a></td>
-<td><a href="index_library_S.html">S</a></td>
-<td><a href="index_library_T.html">T</a></td>
-<td>U</td>
-<td><a href="index_library_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_library_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(90 entries)</td>
-</tr>
-<tr>
-<td>Lemma Index</td>
-<td><a href="index_lemma_A.html">A</a></td>
-<td><a href="index_lemma_B.html">B</a></td>
-<td><a href="index_lemma_C.html">C</a></td>
-<td><a href="index_lemma_D.html">D</a></td>
-<td><a href="index_lemma_E.html">E</a></td>
-<td><a href="index_lemma_F.html">F</a></td>
-<td><a href="index_lemma_G.html">G</a></td>
-<td><a href="index_lemma_H.html">H</a></td>
-<td><a href="index_lemma_I.html">I</a></td>
-<td><a href="index_lemma_J.html">J</a></td>
-<td><a href="index_lemma_K.html">K</a></td>
-<td><a href="index_lemma_L.html">L</a></td>
-<td><a href="index_lemma_M.html">M</a></td>
-<td><a href="index_lemma_N.html">N</a></td>
-<td><a href="index_lemma_O.html">O</a></td>
-<td><a href="index_lemma_P.html">P</a></td>
-<td><a href="index_lemma_Q.html">Q</a></td>
-<td><a href="index_lemma_R.html">R</a></td>
-<td><a href="index_lemma_S.html">S</a></td>
-<td><a href="index_lemma_T.html">T</a></td>
-<td><a href="index_lemma_U.html">U</a></td>
-<td><a href="index_lemma_V.html">V</a></td>
-<td><a href="index_lemma_W.html">W</a></td>
-<td><a href="index_lemma_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_lemma_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(12096 entries)</td>
-</tr>
-<tr>
-<td>Constructor Index</td>
-<td><a href="index_constructor_A.html">A</a></td>
-<td><a href="index_constructor_B.html">B</a></td>
-<td><a href="index_constructor_C.html">C</a></td>
-<td><a href="index_constructor_D.html">D</a></td>
-<td><a href="index_constructor_E.html">E</a></td>
-<td><a href="index_constructor_F.html">F</a></td>
-<td><a href="index_constructor_G.html">G</a></td>
-<td><a href="index_constructor_H.html">H</a></td>
-<td><a href="index_constructor_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td><a href="index_constructor_L.html">L</a></td>
-<td><a href="index_constructor_M.html">M</a></td>
-<td><a href="index_constructor_N.html">N</a></td>
-<td><a href="index_constructor_O.html">O</a></td>
-<td><a href="index_constructor_P.html">P</a></td>
-<td><a href="index_constructor_Q.html">Q</a></td>
-<td><a href="index_constructor_R.html">R</a></td>
-<td><a href="index_constructor_S.html">S</a></td>
-<td><a href="index_constructor_T.html">T</a></td>
-<td><a href="index_constructor_U.html">U</a></td>
-<td><a href="index_constructor_V.html">V</a></td>
-<td>W</td>
-<td><a href="index_constructor_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_constructor_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(368 entries)</td>
-</tr>
-<tr>
-<td>Axiom Index</td>
-<td><a href="index_axiom_A.html">A</a></td>
-<td><a href="index_axiom_B.html">B</a></td>
-<td><a href="index_axiom_C.html">C</a></td>
-<td>D</td>
-<td><a href="index_axiom_E.html">E</a></td>
-<td><a href="index_axiom_F.html">F</a></td>
-<td>G</td>
-<td>H</td>
-<td><a href="index_axiom_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td>L</td>
-<td>M</td>
-<td>N</td>
-<td>O</td>
-<td><a href="index_axiom_P.html">P</a></td>
-<td>Q</td>
-<td><a href="index_axiom_R.html">R</a></td>
-<td><a href="index_axiom_S.html">S</a></td>
-<td>T</td>
-<td>U</td>
-<td>V</td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td>Z</td>
-<td>_</td>
-<td>other</td>
-<td>(45 entries)</td>
-</tr>
-<tr>
-<td>Inductive Index</td>
-<td><a href="index_inductive_A.html">A</a></td>
-<td><a href="index_inductive_B.html">B</a></td>
-<td><a href="index_inductive_C.html">C</a></td>
-<td><a href="index_inductive_D.html">D</a></td>
-<td><a href="index_inductive_E.html">E</a></td>
-<td><a href="index_inductive_F.html">F</a></td>
-<td><a href="index_inductive_G.html">G</a></td>
-<td><a href="index_inductive_H.html">H</a></td>
-<td><a href="index_inductive_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td><a href="index_inductive_L.html">L</a></td>
-<td><a href="index_inductive_M.html">M</a></td>
-<td><a href="index_inductive_N.html">N</a></td>
-<td><a href="index_inductive_O.html">O</a></td>
-<td><a href="index_inductive_P.html">P</a></td>
-<td>Q</td>
-<td><a href="index_inductive_R.html">R</a></td>
-<td><a href="index_inductive_S.html">S</a></td>
-<td><a href="index_inductive_T.html">T</a></td>
-<td><a href="index_inductive_U.html">U</a></td>
-<td><a href="index_inductive_V.html">V</a></td>
-<td>W</td>
-<td><a href="index_inductive_X.html">X</a></td>
-<td>Y</td>
-<td>Z</td>
-<td>_</td>
-<td>other</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><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>
-<td>H</td>
-<td><a href="index_projection_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td>L</td>
-<td><a href="index_projection_M.html">M</a></td>
-<td><a href="index_projection_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_projection_P.html">P</a></td>
-<td><a href="index_projection_Q.html">Q</a></td>
-<td><a href="index_projection_R.html">R</a></td>
-<td><a href="index_projection_S.html">S</a></td>
-<td><a href="index_projection_T.html">T</a></td>
-<td><a href="index_projection_U.html">U</a></td>
-<td><a href="index_projection_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_projection_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(273 entries)</td>
-</tr>
-<tr>
-<td>Section Index</td>
-<td><a href="index_section_A.html">A</a></td>
-<td><a href="index_section_B.html">B</a></td>
-<td><a href="index_section_C.html">C</a></td>
-<td><a href="index_section_D.html">D</a></td>
-<td><a href="index_section_E.html">E</a></td>
-<td><a href="index_section_F.html">F</a></td>
-<td><a href="index_section_G.html">G</a></td>
-<td><a href="index_section_H.html">H</a></td>
-<td><a href="index_section_I.html">I</a></td>
-<td>J</td>
-<td><a href="index_section_K.html">K</a></td>
-<td><a href="index_section_L.html">L</a></td>
-<td><a href="index_section_M.html">M</a></td>
-<td><a href="index_section_N.html">N</a></td>
-<td><a href="index_section_O.html">O</a></td>
-<td><a href="index_section_P.html">P</a></td>
-<td><a href="index_section_Q.html">Q</a></td>
-<td><a href="index_section_R.html">R</a></td>
-<td><a href="index_section_S.html">S</a></td>
-<td><a href="index_section_T.html">T</a></td>
-<td><a href="index_section_U.html">U</a></td>
-<td><a href="index_section_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_section_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(1140 entries)</td>
-</tr>
-<tr>
-<td>Abbreviation Index</td>
-<td><a href="index_abbreviation_A.html">A</a></td>
-<td><a href="index_abbreviation_B.html">B</a></td>
-<td><a href="index_abbreviation_C.html">C</a></td>
-<td><a href="index_abbreviation_D.html">D</a></td>
-<td><a href="index_abbreviation_E.html">E</a></td>
-<td><a href="index_abbreviation_F.html">F</a></td>
-<td><a href="index_abbreviation_G.html">G</a></td>
-<td><a href="index_abbreviation_H.html">H</a></td>
-<td><a href="index_abbreviation_I.html">I</a></td>
-<td><a href="index_abbreviation_J.html">J</a></td>
-<td><a href="index_abbreviation_K.html">K</a></td>
-<td><a href="index_abbreviation_L.html">L</a></td>
-<td><a href="index_abbreviation_M.html">M</a></td>
-<td><a href="index_abbreviation_N.html">N</a></td>
-<td><a href="index_abbreviation_O.html">O</a></td>
-<td><a href="index_abbreviation_P.html">P</a></td>
-<td><a href="index_abbreviation_Q.html">Q</a></td>
-<td><a href="index_abbreviation_R.html">R</a></td>
-<td><a href="index_abbreviation_S.html">S</a></td>
-<td><a href="index_abbreviation_T.html">T</a></td>
-<td><a href="index_abbreviation_U.html">U</a></td>
-<td><a href="index_abbreviation_V.html">V</a></td>
-<td><a href="index_abbreviation_W.html">W</a></td>
-<td><a href="index_abbreviation_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_abbreviation_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(728 entries)</td>
-</tr>
-<tr>
-<td>Definition Index</td>
-<td><a href="index_definition_A.html">A</a></td>
-<td><a href="index_definition_B.html">B</a></td>
-<td><a href="index_definition_C.html">C</a></td>
-<td><a href="index_definition_D.html">D</a></td>
-<td><a href="index_definition_E.html">E</a></td>
-<td><a href="index_definition_F.html">F</a></td>
-<td><a href="index_definition_G.html">G</a></td>
-<td><a href="index_definition_H.html">H</a></td>
-<td><a href="index_definition_I.html">I</a></td>
-<td><a href="index_definition_J.html">J</a></td>
-<td><a href="index_definition_K.html">K</a></td>
-<td><a href="index_definition_L.html">L</a></td>
-<td><a href="index_definition_M.html">M</a></td>
-<td><a href="index_definition_N.html">N</a></td>
-<td><a href="index_definition_O.html">O</a></td>
-<td><a href="index_definition_P.html">P</a></td>
-<td><a href="index_definition_Q.html">Q</a></td>
-<td><a href="index_definition_R.html">R</a></td>
-<td><a href="index_definition_S.html">S</a></td>
-<td><a href="index_definition_T.html">T</a></td>
-<td><a href="index_definition_U.html">U</a></td>
-<td><a href="index_definition_V.html">V</a></td>
-<td><a href="index_definition_W.html">W</a></td>
-<td><a href="index_definition_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_definition_Z.html">Z</a></td>
-<td>_</td>
-<td>other</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><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>
-<td>H</td>
-<td><a href="index_record_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td>L</td>
-<td><a href="index_record_M.html">M</a></td>
-<td><a href="index_record_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_record_P.html">P</a></td>
-<td><a href="index_record_Q.html">Q</a></td>
-<td><a href="index_record_R.html">R</a></td>
-<td><a href="index_record_S.html">S</a></td>
-<td><a href="index_record_T.html">T</a></td>
-<td><a href="index_record_U.html">U</a></td>
-<td><a href="index_record_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_record_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(189 entries)</td>
-</tr>
-</table>
-<hr/><a name="lemma_D"></a><h2>D (lemma)</h2>
-<a href="mathcomp.algebra.vector.html#daddv_pi_add">daddv_pi_add</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#daddv_pi_proj">daddv_pi_proj</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#daddv_pi_id">daddv_pi_id</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dchi_vchar">dchi_vchar</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dchi_ndirrE">dchi_ndirrE</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dchi1">dchi1</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#decrn_inj_in">decrn_inj_in</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#decrn_inj">decrn_inj</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#DecSocleType">DecSocleType</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#dec_mx_reducible_semisimple">dec_mx_reducible_semisimple</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#dec_mxsimple_exists">dec_mxsimple_exists</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dec_Qint_span">dec_Qint_span</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.field.algnum.html#dec_Cint_span">dec_Cint_span</a> [in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/>
-<a href="mathcomp.algebra.poly.html#dec_factor_theorem">dec_factor_theorem</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#def_pnElem">def_pnElem</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.ssreflect.finset.html#def_pblock">def_pblock</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#degree_irr1">degree_irr1</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.algebra.mxpoly.html#degree_mxminpoly_map">degree_mxminpoly_map</a> [in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/>
-<a href="mathcomp.algebra.mxpoly.html#degree_mxminpoly_proof">degree_mxminpoly_proof</a> [in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#delta_mx_dshift">delta_mx_dshift</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#delta_mx_ushift">delta_mx_ushift</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#delta_mx_rshift">delta_mx_rshift</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#delta_mx_lshift">delta_mx_lshift</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#delta_mx_key">delta_mx_key</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.fraction.html#denom_Ratio">denom_Ratio</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
-<a href="mathcomp.algebra.fraction.html#denom_ratioP">denom_ratioP</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denqN">denqN</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denqP">denqP</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denqVz">denqVz</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denq_norm">denq_norm</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denq_mulr_sign">denq_mulr_sign</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denq_int">denq_int</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denq_eq0">denq_eq0</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denq_neq0">denq_neq0</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denq_lt0">denq_lt0</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#denq_gt0">denq_gt0</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#dergS">dergS</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#dergSn">dergSn</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#derg0">derg0</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#derg1">derg1</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#derG1P">derG1P</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.field.separable.html#DerivationS">DerivationS</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#Derivation_separableP">Derivation_separableP</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#Derivation_separable">Derivation_separable</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#Derivation_horner">Derivation_horner</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#Derivation_exp">Derivation_exp</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#Derivation_scalar">Derivation_scalar</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#Derivation_mul_poly">Derivation_mul_poly</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#Derivation_mul">Derivation_mul</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#Derivation1">Derivation1</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivB">derivB</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivC">derivC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivD">derivD</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#derivedP">derivedP</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivM">derivM</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivMn">derivMn</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivMNn">derivMNn</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivMXaddC">derivMXaddC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#derivMz">derivMz</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivN">derivN</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnC">derivnC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnD">derivnD</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnMn">derivnMn</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnMNn">derivnMNn</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnMXaddC">derivnMXaddC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnN">derivnN</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnS">derivnS</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnXn">derivnXn</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivnZ">derivnZ</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivn_map">derivn_map</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivn_poly0">derivn_poly0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivn_sub">derivn_sub</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivn_is_linear">derivn_is_linear</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivn0">derivn0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivn1">derivn1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivSn">derivSn</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivX">derivX</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivXn">derivXn</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivXsubC">derivXsubC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#derivZ">derivZ</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#deriv_exp">deriv_exp</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#deriv_comp">deriv_comp</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#deriv_map">deriv_map</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#deriv_mulC">deriv_mulC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#deriv_is_linear">deriv_is_linear</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#deriv0">deriv0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#derJ">derJ</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#der_bigdprod">der_bigdprod</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#der_bigcprod">der_bigcprod</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#der_dprod">der_dprod</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#der_cprod">der_cprod</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_cont">der_cont</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_normalS">der_normalS</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_subS">der_subS</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_normal">der_normal</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_norm">der_norm</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_sub">der_sub</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_char">der_char</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_abelian">der_abelian</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der_group_set">der_group_set</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#der1_sub_rker">der1_sub_rker</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.solvable.maximal.html#der1_stab_Ohm1_SCN_series">der1_stab_Ohm1_SCN_series</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der1_joing_cycles">der1_joing_cycles</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.solvable.commutator.html#der1_min">der1_min</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#der1_subG">der1_subG</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#determinant_alternate">determinant_alternate</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#determinant_multilinear">determinant_multilinear</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#detM">detM</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.character.character.html#detRepr_lin_char">detRepr_lin_char</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#detV">detV</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#detZ">detZ</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_inv">det_inv</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_lblock">det_lblock</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_ublock">det_ublock</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_diag">det_diag</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_mulmx">det_mulmx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_scalar1">det_scalar1</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_scalar">det_scalar</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_mx00">det_mx00</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_perm">det_perm</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_tr">det_tr</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det_map_mx">det_map_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.character.character.html#det_is_repr">det_is_repr</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det0">det0</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det0P">det0P</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#det1">det1</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.ssreflect.fingraph.html#dfsP">dfsP</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
-<a href="mathcomp.ssreflect.fingraph.html#dfs_pathP">dfs_pathP</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#diag_mx_comm">diag_mx_comm</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#diag_mxC">diag_mxC</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#diag_const_mx">diag_const_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#diag_mx_sum_delta">diag_mx_sum_delta</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#diag_mx_is_linear">diag_mx_is_linear</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#diag_mx_key">diag_mx_key</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#diffmxE">diffmxE</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#diffmxSl">diffmxSl</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#diffmx_key">diffmx_key</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.vector.html#diffvSl">diffvSl</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#diffv_eq0">diffv_eq0</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.solvable.burnside_app.html#diff_id_sh">diff_id_sh</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/>
-<a href="mathcomp.solvable.extremal.html#dihedral_classP">dihedral_classP</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/>
-<a href="mathcomp.solvable.extremal.html#dihedral2_structure">dihedral2_structure</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimvf">dimvf</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimvS">dimvS</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_sum_leqif">dimv_sum_leqif</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_leq_sum">dimv_leq_sum</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_add_leqif">dimv_add_leqif</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_disjoint_sum">dimv_disjoint_sum</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_sum_cap">dimv_sum_cap</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_cap_compl">dimv_cap_compl</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_compl">dimv_compl</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_leqif_eq">dimv_leqif_eq</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_leqif_sup">dimv_leqif_sup</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv_eq0">dimv_eq0</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dimv0">dimv0</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.field.falgebra.html#dimv1">dimv1</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.galois.html#dim_fixed_galois">dim_fixed_galois</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
-<a href="mathcomp.field.galois.html#dim_fixedField">dim_fixedField</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
-<a href="mathcomp.field.fieldext.html#dim_refBaseField">dim_refBaseField</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#dim_baseVspace">dim_baseVspace</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#dim_aspaceOver">dim_aspaceOver</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#dim_vspaceOver">dim_vspaceOver</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#dim_Fadjoin">dim_Fadjoin</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#dim_sup_field">dim_sup_field</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#dim_field_module">dim_field_module</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#dim_cosetv">dim_cosetv</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dim_span">dim_span</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#dim_vline">dim_vline</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.character.classfun.html#dim_cfun_on_abelian">dim_cfun_on_abelian</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.character.classfun.html#dim_cfun_on">dim_cfun_on</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.character.classfun.html#dim_cfun">dim_cfun</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.character.mxabelem.html#dim_abelemE">dim_abelemE</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/>
-<a href="mathcomp.field.falgebra.html#dim_cosetv_unit">dim_cosetv_unit</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#dim_algid">dim_algid</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#dim_prodv">dim_prodv</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#dinjectiveP">dinjectiveP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#dinjectivePn">dinjectivePn</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directvE">directvE</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directvEgeq">directvEgeq</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directvP">directvP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directv_sum_unique">directv_sum_unique</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directv_sum_independent">directv_sum_independent</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directv_sumE">directv_sumE</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directv_sumP">directv_sumP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directv_add_unique">directv_add_unique</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directv_addP">directv_addP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directv_addE">directv_addE</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#directv_trivial">directv_trivial</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirrE">dirrE</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dIrrP">dIrrP</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirrP">dirrP</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_small_norm">dirr_small_norm</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_constt_oppl">dirr_constt_oppl</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_constt_oppI">dirr_constt_oppI</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_constt_oppr">dirr_constt_oppr</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_consttE">dirr_consttE</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_dIirrE">dirr_dIirrE</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_dIirrPE">dirr_dIirrPE</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_inj">dirr_inj</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_dchi">dirr_dchi</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_aut">dirr_aut</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_norm1">dirr_norm1</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_sign">dirr_sign</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_opp">dirr_opp</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_oppr_closed">dirr_oppr_closed</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.character.vcharacter.html#dirr_key">dirr_key</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/>
-<a href="mathcomp.solvable.burnside_app.html#dir_s0p">dir_s0p</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/>
-<a href="mathcomp.solvable.burnside_app.html#dir_iso_iso3">dir_iso_iso3</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/>
-<a href="mathcomp.ssreflect.finset.html#disjoints_subset">disjoints_subset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjointU">disjointU</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjointU1">disjointU1</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjoint_cat">disjoint_cat</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjoint_has">disjoint_has</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjoint_cons">disjoint_cons</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjoint_trans">disjoint_trans</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjoint_subset">disjoint_subset</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjoint_sym">disjoint_sym</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.finset.html#disjoint_setI0">disjoint_setI0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjoint0">disjoint0</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#disjoint1">disjoint1</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#divgI">divgI</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#divgrM">divgrM</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#divgrMid">divgrMid</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#divgrMl">divgrMl</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#divgr_id">divgr_id</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#divgr_eq">divgr_eq</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#divgS">divgS</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.quotient.html#divg_normal">divg_normal</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#divg_indexS">divg_indexS</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#divg_index">divg_index</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#divisors_id">divisors_id</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#divisors_uniq">divisors_uniq</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#divisors_correct">divisors_correct</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#divisor1">divisor1</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnA">divnA</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnAC">divnAC</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnDl">divnDl</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnDr">divnDr</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnK">divnK</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnMA">divnMA</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnMDl">divnMDl</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnMl">divnMl</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnMr">divnMr</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divnn">divnn</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divNz_nat">divNz_nat</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#divn_count_dvd">divn_count_dvd</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divn_mulAC">divn_mulAC</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divn_gt0">divn_gt0</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divn_small">divn_small</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divn_eq">divn_eq</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divn0">divn0</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divn1">divn1</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#divn2">divn2</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.field.fieldext.html#divp_polyOver">divp_polyOver</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.algebra.rat.html#divqP">divqP</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#divq_eq">divq_eq</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#divq_num_den">divq_num_den</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzA">divzA</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzAC">divzAC</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzDl">divzDl</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzDr">divzDr</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzK">divzK</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzMA">divzMA</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzMA_ge0">divzMA_ge0</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzMDl">divzMDl</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzMl">divzMl</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzMpl">divzMpl</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzMpr">divzMpr</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzMr">divzMr</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzN">divzN</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divzz">divzz</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divz_mulAC">divz_mulAC</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divz_ge0">divz_ge0</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divz_small">divz_small</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divz_eq">divz_eq</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divz_abs">divz_abs</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divz_nat">divz_nat</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divz0">divz0</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#divz1">divz1</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.polyXY.html#div_annihilantP">div_annihilantP</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/>
-<a href="mathcomp.algebra.polyXY.html#div_annihilant_neq0">div_annihilant_neq0</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/>
-<a href="mathcomp.algebra.polyXY.html#div_annihilant_in_ideal">div_annihilant_in_ideal</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/>
-<a href="mathcomp.solvable.cyclic.html#div_ring_mul_group_cyclic">div_ring_mul_group_cyclic</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#div0n">div0n</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#div0z">div0z</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.solvable.extraspecial.html#DnQ_extraspecial">DnQ_extraspecial</a> [in <a href="mathcomp.solvable.extraspecial.html">mathcomp.solvable.extraspecial</a>]<br/>
-<a href="mathcomp.solvable.extraspecial.html#DnQ_pgroup">DnQ_pgroup</a> [in <a href="mathcomp.solvable.extraspecial.html">mathcomp.solvable.extraspecial</a>]<br/>
-<a href="mathcomp.solvable.extraspecial.html#DnQ_P">DnQ_P</a> [in <a href="mathcomp.solvable.extraspecial.html">mathcomp.solvable.extraspecial</a>]<br/>
-<a href="mathcomp.fingroup.morphism.html#domP">domP</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#dom_hom_mx_module">dom_hom_mx_module</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#dom_hom_invmx">dom_hom_invmx</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.fingroup.action.html#dom_qactJ">dom_qactJ</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
-<a href="mathcomp.fingroup.morphism.html#dom_ker">dom_ker</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#doubleB">doubleB</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#doubleD">doubleD</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#doubleE">doubleE</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#doubleK">doubleK</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#doubleMl">doubleMl</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#doubleMr">doubleMr</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#doubleS">doubleS</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#double_eq0">double_eq0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#double_gt0">double_gt0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#double0">double0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodA">dprodA</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodC">dprodC</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodE">dprodE</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodEcp">dprodEcp</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodEsd">dprodEsd</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodEY">dprodEY</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodg1">dprodg1</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodJ">dprodJ</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.character.character.html#dprodl_Iirr0">dprodl_Iirr0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprodl_Iirr_eq0">dprodl_Iirr_eq0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprodl_IirrK">dprodl_IirrK</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprodl_IirrE">dprodl_IirrE</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodmE">dprodmE</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodmEl">dprodmEl</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodmEr">dprodmEr</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodm_eqf">dprodm_eqf</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodm_cprod">dprodm_cprod</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodP">dprodP</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.character.character.html#dprodr_Iirr0">dprodr_Iirr0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprodr_Iirr_eq0">dprodr_Iirr_eq0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprodr_IirrK">dprodr_IirrK</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprodr_IirrE">dprodr_IirrE</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodW">dprodW</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodWC">dprodWC</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodWcp">dprodWcp</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodWsd">dprodWsd</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodWsdC">dprodWsdC</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodWY">dprodWY</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprodYP">dprodYP</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprod_card">dprod_card</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprod_modr">dprod_modr</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprod_modl">dprod_modl</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprod_normal2">dprod_normal2</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_IirrC">dprod_IirrC</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_IirrK">dprod_IirrK</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_Iirr_onto">dprod_Iirr_onto</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_Iirr_eq0">dprod_Iirr_eq0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_Iirr0r">dprod_Iirr0r</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_Iirr0l">dprod_Iirr0l</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_Iirr0">dprod_Iirr0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_Iirr_inj">dprod_Iirr_inj</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_IirrEr">dprod_IirrEr</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_IirrEl">dprod_IirrEl</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#dprod_IirrE">dprod_IirrE</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#dprod_homocyclic">dprod_homocyclic</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#dprod_abelem">dprod_abelem</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#dprod_exponent">dprod_exponent</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.character.mxabelem.html#dprod_rowg">dprod_rowg</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#dprod_nil">dprod_nil</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.fingroup.gproduct.html#dprod1g">dprod1g</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
-<a href="mathcomp.ssreflect.tuple.html#drop_tupleP">drop_tupleP</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_subseq">drop_subseq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_rev">drop_rev</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_nth">drop_nth</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_rcons">drop_rcons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_drop">drop_drop</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_size_cat">drop_size_cat</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_cat">drop_cat</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_cons">drop_cons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_size">drop_size</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_oversize">drop_oversize</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop_behead">drop_behead</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop0">drop0</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#drop1">drop1</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#dsubmx_key">dsubmx_key</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.character.character.html#dsumx_mul">dsumx_mul</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.solvable.primitive_action.html#dtuple_on_subset">dtuple_on_subset</a> [in <a href="mathcomp.solvable.primitive_action.html">mathcomp.solvable.primitive_action</a>]<br/>
-<a href="mathcomp.solvable.primitive_action.html#dtuple_on_add_D1">dtuple_on_add_D1</a> [in <a href="mathcomp.solvable.primitive_action.html">mathcomp.solvable.primitive_action</a>]<br/>
-<a href="mathcomp.solvable.primitive_action.html#dtuple_on_add">dtuple_on_add</a> [in <a href="mathcomp.solvable.primitive_action.html">mathcomp.solvable.primitive_action</a>]<br/>
-<a href="mathcomp.solvable.primitive_action.html#dtuple_onP">dtuple_onP</a> [in <a href="mathcomp.solvable.primitive_action.html">mathcomp.solvable.primitive_action</a>]<br/>
-<a href="mathcomp.field.algnum.html#dvdA_zmod_closed">dvdA_zmod_closed</a> [in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/>
-<a href="mathcomp.field.algnum.html#dvdA_key">dvdA_key</a> [in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdCP">dvdCP</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdCP_nat">dvdCP_nat</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_int">dvdC_int</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_nat">dvdC_nat</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_zmod">dvdC_zmod</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_key">dvdC_key</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_refl">dvdC_refl</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_trans">dvdC_trans</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_mul2l">dvdC_mul2l</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_mul2r">dvdC_mul2r</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_mulr">dvdC_mulr</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC_mull">dvdC_mull</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.field.algC.html#dvdC0">dvdC0</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdnn">dvdnn</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdnP">dvdnP</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.fingroup.quotient.html#dvdn_quotient">dvdn_quotient</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/>
-<a href="mathcomp.fingroup.quotient.html#dvdn_morphim">dvdn_morphim</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/>
-<a href="mathcomp.ssreflect.binomial.html#dvdn_pred_predX">dvdn_pred_predX</a> [in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#dvdn_partP">dvdn_partP</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#dvdn_sum">dvdn_sum</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#dvdn_divisors">dvdn_divisors</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#dvdn_part">dvdn_part</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#dvdn_pfactor">dvdn_pfactor</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#dvdn_leq_log">dvdn_leq_log</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#dvdn_prime2">dvdn_prime2</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_pexp2r">dvdn_pexp2r</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_double_ltn">dvdn_double_ltn</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_double_leq">dvdn_double_leq</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_lcm">dvdn_lcm</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_lcmr">dvdn_lcmr</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_lcml">dvdn_lcml</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_gcd">dvdn_gcd</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_gcdl">dvdn_gcdl</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_gcdr">dvdn_gcdr</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_fact">dvdn_fact</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_exp">dvdn_exp</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_sub">dvdn_sub</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_subl">dvdn_subl</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_subr">dvdn_subr</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_add_eq">dvdn_add_eq</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_add">dvdn_add</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_addl">dvdn_addl</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_addr">dvdn_addr</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_exp2r">dvdn_exp2r</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_Pexp2l">dvdn_Pexp2l</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_exp2l">dvdn_exp2l</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_div">dvdn_div</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_divRL">dvdn_divRL</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_divLR">dvdn_divLR</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_pmul2r">dvdn_pmul2r</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_pmul2l">dvdn_pmul2l</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_leq">dvdn_leq</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_odd">dvdn_odd</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_eq">dvdn_eq</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_trans">dvdn_trans</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_mul">dvdn_mul</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_mulr">dvdn_mulr</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_mull">dvdn_mull</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn_gt0">dvdn_gt0</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.field.algnum.html#dvdn_orderC">dvdn_orderC</a> [in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/>
-<a href="mathcomp.character.inertia.html#dvdn_constt_Res1_irr1">dvdn_constt_Res1_irr1</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#dvdn_exponent">dvdn_exponent</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.fingroup.action.html#dvdn_orbit">dvdn_orbit</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
-<a href="mathcomp.character.classfun.html#dvdn_cforder">dvdn_cforder</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.character.classfun.html#dvdn_cforderP">dvdn_cforderP</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.algebra.poly.html#dvdn_prim_root">dvdn_prim_root</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.ssreflect.bigop.html#dvdn_biggcdP">dvdn_biggcdP</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/>
-<a href="mathcomp.ssreflect.bigop.html#dvdn_biglcmP">dvdn_biglcmP</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#dvdn_cardMg">dvdn_cardMg</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#dvdn_indexg">dvdn_indexg</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.solvable.cyclic.html#dvdn_prime_cyclic">dvdn_prime_cyclic</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn0">dvdn0</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn1">dvdn1</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvdn2">dvdn2</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdpP_rat_int">dvdpP_rat_int</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdpP_int">dvdpP_int</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.field.separable.html#dvdp_separable">dvdp_separable</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdp_rat_int">dvdp_rat_int</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdzE">dvdzE</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdzP">dvdzP</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdzz">dvdzz</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_contents">dvdz_contents</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_pexp2r">dvdz_pexp2r</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_gcd">dvdz_gcd</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_gcdl">dvdz_gcdl</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_gcdr">dvdz_gcdr</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_exp">dvdz_exp</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_zmod_closed">dvdz_zmod_closed</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_exp2r">dvdz_exp2r</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_Pexp2l">dvdz_Pexp2l</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_exp2l">dvdz_exp2l</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_mul2r">dvdz_mul2r</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_mul2l">dvdz_mul2l</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_eq">dvdz_eq</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_mod0P">dvdz_mod0P</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_trans">dvdz_trans</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_mul">dvdz_mul</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_mulr">dvdz_mulr</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_mull">dvdz_mull</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz_key">dvdz_key</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz0">dvdz0</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvdz1">dvdz1</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.character.integral_char.html#dvd_irr1_index_center">dvd_irr1_index_center</a> [in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
-<a href="mathcomp.character.integral_char.html#dvd_irr1_cardG">dvd_irr1_cardG</a> [in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
-<a href="mathcomp.field.algC.html#dvd0C">dvd0C</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvd0n">dvd0n</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvd0z">dvd0z</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#dvd1n">dvd1n</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#dvd1z">dvd1z</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<br/><br/><hr/><table>
-<tr>
-<td>Global Index</td>
-<td><a href="index_global_A.html">A</a></td>
-<td><a href="index_global_B.html">B</a></td>
-<td><a href="index_global_C.html">C</a></td>
-<td><a href="index_global_D.html">D</a></td>
-<td><a href="index_global_E.html">E</a></td>
-<td><a href="index_global_F.html">F</a></td>
-<td><a href="index_global_G.html">G</a></td>
-<td><a href="index_global_H.html">H</a></td>
-<td><a href="index_global_I.html">I</a></td>
-<td><a href="index_global_J.html">J</a></td>
-<td><a href="index_global_K.html">K</a></td>
-<td><a href="index_global_L.html">L</a></td>
-<td><a href="index_global_M.html">M</a></td>
-<td><a href="index_global_N.html">N</a></td>
-<td><a href="index_global_O.html">O</a></td>
-<td><a href="index_global_P.html">P</a></td>
-<td><a href="index_global_Q.html">Q</a></td>
-<td><a href="index_global_R.html">R</a></td>
-<td><a href="index_global_S.html">S</a></td>
-<td><a href="index_global_T.html">T</a></td>
-<td><a href="index_global_U.html">U</a></td>
-<td><a href="index_global_V.html">V</a></td>
-<td><a href="index_global_W.html">W</a></td>
-<td><a href="index_global_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_global_Z.html">Z</a></td>
-<td>_</td>
-<td><a href="index_global_*.html">other</a></td>
-<td>(23836 entries)</td>
-</tr>
-<tr>
-<td>Notation Index</td>
-<td><a href="index_notation_A.html">A</a></td>
-<td><a href="index_notation_B.html">B</a></td>
-<td><a href="index_notation_C.html">C</a></td>
-<td><a href="index_notation_D.html">D</a></td>
-<td><a href="index_notation_E.html">E</a></td>
-<td><a href="index_notation_F.html">F</a></td>
-<td><a href="index_notation_G.html">G</a></td>
-<td>H</td>
-<td><a href="index_notation_I.html">I</a></td>
-<td>J</td>
-<td><a href="index_notation_K.html">K</a></td>
-<td><a href="index_notation_L.html">L</a></td>
-<td><a href="index_notation_M.html">M</a></td>
-<td><a href="index_notation_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_notation_P.html">P</a></td>
-<td><a href="index_notation_Q.html">Q</a></td>
-<td><a href="index_notation_R.html">R</a></td>
-<td><a href="index_notation_S.html">S</a></td>
-<td>T</td>
-<td><a href="index_notation_U.html">U</a></td>
-<td><a href="index_notation_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_notation_Z.html">Z</a></td>
-<td>_</td>
-<td><a href="index_notation_*.html">other</a></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><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>
-<td>H</td>
-<td><a href="index_module_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td>L</td>
-<td><a href="index_module_M.html">M</a></td>
-<td><a href="index_module_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_module_P.html">P</a></td>
-<td><a href="index_module_Q.html">Q</a></td>
-<td><a href="index_module_R.html">R</a></td>
-<td><a href="index_module_S.html">S</a></td>
-<td>T</td>
-<td><a href="index_module_U.html">U</a></td>
-<td><a href="index_module_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td>Z</td>
-<td>_</td>
-<td>other</td>
-<td>(221 entries)</td>
-</tr>
-<tr>
-<td>Variable Index</td>
-<td><a href="index_variable_A.html">A</a></td>
-<td><a href="index_variable_B.html">B</a></td>
-<td><a href="index_variable_C.html">C</a></td>
-<td><a href="index_variable_D.html">D</a></td>
-<td><a href="index_variable_E.html">E</a></td>
-<td><a href="index_variable_F.html">F</a></td>
-<td><a href="index_variable_G.html">G</a></td>
-<td><a href="index_variable_H.html">H</a></td>
-<td><a href="index_variable_I.html">I</a></td>
-<td>J</td>
-<td><a href="index_variable_K.html">K</a></td>
-<td><a href="index_variable_L.html">L</a></td>
-<td><a href="index_variable_M.html">M</a></td>
-<td><a href="index_variable_N.html">N</a></td>
-<td><a href="index_variable_O.html">O</a></td>
-<td><a href="index_variable_P.html">P</a></td>
-<td><a href="index_variable_Q.html">Q</a></td>
-<td><a href="index_variable_R.html">R</a></td>
-<td><a href="index_variable_S.html">S</a></td>
-<td><a href="index_variable_T.html">T</a></td>
-<td><a href="index_variable_U.html">U</a></td>
-<td><a href="index_variable_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_variable_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(3574 entries)</td>
-</tr>
-<tr>
-<td>Library Index</td>
-<td><a href="index_library_A.html">A</a></td>
-<td><a href="index_library_B.html">B</a></td>
-<td><a href="index_library_C.html">C</a></td>
-<td><a href="index_library_D.html">D</a></td>
-<td><a href="index_library_E.html">E</a></td>
-<td><a href="index_library_F.html">F</a></td>
-<td><a href="index_library_G.html">G</a></td>
-<td><a href="index_library_H.html">H</a></td>
-<td><a href="index_library_I.html">I</a></td>
-<td><a href="index_library_J.html">J</a></td>
-<td>K</td>
-<td>L</td>
-<td><a href="index_library_M.html">M</a></td>
-<td><a href="index_library_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_library_P.html">P</a></td>
-<td><a href="index_library_Q.html">Q</a></td>
-<td><a href="index_library_R.html">R</a></td>
-<td><a href="index_library_S.html">S</a></td>
-<td><a href="index_library_T.html">T</a></td>
-<td>U</td>
-<td><a href="index_library_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_library_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(90 entries)</td>
-</tr>
-<tr>
-<td>Lemma Index</td>
-<td><a href="index_lemma_A.html">A</a></td>
-<td><a href="index_lemma_B.html">B</a></td>
-<td><a href="index_lemma_C.html">C</a></td>
-<td><a href="index_lemma_D.html">D</a></td>
-<td><a href="index_lemma_E.html">E</a></td>
-<td><a href="index_lemma_F.html">F</a></td>
-<td><a href="index_lemma_G.html">G</a></td>
-<td><a href="index_lemma_H.html">H</a></td>
-<td><a href="index_lemma_I.html">I</a></td>
-<td><a href="index_lemma_J.html">J</a></td>
-<td><a href="index_lemma_K.html">K</a></td>
-<td><a href="index_lemma_L.html">L</a></td>
-<td><a href="index_lemma_M.html">M</a></td>
-<td><a href="index_lemma_N.html">N</a></td>
-<td><a href="index_lemma_O.html">O</a></td>
-<td><a href="index_lemma_P.html">P</a></td>
-<td><a href="index_lemma_Q.html">Q</a></td>
-<td><a href="index_lemma_R.html">R</a></td>
-<td><a href="index_lemma_S.html">S</a></td>
-<td><a href="index_lemma_T.html">T</a></td>
-<td><a href="index_lemma_U.html">U</a></td>
-<td><a href="index_lemma_V.html">V</a></td>
-<td><a href="index_lemma_W.html">W</a></td>
-<td><a href="index_lemma_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_lemma_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(12096 entries)</td>
-</tr>
-<tr>
-<td>Constructor Index</td>
-<td><a href="index_constructor_A.html">A</a></td>
-<td><a href="index_constructor_B.html">B</a></td>
-<td><a href="index_constructor_C.html">C</a></td>
-<td><a href="index_constructor_D.html">D</a></td>
-<td><a href="index_constructor_E.html">E</a></td>
-<td><a href="index_constructor_F.html">F</a></td>
-<td><a href="index_constructor_G.html">G</a></td>
-<td><a href="index_constructor_H.html">H</a></td>
-<td><a href="index_constructor_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td><a href="index_constructor_L.html">L</a></td>
-<td><a href="index_constructor_M.html">M</a></td>
-<td><a href="index_constructor_N.html">N</a></td>
-<td><a href="index_constructor_O.html">O</a></td>
-<td><a href="index_constructor_P.html">P</a></td>
-<td><a href="index_constructor_Q.html">Q</a></td>
-<td><a href="index_constructor_R.html">R</a></td>
-<td><a href="index_constructor_S.html">S</a></td>
-<td><a href="index_constructor_T.html">T</a></td>
-<td><a href="index_constructor_U.html">U</a></td>
-<td><a href="index_constructor_V.html">V</a></td>
-<td>W</td>
-<td><a href="index_constructor_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_constructor_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(368 entries)</td>
-</tr>
-<tr>
-<td>Axiom Index</td>
-<td><a href="index_axiom_A.html">A</a></td>
-<td><a href="index_axiom_B.html">B</a></td>
-<td><a href="index_axiom_C.html">C</a></td>
-<td>D</td>
-<td><a href="index_axiom_E.html">E</a></td>
-<td><a href="index_axiom_F.html">F</a></td>
-<td>G</td>
-<td>H</td>
-<td><a href="index_axiom_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td>L</td>
-<td>M</td>
-<td>N</td>
-<td>O</td>
-<td><a href="index_axiom_P.html">P</a></td>
-<td>Q</td>
-<td><a href="index_axiom_R.html">R</a></td>
-<td><a href="index_axiom_S.html">S</a></td>
-<td>T</td>
-<td>U</td>
-<td>V</td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td>Z</td>
-<td>_</td>
-<td>other</td>
-<td>(45 entries)</td>
-</tr>
-<tr>
-<td>Inductive Index</td>
-<td><a href="index_inductive_A.html">A</a></td>
-<td><a href="index_inductive_B.html">B</a></td>
-<td><a href="index_inductive_C.html">C</a></td>
-<td><a href="index_inductive_D.html">D</a></td>
-<td><a href="index_inductive_E.html">E</a></td>
-<td><a href="index_inductive_F.html">F</a></td>
-<td><a href="index_inductive_G.html">G</a></td>
-<td><a href="index_inductive_H.html">H</a></td>
-<td><a href="index_inductive_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td><a href="index_inductive_L.html">L</a></td>
-<td><a href="index_inductive_M.html">M</a></td>
-<td><a href="index_inductive_N.html">N</a></td>
-<td><a href="index_inductive_O.html">O</a></td>
-<td><a href="index_inductive_P.html">P</a></td>
-<td>Q</td>
-<td><a href="index_inductive_R.html">R</a></td>
-<td><a href="index_inductive_S.html">S</a></td>
-<td><a href="index_inductive_T.html">T</a></td>
-<td><a href="index_inductive_U.html">U</a></td>
-<td><a href="index_inductive_V.html">V</a></td>
-<td>W</td>
-<td><a href="index_inductive_X.html">X</a></td>
-<td>Y</td>
-<td>Z</td>
-<td>_</td>
-<td>other</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><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>
-<td>H</td>
-<td><a href="index_projection_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td>L</td>
-<td><a href="index_projection_M.html">M</a></td>
-<td><a href="index_projection_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_projection_P.html">P</a></td>
-<td><a href="index_projection_Q.html">Q</a></td>
-<td><a href="index_projection_R.html">R</a></td>
-<td><a href="index_projection_S.html">S</a></td>
-<td><a href="index_projection_T.html">T</a></td>
-<td><a href="index_projection_U.html">U</a></td>
-<td><a href="index_projection_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_projection_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(273 entries)</td>
-</tr>
-<tr>
-<td>Section Index</td>
-<td><a href="index_section_A.html">A</a></td>
-<td><a href="index_section_B.html">B</a></td>
-<td><a href="index_section_C.html">C</a></td>
-<td><a href="index_section_D.html">D</a></td>
-<td><a href="index_section_E.html">E</a></td>
-<td><a href="index_section_F.html">F</a></td>
-<td><a href="index_section_G.html">G</a></td>
-<td><a href="index_section_H.html">H</a></td>
-<td><a href="index_section_I.html">I</a></td>
-<td>J</td>
-<td><a href="index_section_K.html">K</a></td>
-<td><a href="index_section_L.html">L</a></td>
-<td><a href="index_section_M.html">M</a></td>
-<td><a href="index_section_N.html">N</a></td>
-<td><a href="index_section_O.html">O</a></td>
-<td><a href="index_section_P.html">P</a></td>
-<td><a href="index_section_Q.html">Q</a></td>
-<td><a href="index_section_R.html">R</a></td>
-<td><a href="index_section_S.html">S</a></td>
-<td><a href="index_section_T.html">T</a></td>
-<td><a href="index_section_U.html">U</a></td>
-<td><a href="index_section_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_section_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(1140 entries)</td>
-</tr>
-<tr>
-<td>Abbreviation Index</td>
-<td><a href="index_abbreviation_A.html">A</a></td>
-<td><a href="index_abbreviation_B.html">B</a></td>
-<td><a href="index_abbreviation_C.html">C</a></td>
-<td><a href="index_abbreviation_D.html">D</a></td>
-<td><a href="index_abbreviation_E.html">E</a></td>
-<td><a href="index_abbreviation_F.html">F</a></td>
-<td><a href="index_abbreviation_G.html">G</a></td>
-<td><a href="index_abbreviation_H.html">H</a></td>
-<td><a href="index_abbreviation_I.html">I</a></td>
-<td><a href="index_abbreviation_J.html">J</a></td>
-<td><a href="index_abbreviation_K.html">K</a></td>
-<td><a href="index_abbreviation_L.html">L</a></td>
-<td><a href="index_abbreviation_M.html">M</a></td>
-<td><a href="index_abbreviation_N.html">N</a></td>
-<td><a href="index_abbreviation_O.html">O</a></td>
-<td><a href="index_abbreviation_P.html">P</a></td>
-<td><a href="index_abbreviation_Q.html">Q</a></td>
-<td><a href="index_abbreviation_R.html">R</a></td>
-<td><a href="index_abbreviation_S.html">S</a></td>
-<td><a href="index_abbreviation_T.html">T</a></td>
-<td><a href="index_abbreviation_U.html">U</a></td>
-<td><a href="index_abbreviation_V.html">V</a></td>
-<td><a href="index_abbreviation_W.html">W</a></td>
-<td><a href="index_abbreviation_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_abbreviation_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(728 entries)</td>
-</tr>
-<tr>
-<td>Definition Index</td>
-<td><a href="index_definition_A.html">A</a></td>
-<td><a href="index_definition_B.html">B</a></td>
-<td><a href="index_definition_C.html">C</a></td>
-<td><a href="index_definition_D.html">D</a></td>
-<td><a href="index_definition_E.html">E</a></td>
-<td><a href="index_definition_F.html">F</a></td>
-<td><a href="index_definition_G.html">G</a></td>
-<td><a href="index_definition_H.html">H</a></td>
-<td><a href="index_definition_I.html">I</a></td>
-<td><a href="index_definition_J.html">J</a></td>
-<td><a href="index_definition_K.html">K</a></td>
-<td><a href="index_definition_L.html">L</a></td>
-<td><a href="index_definition_M.html">M</a></td>
-<td><a href="index_definition_N.html">N</a></td>
-<td><a href="index_definition_O.html">O</a></td>
-<td><a href="index_definition_P.html">P</a></td>
-<td><a href="index_definition_Q.html">Q</a></td>
-<td><a href="index_definition_R.html">R</a></td>
-<td><a href="index_definition_S.html">S</a></td>
-<td><a href="index_definition_T.html">T</a></td>
-<td><a href="index_definition_U.html">U</a></td>
-<td><a href="index_definition_V.html">V</a></td>
-<td><a href="index_definition_W.html">W</a></td>
-<td><a href="index_definition_X.html">X</a></td>
-<td>Y</td>
-<td><a href="index_definition_Z.html">Z</a></td>
-<td>_</td>
-<td>other</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><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>
-<td>H</td>
-<td><a href="index_record_I.html">I</a></td>
-<td>J</td>
-<td>K</td>
-<td>L</td>
-<td><a href="index_record_M.html">M</a></td>
-<td><a href="index_record_N.html">N</a></td>
-<td>O</td>
-<td><a href="index_record_P.html">P</a></td>
-<td><a href="index_record_Q.html">Q</a></td>
-<td><a href="index_record_R.html">R</a></td>
-<td><a href="index_record_S.html">S</a></td>
-<td><a href="index_record_T.html">T</a></td>
-<td><a href="index_record_U.html">U</a></td>
-<td><a href="index_record_V.html">V</a></td>
-<td>W</td>
-<td>X</td>
-<td>Y</td>
-<td><a href="index_record_Z.html">Z</a></td>
-<td>_</td>
-<td>other</td>
-<td>(189 entries)</td>
-</tr>
-</table>
-</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