removing everything but index which redirects to the new page

author: Cyril Cohen 2019-10-16 11:26:43 +0200
committer: Cyril Cohen 2019-10-16 11:26:43 +0200
commit: 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch)
tree: 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/index_global_L.html
parent: dd82aaeae7e9478efc178ce8430986649555b032 (diff)
1 files changed, 0 insertions, 1604 deletions
diff --git a/docs/htmldoc/index_global_L.html b/docs/htmldoc/index_global_L.html
deleted file mode 100644
index 0864480..0000000
--- a/docs/htmldoc/index_global_L.html
+++ /dev/null
@@ -1,1604 +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="global_L"></a><h2>L </h2>
-<a href="mathcomp.fingroup.fingroup.html#Lagrange">Lagrange</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#Lagrange">Lagrange</a> [section, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#LagrangeI">LagrangeI</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#LagrangeMl">LagrangeMl</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#LagrangeMr">LagrangeMr</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#Lagrange_index">Lagrange_index</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#Lagrange.gT">Lagrange.gT</a> [variable, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.field.separable.html#large_field_PET">large_field_PET</a> [lemma, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last">last</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#lastI">lastI</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#LastNil">LastNil</a> [constructor, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#lastP">lastP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#LastRcons">LastRcons</a> [constructor, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.path.html#last_traject">last_traject</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last_map">last_map</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last_eq">last_eq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last_nth">last_nth</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last_ind">last_ind</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last_spec">last_spec</a> [inductive, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last_rcons">last_rcons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last_cat">last_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#last_cons">last_cons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmn">lcmn</a> [definition, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmnA">lcmnA</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmnAC">lcmnAC</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmnACA">lcmnACA</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmnC">lcmnC</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmnCA">lcmnCA</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmnMl">lcmnMl</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmnMr">lcmnMr</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmn_idPl">lcmn_idPl</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmn_idPr">lcmn_idPr</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmn_gt0">lcmn_gt0</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmn0">lcmn0</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcmn1">lcmn1</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcm0n">lcm0n</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#lcm1n">lcm1n</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcnE">lcnE</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcnP">lcnP</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcnS">lcnS</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcnSn">lcnSn</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcnSnS">lcnSnS</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.field.separable.html#lcn_neq0">lcn_neq0</a> [abbreviation, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_cont">lcn_cont</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_nil_classP">lcn_nil_classP</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_bigdprod">lcn_bigdprod</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_bigcprod">lcn_bigcprod</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_dprod">lcn_dprod</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_cprod">lcn_cprod</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_sub_leq">lcn_sub_leq</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_central">lcn_central</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_normalS">lcn_normalS</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_subS">lcn_subS</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_norm">lcn_norm</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_sub">lcn_sub</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_normal">lcn_normal</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_char">lcn_char</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn_group_set">lcn_group_set</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn0">lcn0</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn1">lcn1</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lcn2">lcn2</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.burnside_app.html#Lcorrect">Lcorrect</a> [lemma, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset">lcoset</a> [definition, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcosetE">lcosetE</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcosetK">lcosetK</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcosetKV">lcosetKV</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcosetM">lcosetM</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcosetP">lcosetP</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcosetS">lcosetS</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcosets">lcosets</a> [definition, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcosetsP">lcosetsP</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset_id">lcoset_id</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset_trans">lcoset_trans</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset_transl">lcoset_transl</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset_eqP">lcoset_eqP</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset_sym">lcoset_sym</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset_refl">lcoset_refl</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset_inj">lcoset_inj</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lcoset1">lcoset1</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#Ldiv">Ldiv</a> [definition, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#LdivJ">LdivJ</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#LdivP">LdivP</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#LdivT_J">LdivT_J</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.algebra.polyXY.html#lead_coef_poly_XaY">lead_coef_poly_XaY</a> [lemma, in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_map">lead_coef_map</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_comp">lead_coef_comp</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_exp">lead_coef_exp</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefZ">lead_coefZ</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefM">lead_coefM</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_map_eq">lead_coef_map_eq</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_map_inj">lead_coef_map_inj</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_map_id0">lead_coef_map_id0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_lreg">lead_coef_lreg</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_Mmonic">lead_coef_Mmonic</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_monicM">lead_coef_monicM</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefXn">lead_coefXn</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefMX">lead_coefMX</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefXsubC">lead_coefXsubC</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefX">lead_coefX</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_proper_mul">lead_coef_proper_mul</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef1">lead_coef1</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefDr">lead_coefDr</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefDl">lead_coefDl</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_opp">lead_coef_opp</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_eq0">lead_coef_eq0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef0">lead_coef0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef_poly">lead_coef_poly</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefC">lead_coefC</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coefE">lead_coefE</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lead_coef">lead_coef</a> [definition, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.field.algC.html#leC_nat">leC_nat</a> [definition, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.ssreflect.path.html#left_arc">left_arc</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
-<a href="mathcomp.ssreflect.generic_quotient.html#left_trans">left_trans</a> [lemma, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#left_mx_ideal">left_mx_ideal</a> [definition, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#leNz_nat">leNz_nat</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leP">leP</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq">leq</a> [definition, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqif">leqif</a> [definition, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqifP">leqifP</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqif_mul">leqif_mul</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqif_add">leqif_add</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqif_eq">leqif_eq</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqif_geq">leqif_geq</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqif_trans">leqif_trans</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqif_refl">leqif_refl</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.bigop.html#leqif_sum">leqif_sum</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqNgt">leqNgt</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqnn">leqnn</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#LeqNotGtn">LeqNotGtn</a> [constructor, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqnSn">leqnSn</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqn0">leqn0</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqP">leqP</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqSpred">leqSpred</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqW">leqW</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqW_nmono_in">leqW_nmono_in</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqW_mono_in">leqW_mono_in</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqW_nmono">leqW_nmono</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leqW_mono">leqW_mono</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.fingroup.quotient.html#leq_quotient">leq_quotient</a> [lemma, in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/>
-<a href="mathcomp.ssreflect.binomial.html#leq_bin2l">leq_bin2l</a> [lemma, in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/>
-<a href="mathcomp.ssreflect.path.html#leq_index">leq_index</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#leq_divLR">leq_divLR</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#leq_divDl">leq_divDl</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#leq_div2l">leq_div2l</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#leq_div2r">leq_div2r</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#leq_divRL">leq_divRL</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#leq_div">leq_div</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#leq_mod">leq_mod</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#leq_trunc_div">leq_trunc_div</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#leq_size_perm">leq_size_perm</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#leq_size_uniq">leq_size_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#leq_ord">leq_ord</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#leq_bump2">leq_bump2</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#leq_bump">leq_bump</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#leq_image_card">leq_image_card</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_nmono_in">leq_nmono_in</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_mono_in">leq_mono_in</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_nmono">leq_nmono</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_mono">leq_mono</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_sqr">leq_sqr</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_Sdouble">leq_Sdouble</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_double">leq_double</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_b1">leq_b1</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_exp2r">leq_exp2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_pexp2l">leq_pexp2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_exp2l">leq_exp2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_pmul2r">leq_pmul2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_pmul2l">leq_pmul2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_mul">leq_mul</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_mul2r">leq_mul2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_mul2l">leq_mul2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_pmulr">leq_pmulr</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_pmull">leq_pmull</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_min">leq_min</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_maxr">leq_maxr</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_maxl">leq_maxl</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_max">leq_max</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_sub">leq_sub</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_sub2l">leq_sub2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_sub2r">leq_sub2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_subr">leq_subr</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_subLR">leq_subLR</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_addl">leq_addl</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_addr">leq_addr</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_add">leq_add</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_add2r">leq_add2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_add2l">leq_add2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_xor_gtn">leq_xor_gtn</a> [inductive, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_total">leq_total</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_ltn_trans">leq_ltn_trans</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_trans">leq_trans</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_eqVlt">leq_eqVlt</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_gtF">leq_gtF</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq_pred">leq_pred</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.algebra.poly.html#leq_sizeP">leq_sizeP</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.ssreflect.bigop.html#leq_bigmax">leq_bigmax</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/>
-<a href="mathcomp.ssreflect.bigop.html#leq_bigmax_cond">leq_bigmax_cond</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/>
-<a href="mathcomp.ssreflect.bigop.html#leq_sum">leq_sum</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/>
-<a href="mathcomp.fingroup.morphism.html#leq_homg">leq_homg</a> [lemma, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
-<a href="mathcomp.fingroup.morphism.html#leq_morphim">leq_morphim</a> [lemma, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
-<a href="mathcomp.ssreflect.finset.html#leq_card_cover">leq_card_cover</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/>
-<a href="mathcomp.ssreflect.finset.html#leq_card_setU">leq_card_setU</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/>
-<a href="mathcomp.ssreflect.finset.html#leq_imset_card">leq_imset_card</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#leq0n">leq0n</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#lerq0">lerq0</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif">lersif</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersifF">lersifF</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifField">LersifField</a> [section, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifField.b">LersifField.b</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifField.F">LersifField.F</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifField.x">LersifField.x</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifField.y">LersifField.y</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifField.z">LersifField.z</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersifN">lersifN</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersifNF">lersifNF</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifOrdered">LersifOrdered</a> [section, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifOrdered.b">LersifOrdered.b</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifOrdered.e">LersifOrdered.e</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifOrdered.R">LersifOrdered.R</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifOrdered.x">LersifOrdered.x</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifOrdered.y">LersifOrdered.y</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifOrdered.z">LersifOrdered.z</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifPo">LersifPo</a> [section, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#LersifPo.R">LersifPo.R</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#82bf2ea71d9e8bc83fc9c1dc82554e8c">_ <= _ ?< if _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersifS">lersifS</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersifT">lersifT</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersifW">lersifW</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersifxx">lersifxx</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_in_itv">lersif_in_itv</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_ndivr_mull">lersif_ndivr_mull</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_ndivl_mull">lersif_ndivl_mull</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_ndivr_mulr">lersif_ndivr_mulr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_ndivl_mulr">lersif_ndivl_mulr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_pdivr_mull">lersif_pdivr_mull</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_pdivl_mull">lersif_pdivl_mull</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_pdivr_mulr">lersif_pdivr_mulr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_pdivl_mulr">lersif_pdivl_mulr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_maxl">lersif_maxl</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_maxr">lersif_maxr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_minl">lersif_minl</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_minr">lersif_minr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_distl">lersif_distl</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_normr">lersif_normr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_norml">lersif_norml</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_nnormr">lersif_nnormr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_nmul2r">lersif_nmul2r</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_nmul2l">lersif_nmul2l</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_pmul2r">lersif_pmul2r</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_pmul2l">lersif_pmul2l</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_imply">lersif_imply</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_orb">lersif_orb</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_andb">lersif_andb</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_sub_addl">lersif_sub_addl</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_subr_addl">lersif_subr_addl</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_subl_addl">lersif_subl_addl</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_sub_addr">lersif_sub_addr</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_subr_addr">lersif_subr_addr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_subl_addr">lersif_subl_addr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_add2">lersif_add2</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_add2r">lersif_add2r</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_add2l">lersif_add2l</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_oppE">lersif_oppE</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_opp2">lersif_opp2</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_oppr0">lersif_oppr0</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_0oppr">lersif_0oppr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_oppr">lersif_oppr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_oppl">lersif_oppl</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_anti">lersif_anti</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif_trans">lersif_trans</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#lersif01">lersif01</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lerz0">lerz0</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lerz1">lerz1</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.rat.html#ler_rat">ler_rat</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.interval.html#ler_in_itv">ler_in_itv</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_nexpz2r">ler_nexpz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_pexpz2r">ler_pexpz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wnexpz2r">ler_wnexpz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wpexpz2r">ler_wpexpz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_eexpz2l">ler_eexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_niexpz2l">ler_niexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_piexpz2l">ler_piexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_weexpz2l">ler_weexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wneexpz2l">ler_wneexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wpeexpz2l">ler_wpeexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wniexpz2l">ler_wniexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wpiexpz2l">ler_wpiexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_int">ler_int</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_nmulz2l">ler_nmulz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_pmulz2l">ler_pmulz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wnmulz2l">ler_wnmulz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wpmulz2l">ler_wpmulz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wnmulz2r">ler_wnmulz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_wpmulz2r">ler_wpmulz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_nmulz2r">ler_nmulz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler_pmulz2r">ler_pmulz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.rat.html#ler0q">ler0q</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler0z">ler0z</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ler1z">ler1z</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lezN_nat">lezN_nat</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#lez_divLR">lez_divLR</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#lez_divRL">lez_divRL</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#lez_div">lez_div</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#lez_floor">lez_floor</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lez_addr1">lez_addr1</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lez_add1r">lez_add1r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lez_nat">lez_nat</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lez0_abs">lez0_abs</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lez0_nat">lez0_nat</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.rat.html#le_rat_total">le_rat_total</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#le_rat0_anti">le_rat0_anti</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#le_rat0M">le_rat0M</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#le_rat0D">le_rat0D</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#le_rat0">le_rat0</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#le_rat">le_rat</a> [definition, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundr_total">le_boundr_total</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundl_total">le_boundl_total</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundr_anti">le_boundr_anti</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundl_anti">le_boundl_anti</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundr_bb">le_boundr_bb</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundl_bb">le_boundl_bb</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundr_trans">le_boundr_trans</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundl_trans">le_boundl_trans</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundr_refl">le_boundr_refl</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundl_refl">le_boundl_refl</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundr">le_boundr</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#le_boundl">le_boundl</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#le_irrelevance">le_irrelevance</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#le0z_nat">le0z_nat</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunAlgebra">LfunAlgebra</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunAlgebra.R">LfunAlgebra.R</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunAlgebra.vT">LfunAlgebra.vT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunAlgebra.vT_proper">LfunAlgebra.vT_proper</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunDefs">LfunDefs</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunDefs.R">LfunDefs.R</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfunE">lfunE</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfunP">lfunP</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfunPn">lfunPn</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunVectType">LfunVectType</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunVectType.aT">LfunVectType.aT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunVectType.R">LfunVectType.R</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunVectType.rT">LfunVectType.rT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#56c5b67537d06f866a5342dee7b6401b">_ *:l _</a> [notation, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunVspaceDefs">LfunVspaceDefs</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunVspaceDefs.K">LfunVspaceDefs.K</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunZmodType">LfunZmodType</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunZmodType.aT">LfunZmodType.aT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunZmodType.R">LfunZmodType.R</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LfunZmodType.rT">LfunZmodType.rT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_algType">lfun_algType</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_lalgType">lfun_lalgType</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_ringType">lfun_ringType</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_ringMixin">lfun_ringMixin</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_comp_ringType">lfun_comp_ringType</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_comp_ringMixin">lfun_comp_ringMixin</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_simp">lfun_simp</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_vectMixin">lfun_vectMixin</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_vect_iso">lfun_vect_iso</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_lmodMixin">lfun_lmodMixin</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_scaleDl">lfun_scaleDl</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_scaleDr">lfun_scaleDr</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_scale1">lfun_scale1</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_scaleA">lfun_scaleA</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_zmodMixin">lfun_zmodMixin</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_addN">lfun_addN</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_add0">lfun_add0</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_addC">lfun_addC</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_addA">lfun_addA</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_is_linear">lfun_is_linear</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_choiceMixin">lfun_choiceMixin</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_eqMixin">lfun_eqMixin</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_preim">lfun_preim</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_img">lfun_img</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_img_def">lfun_img_def</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_img_key">lfun_img_key</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun_key">lfun_key</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lfun1_neq0">lfun1_neq0</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.field.falgebra.html#lfun1_poly">lfun1_poly</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#lift">lift</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#liftK">liftK</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#LiftPerm">LiftPerm</a> [section, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#LiftPerm.n">LiftPerm.n</a> [variable, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#lift_permV">lift_permV</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#lift_perm1">lift_perm1</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#lift_permM">lift_permM</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#lift_perm_lift">lift_perm_lift</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#lift_perm_id">lift_perm_id</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#lift_perm">lift_perm</a> [definition, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#lift_permK">lift_permK</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.fingroup.perm.html#lift_perm_fun">lift_perm_fun</a> [definition, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
-<a href="mathcomp.ssreflect.generic_quotient.html#lift_embed">lift_embed</a> [abbreviation, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/>
-<a href="mathcomp.ssreflect.generic_quotient.html#lift_cst">lift_cst</a> [abbreviation, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/>
-<a href="mathcomp.ssreflect.generic_quotient.html#lift_op11">lift_op11</a> [abbreviation, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/>
-<a href="mathcomp.ssreflect.generic_quotient.html#lift_fun2">lift_fun2</a> [abbreviation, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/>
-<a href="mathcomp.ssreflect.generic_quotient.html#lift_fun1">lift_fun1</a> [abbreviation, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/>
-<a href="mathcomp.ssreflect.generic_quotient.html#lift_op2">lift_op2</a> [abbreviation, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/>
-<a href="mathcomp.ssreflect.generic_quotient.html#lift_op1">lift_op1</a> [abbreviation, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#lift_max">lift_max</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#lift_inj">lift_inj</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#lift_subproof">lift_subproof</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#lift0">lift0</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lift0_mx_is_perm">lift0_mx_is_perm</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lift0_mx_perm">lift0_mx_perm</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lift0_mx">lift0_mx</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lift0_perm_eq0">lift0_perm_eq0</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lift0_permK">lift0_permK</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lift0_perm_lift">lift0_perm_lift</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lift0_perm0">lift0_perm0</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lift0_perm">lift0_perm</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg">limg</a> [abbreviation, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limgS">limgS</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.field.galois.html#limg_gal">limg_gal</a> [lemma, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_proj">limg_proj</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_comp">limg_comp</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_ker0">limg_ker0</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_basis_of">limg_basis_of</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_dim_eq">limg_dim_eq</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_ker_dim">limg_ker_dim</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_ker_compl">limg_ker_compl</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_lfunVK">limg_lfunVK</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_span">limg_span</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_bigcap">limg_bigcap</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_cap">limg_cap</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_sum">limg_sum</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_add">limg_add</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg_line">limg_line</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.field.falgebra.html#limg_amulr">limg_amulr</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.algebra.vector.html#limg0">limg0</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lim0g">lim0g</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lim1g">lim1g</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinAut">LinAut</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinAut.f">LinAut.f</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinAut.K">LinAut.K</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinAut.kerf0">LinAut.kerf0</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinAut.vT">LinAut.vT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.rat.html#Linear">Linear</a> [section, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.character.character.html#Linear">Linear</a> [section, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImage">LinearImage</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImageComp">LinearImageComp</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImageComp.aT">LinearImageComp.aT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImageComp.K">LinearImageComp.K</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImageComp.rT">LinearImageComp.rT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImageComp.vT">LinearImageComp.vT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImage.aT">LinearImage.aT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImage.K">LinearImage.K</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearImage.rT">LinearImage.rT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#linearMn">linearMn</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearPreimage">LinearPreimage</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearPreimage.aT">LinearPreimage.aT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearPreimage.K">LinearPreimage.K</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#LinearPreimage.rT">LinearPreimage.rT</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#linear_irr_comp">linear_irr_comp</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#linear_irr">linear_irr</a> [definition, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#linear_mxsimple">linear_mxsimple</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#linear_mx_abs_irr">linear_mx_abs_irr</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.algebra.vector.html#linear_of_free">linear_of_free</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.character.character.html#linear_char_divr">linear_char_divr</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#linear_char_key">linear_char_key</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#linear_char">linear_char</a> [definition, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#Linear.G">Linear.G</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#Linear.gT">Linear.gT</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#Linear.OneChar">Linear.OneChar</a> [section, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#Linear.OneChar.CFxi">Linear.OneChar.CFxi</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#Linear.OneChar.xi">Linear.OneChar.xi</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#Linear.OneChar.xiMV">Linear.OneChar.xiMV</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.algebra.vector.html#linfun">linfun</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#linfun_def">linfun_def</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.field.falgebra.html#linfun_is_ahom">linfun_is_ahom</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin_mul_row_is_linear">lin_mul_row_is_linear</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin_mul_row">lin_mul_row</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin_mulmx_is_linear">lin_mulmx_is_linear</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin_mulmx">lin_mulmx</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin_mulmxr_is_linear">lin_mulmxr_is_linear</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin_mulmxr">lin_mulmxr</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin_mx">lin_mx</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.character.character.html#lin_char_group">lin_char_group</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_irr_der1">lin_irr_der1</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_Res_IirrE">lin_Res_IirrE</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_char_der1">lin_char_der1</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_char_unitr">lin_char_unitr</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_char_irr">lin_char_irr</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_charV_conj">lin_charV_conj</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_char_unity_root">lin_char_unity_root</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_charX">lin_charX</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_charV">lin_charV</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_char_neq0">lin_char_neq0</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_char_prod">lin_char_prod</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_charM">lin_charM</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_charW">lin_charW</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#lin_char1">lin_char1</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin1_mx">lin1_mx</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lin1_mx_key">lin1_mx_key</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker">lker</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lkerE">lkerE</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker_proj">lker_proj</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0P">lker0P</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_compfVK">lker0_compfVK</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_compfK">lker0_compfK</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_compKf">lker0_compKf</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_compVKf">lker0_compVKf</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_compfV">lker0_compfV</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_lfunVK">lker0_lfunVK</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_limgf">lker0_limgf</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_compVf">lker0_compVf</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lker0_lfunK">lker0_lfunK</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.field.falgebra.html#lker0_amulr">lker0_amulr</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#lker0_amull">lker0_amull</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#LMod">LMod</a> [section, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#LMod.R">LMod.R</a> [variable, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#LMod.V">LMod.V</a> [variable, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn">logn</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#lognE">lognE</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#lognM">lognM</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#lognSg">lognSg</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#lognX">lognX</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.solvable.pgroup.html#logn_quotient_cent_cyclic_pgroup">logn_quotient_cent_cyclic_pgroup</a> [lemma, in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/>
-<a href="mathcomp.fingroup.quotient.html#logn_morphim">logn_morphim</a> [lemma, in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/>
-<a href="mathcomp.ssreflect.binomial.html#logn_fact">logn_fact</a> [lemma, in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn_part">logn_part</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn_count_dvd">logn_count_dvd</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn_div">logn_div</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn_Gauss">logn_Gauss</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn_prime">logn_prime</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn_gt0">logn_gt0</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn_rec">logn_rec</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#logn_quotient">logn_quotient</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.solvable.abelian.html#logn_le_p_rank">logn_le_p_rank</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#logn_card_GL_p">logn_card_GL_p</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn0">logn0</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#logn1">logn1</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.fingroup.automorphism.html#lone_subgroup_char">lone_subgroup_char</a> [lemma, in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/>
-<a href="mathcomp.ssreflect.path.html#looping">looping</a> [definition, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
-<a href="mathcomp.ssreflect.path.html#loopingP">loopingP</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
-<a href="mathcomp.ssreflect.path.html#looping_uniq">looping_uniq</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
-<a href="mathcomp.ssreflect.fingraph.html#looping_order">looping_order</a> [lemma, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#LowerCentral">LowerCentral</a> [section, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#LowerCentral.gT">LowerCentral.gT</a> [variable, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lower_central_at">lower_central_at</a> [definition, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.solvable.nilpotent.html#lower_central_at_rec">lower_central_at_rec</a> [definition, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lpreimK">lpreimK</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lpreimS">lpreimS</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lpreim_cap_limg">lpreim_cap_limg</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.vector.html#lpreim0">lpreim0</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lreg_polyZ_eq0">lreg_polyZ_eq0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lreg_size">lreg_size</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lreg_lead0">lreg_lead0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lreg_lead">lreg_lead</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#lshift">lshift</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#lshift_subproof">lshift_subproof</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.algebra.zmodp.html#lshift0">lshift0</a> [lemma, in <a href="mathcomp.algebra.zmodp.html">mathcomp.algebra.zmodp</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lsubmx">lsubmx</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.algebra.matrix.html#lsubmx_key">lsubmx_key</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.field.algC.html#ltC_nat">ltC_nat</a> [definition, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#lteNz_nat">lteNz_nat</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltezN_nat">ltezN_nat</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltez_natE">ltez_natE</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltez_nat">ltez_nat</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmx">ltmx</a> [definition, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmxE">ltmxE</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmxEneq">ltmxEneq</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmxErank">ltmxErank</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmxW">ltmxW</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmx_irrefl">ltmx_irrefl</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmx_trans">ltmx_trans</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmx_sub_trans">ltmx_sub_trans</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmx0">ltmx0</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#ltmx1">ltmx1</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn">ltn</a> [definition, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltngtP">ltngtP</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnn">ltnn</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnNge">ltnNge</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#LtnNotGeq">LtnNotGeq</a> [constructor, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnP">ltnP</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnS">ltnS</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnSn">ltnSn</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnW">ltnW</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnW_nhomo_in">ltnW_nhomo_in</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnW_homo_in">ltnW_homo_in</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnW_nhomo">ltnW_nhomo</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltnW_homo">ltnW_homo</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltNz_nat">ltNz_nat</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.solvable.pgroup.html#ltn_log_quotient">ltn_log_quotient</a> [lemma, in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/>
-<a href="mathcomp.fingroup.quotient.html#ltn_quotient">ltn_quotient</a> [lemma, in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/>
-<a href="mathcomp.ssreflect.path.html#ltn_index">ltn_index</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
-<a href="mathcomp.ssreflect.path.html#ltn_sorted_uniq_leq">ltn_sorted_uniq_leq</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/>
-<a href="mathcomp.solvable.frobenius.html#ltn_odd_Frobenius_ker">ltn_odd_Frobenius_ker</a> [lemma, in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#ltn_logl">ltn_logl</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#ltn_log0">ltn_log0</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#ltn_pdiv2_prime">ltn_pdiv2_prime</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#ltn_divRL">ltn_divRL</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#ltn_Pdiv">ltn_Pdiv</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#ltn_divLR">ltn_divLR</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#ltn_ceil">ltn_ceil</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#ltn_pmod">ltn_pmod</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.div.html#ltn_mod">ltn_mod</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
-<a href="mathcomp.ssreflect.seq.html#ltn_size_undup">ltn_size_undup</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#ltn_unsplit">ltn_unsplit</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#ltn_ord">ltn_ord</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_leqif">ltn_leqif</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_sqr">ltn_sqr</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_Sdouble">ltn_Sdouble</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_double">ltn_double</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_exp2r">ltn_exp2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_pexp2l">ltn_pexp2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_exp2l">ltn_exp2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_expl">ltn_expl</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_mul">ltn_mul</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_Pmulr">ltn_Pmulr</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_Pmull">ltn_Pmull</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_pmul2r">ltn_pmul2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_pmul2l">ltn_pmul2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_mul2r">ltn_mul2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_mul2l">ltn_mul2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_subRL">ltn_subRL</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_sub2l">ltn_sub2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_sub2r">ltn_sub2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_addl">ltn_addl</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_addr">ltn_addr</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_add2r">ltn_add2r</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_add2l">ltn_add2l</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_xor_geq">ltn_xor_geq</a> [inductive, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_trans">ltn_trans</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_neqAle">ltn_neqAle</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_geF">ltn_geF</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_eqF">ltn_eqF</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn_predK">ltn_predK</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.fingroup.morphism.html#ltn_morphim">ltn_morphim</a> [lemma, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn0">ltn0</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltn0Sn">ltn0Sn</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#ltP">ltP</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#ltrq0">ltrq0</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.interval.html#ltrW_lersif">ltrW_lersif</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltrz0">ltrz0</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltrz1">ltrz1</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.rat.html#ltr_rat">ltr_rat</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.interval.html#ltr_in_itv">ltr_in_itv</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_nexpz2r">ltr_nexpz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_pexpz2r">ltr_pexpz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_eexpz2l">ltr_eexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_niexpz2l">ltr_niexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_piexpz2l">ltr_piexpz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_int">ltr_int</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_nmulz2l">ltr_nmulz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_pmulz2l">ltr_pmulz2l</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_nmulz2r">ltr_nmulz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr_pmulz2r">ltr_pmulz2r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.rat.html#ltr0q">ltr0q</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr0z">ltr0z</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr0_sgz">ltr0_sgz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltr1z">ltr1z</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltzN_nat">ltzN_nat</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#ltz_divRL">ltz_divRL</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#ltz_divLR">ltz_divLR</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#ltz_ceil">ltz_ceil</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#ltz_mod">ltz_mod</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.intdiv.html#ltz_pmod">ltz_pmod</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltz_addr1">ltz_addr1</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltz_add1r">ltz_add1r</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltz_nat">ltz_nat</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#ltz0_abs">ltz0_abs</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.rat.html#lt_rat_def">lt_rat_def</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#lt_rat0">lt_rat0</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.algebra.rat.html#lt_rat">lt_rat</a> [definition, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#lt_irrelevance">lt_irrelevance</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.algebra.poly.html#lt_size_deriv">lt_size_deriv</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#lt_eqmx">lt_eqmx</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#lt0b">lt0b</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#lt0mx">lt0mx</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#lt0n">lt0n</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.ssreflect.ssrnat.html#lt0n_neq0">lt0n_neq0</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#lt1mx">lt1mx</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.algebra.mxalgebra.html#LUP_card_GL">LUP_card_GL</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
-<a href="mathcomp.field.fieldext.html#L_F">L_F</a> [abbreviation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.solvable.burnside_app.html#L_iso">L_iso</a> [lemma, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/>
-<a href="mathcomp.field.fieldext.html#L0">L0</a> [abbreviation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</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
author	Cyril Cohen	2019-10-16 11:26:43 +0200
committer	Cyril Cohen	2019-10-16 11:26:43 +0200
commit	6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch)
tree	1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/index_global_L.html
parent	dd82aaeae7e9478efc178ce8430986649555b032 (diff)