diff options
| 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_lemma_S.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/index_lemma_S.html')
| -rw-r--r-- | docs/htmldoc/index_lemma_S.html | 1926 |
1 files changed, 0 insertions, 1926 deletions
diff --git a/docs/htmldoc/index_lemma_S.html b/docs/htmldoc/index_lemma_S.html deleted file mode 100644 index 1ef1855..0000000 --- a/docs/htmldoc/index_lemma_S.html +++ /dev/null @@ -1,1926 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.test_suite.hierarchy_test</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<table> -<tr> -<td>Global Index</td> -<td><a href="index_global_A.html">A</a></td> -<td><a href="index_global_B.html">B</a></td> -<td><a href="index_global_C.html">C</a></td> -<td><a href="index_global_D.html">D</a></td> -<td><a href="index_global_E.html">E</a></td> -<td><a href="index_global_F.html">F</a></td> -<td><a href="index_global_G.html">G</a></td> -<td><a href="index_global_H.html">H</a></td> -<td><a href="index_global_I.html">I</a></td> -<td><a href="index_global_J.html">J</a></td> -<td><a href="index_global_K.html">K</a></td> -<td><a href="index_global_L.html">L</a></td> -<td><a href="index_global_M.html">M</a></td> -<td><a href="index_global_N.html">N</a></td> -<td><a href="index_global_O.html">O</a></td> -<td><a href="index_global_P.html">P</a></td> -<td><a href="index_global_Q.html">Q</a></td> -<td><a href="index_global_R.html">R</a></td> -<td><a href="index_global_S.html">S</a></td> -<td><a href="index_global_T.html">T</a></td> -<td><a href="index_global_U.html">U</a></td> -<td><a href="index_global_V.html">V</a></td> -<td><a href="index_global_W.html">W</a></td> -<td><a href="index_global_X.html">X</a></td> -<td>Y</td> -<td><a href="index_global_Z.html">Z</a></td> -<td>_</td> -<td><a href="index_global_*.html">other</a></td> -<td>(23836 entries)</td> -</tr> -<tr> -<td>Notation Index</td> -<td><a href="index_notation_A.html">A</a></td> -<td><a href="index_notation_B.html">B</a></td> -<td><a href="index_notation_C.html">C</a></td> -<td><a href="index_notation_D.html">D</a></td> -<td><a href="index_notation_E.html">E</a></td> -<td><a href="index_notation_F.html">F</a></td> -<td><a href="index_notation_G.html">G</a></td> -<td>H</td> -<td><a href="index_notation_I.html">I</a></td> -<td>J</td> -<td><a href="index_notation_K.html">K</a></td> -<td><a href="index_notation_L.html">L</a></td> -<td><a href="index_notation_M.html">M</a></td> -<td><a href="index_notation_N.html">N</a></td> -<td>O</td> -<td><a href="index_notation_P.html">P</a></td> -<td><a href="index_notation_Q.html">Q</a></td> -<td><a href="index_notation_R.html">R</a></td> -<td><a href="index_notation_S.html">S</a></td> -<td>T</td> -<td><a href="index_notation_U.html">U</a></td> -<td><a href="index_notation_V.html">V</a></td> -<td>W</td> -<td>X</td> -<td>Y</td> -<td><a href="index_notation_Z.html">Z</a></td> -<td>_</td> -<td><a href="index_notation_*.html">other</a></td> -<td>(1409 entries)</td> -</tr> -<tr> -<td>Module Index</td> -<td><a href="index_module_A.html">A</a></td> -<td><a href="index_module_B.html">B</a></td> -<td><a href="index_module_C.html">C</a></td> -<td><a href="index_module_D.html">D</a></td> -<td><a href="index_module_E.html">E</a></td> -<td><a href="index_module_F.html">F</a></td> -<td><a href="index_module_G.html">G</a></td> -<td>H</td> -<td><a href="index_module_I.html">I</a></td> -<td>J</td> -<td>K</td> -<td>L</td> -<td><a href="index_module_M.html">M</a></td> -<td><a href="index_module_N.html">N</a></td> -<td>O</td> -<td><a href="index_module_P.html">P</a></td> -<td><a href="index_module_Q.html">Q</a></td> -<td><a href="index_module_R.html">R</a></td> -<td><a href="index_module_S.html">S</a></td> -<td>T</td> -<td><a href="index_module_U.html">U</a></td> -<td><a href="index_module_V.html">V</a></td> -<td>W</td> -<td>X</td> -<td>Y</td> -<td>Z</td> -<td>_</td> -<td>other</td> -<td>(221 entries)</td> -</tr> -<tr> -<td>Variable Index</td> -<td><a href="index_variable_A.html">A</a></td> -<td><a href="index_variable_B.html">B</a></td> -<td><a href="index_variable_C.html">C</a></td> -<td><a href="index_variable_D.html">D</a></td> -<td><a href="index_variable_E.html">E</a></td> -<td><a href="index_variable_F.html">F</a></td> -<td><a href="index_variable_G.html">G</a></td> -<td><a href="index_variable_H.html">H</a></td> -<td><a href="index_variable_I.html">I</a></td> -<td>J</td> -<td><a href="index_variable_K.html">K</a></td> -<td><a href="index_variable_L.html">L</a></td> -<td><a href="index_variable_M.html">M</a></td> -<td><a href="index_variable_N.html">N</a></td> -<td><a href="index_variable_O.html">O</a></td> -<td><a href="index_variable_P.html">P</a></td> -<td><a href="index_variable_Q.html">Q</a></td> -<td><a href="index_variable_R.html">R</a></td> -<td><a href="index_variable_S.html">S</a></td> -<td><a href="index_variable_T.html">T</a></td> -<td><a href="index_variable_U.html">U</a></td> -<td><a href="index_variable_V.html">V</a></td> -<td>W</td> -<td>X</td> -<td>Y</td> -<td><a href="index_variable_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(3574 entries)</td> -</tr> -<tr> -<td>Library Index</td> -<td><a href="index_library_A.html">A</a></td> -<td><a href="index_library_B.html">B</a></td> -<td><a href="index_library_C.html">C</a></td> -<td><a href="index_library_D.html">D</a></td> -<td><a href="index_library_E.html">E</a></td> -<td><a href="index_library_F.html">F</a></td> -<td><a href="index_library_G.html">G</a></td> -<td><a href="index_library_H.html">H</a></td> -<td><a href="index_library_I.html">I</a></td> -<td><a href="index_library_J.html">J</a></td> -<td>K</td> -<td>L</td> -<td><a href="index_library_M.html">M</a></td> -<td><a href="index_library_N.html">N</a></td> -<td>O</td> -<td><a href="index_library_P.html">P</a></td> -<td><a href="index_library_Q.html">Q</a></td> -<td><a href="index_library_R.html">R</a></td> -<td><a href="index_library_S.html">S</a></td> -<td><a href="index_library_T.html">T</a></td> -<td>U</td> -<td><a href="index_library_V.html">V</a></td> -<td>W</td> -<td>X</td> -<td>Y</td> -<td><a href="index_library_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(90 entries)</td> -</tr> -<tr> -<td>Lemma Index</td> -<td><a href="index_lemma_A.html">A</a></td> -<td><a href="index_lemma_B.html">B</a></td> -<td><a href="index_lemma_C.html">C</a></td> -<td><a href="index_lemma_D.html">D</a></td> -<td><a href="index_lemma_E.html">E</a></td> -<td><a href="index_lemma_F.html">F</a></td> -<td><a href="index_lemma_G.html">G</a></td> -<td><a href="index_lemma_H.html">H</a></td> -<td><a href="index_lemma_I.html">I</a></td> -<td><a href="index_lemma_J.html">J</a></td> -<td><a href="index_lemma_K.html">K</a></td> -<td><a href="index_lemma_L.html">L</a></td> -<td><a href="index_lemma_M.html">M</a></td> -<td><a href="index_lemma_N.html">N</a></td> -<td><a href="index_lemma_O.html">O</a></td> -<td><a href="index_lemma_P.html">P</a></td> -<td><a href="index_lemma_Q.html">Q</a></td> -<td><a href="index_lemma_R.html">R</a></td> -<td><a href="index_lemma_S.html">S</a></td> -<td><a href="index_lemma_T.html">T</a></td> -<td><a href="index_lemma_U.html">U</a></td> -<td><a href="index_lemma_V.html">V</a></td> -<td><a href="index_lemma_W.html">W</a></td> -<td><a href="index_lemma_X.html">X</a></td> -<td>Y</td> -<td><a href="index_lemma_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(12096 entries)</td> -</tr> -<tr> -<td>Constructor Index</td> -<td><a href="index_constructor_A.html">A</a></td> -<td><a href="index_constructor_B.html">B</a></td> -<td><a href="index_constructor_C.html">C</a></td> -<td><a href="index_constructor_D.html">D</a></td> -<td><a href="index_constructor_E.html">E</a></td> -<td><a href="index_constructor_F.html">F</a></td> -<td><a href="index_constructor_G.html">G</a></td> -<td><a href="index_constructor_H.html">H</a></td> -<td><a href="index_constructor_I.html">I</a></td> -<td>J</td> -<td>K</td> -<td><a href="index_constructor_L.html">L</a></td> -<td><a href="index_constructor_M.html">M</a></td> -<td><a href="index_constructor_N.html">N</a></td> -<td><a href="index_constructor_O.html">O</a></td> -<td><a href="index_constructor_P.html">P</a></td> -<td><a href="index_constructor_Q.html">Q</a></td> -<td><a href="index_constructor_R.html">R</a></td> -<td><a href="index_constructor_S.html">S</a></td> -<td><a href="index_constructor_T.html">T</a></td> -<td><a href="index_constructor_U.html">U</a></td> -<td><a href="index_constructor_V.html">V</a></td> -<td>W</td> -<td><a href="index_constructor_X.html">X</a></td> -<td>Y</td> -<td><a href="index_constructor_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(368 entries)</td> -</tr> -<tr> -<td>Axiom Index</td> -<td><a href="index_axiom_A.html">A</a></td> -<td><a href="index_axiom_B.html">B</a></td> -<td><a href="index_axiom_C.html">C</a></td> -<td>D</td> -<td><a href="index_axiom_E.html">E</a></td> -<td><a href="index_axiom_F.html">F</a></td> -<td>G</td> -<td>H</td> -<td><a href="index_axiom_I.html">I</a></td> -<td>J</td> -<td>K</td> -<td>L</td> -<td>M</td> -<td>N</td> -<td>O</td> -<td><a href="index_axiom_P.html">P</a></td> -<td>Q</td> -<td><a href="index_axiom_R.html">R</a></td> -<td><a href="index_axiom_S.html">S</a></td> -<td>T</td> -<td>U</td> -<td>V</td> -<td>W</td> -<td>X</td> -<td>Y</td> -<td>Z</td> -<td>_</td> -<td>other</td> -<td>(45 entries)</td> -</tr> -<tr> -<td>Inductive Index</td> -<td><a href="index_inductive_A.html">A</a></td> -<td><a href="index_inductive_B.html">B</a></td> -<td><a href="index_inductive_C.html">C</a></td> -<td><a href="index_inductive_D.html">D</a></td> -<td><a href="index_inductive_E.html">E</a></td> -<td><a href="index_inductive_F.html">F</a></td> -<td><a href="index_inductive_G.html">G</a></td> -<td><a href="index_inductive_H.html">H</a></td> -<td><a href="index_inductive_I.html">I</a></td> -<td>J</td> -<td>K</td> -<td><a href="index_inductive_L.html">L</a></td> -<td><a href="index_inductive_M.html">M</a></td> -<td><a href="index_inductive_N.html">N</a></td> -<td><a href="index_inductive_O.html">O</a></td> -<td><a href="index_inductive_P.html">P</a></td> -<td>Q</td> -<td><a href="index_inductive_R.html">R</a></td> -<td><a href="index_inductive_S.html">S</a></td> -<td><a href="index_inductive_T.html">T</a></td> -<td><a href="index_inductive_U.html">U</a></td> -<td><a href="index_inductive_V.html">V</a></td> -<td>W</td> -<td><a href="index_inductive_X.html">X</a></td> -<td>Y</td> -<td>Z</td> -<td>_</td> -<td>other</td> -<td>(107 entries)</td> -</tr> -<tr> -<td>Projection Index</td> -<td><a href="index_projection_A.html">A</a></td> -<td><a href="index_projection_B.html">B</a></td> -<td><a href="index_projection_C.html">C</a></td> -<td><a href="index_projection_D.html">D</a></td> -<td><a href="index_projection_E.html">E</a></td> -<td><a href="index_projection_F.html">F</a></td> -<td><a href="index_projection_G.html">G</a></td> -<td>H</td> -<td><a href="index_projection_I.html">I</a></td> -<td>J</td> -<td>K</td> -<td>L</td> -<td><a href="index_projection_M.html">M</a></td> -<td><a href="index_projection_N.html">N</a></td> -<td>O</td> -<td><a href="index_projection_P.html">P</a></td> -<td><a href="index_projection_Q.html">Q</a></td> -<td><a href="index_projection_R.html">R</a></td> -<td><a href="index_projection_S.html">S</a></td> -<td><a href="index_projection_T.html">T</a></td> -<td><a href="index_projection_U.html">U</a></td> -<td><a href="index_projection_V.html">V</a></td> -<td>W</td> -<td>X</td> -<td>Y</td> -<td><a href="index_projection_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(273 entries)</td> -</tr> -<tr> -<td>Section Index</td> -<td><a href="index_section_A.html">A</a></td> -<td><a href="index_section_B.html">B</a></td> -<td><a href="index_section_C.html">C</a></td> -<td><a href="index_section_D.html">D</a></td> -<td><a href="index_section_E.html">E</a></td> -<td><a href="index_section_F.html">F</a></td> -<td><a href="index_section_G.html">G</a></td> -<td><a href="index_section_H.html">H</a></td> -<td><a href="index_section_I.html">I</a></td> -<td>J</td> -<td><a href="index_section_K.html">K</a></td> -<td><a href="index_section_L.html">L</a></td> -<td><a href="index_section_M.html">M</a></td> -<td><a href="index_section_N.html">N</a></td> -<td><a href="index_section_O.html">O</a></td> -<td><a href="index_section_P.html">P</a></td> -<td><a href="index_section_Q.html">Q</a></td> -<td><a href="index_section_R.html">R</a></td> -<td><a href="index_section_S.html">S</a></td> -<td><a href="index_section_T.html">T</a></td> -<td><a href="index_section_U.html">U</a></td> -<td><a href="index_section_V.html">V</a></td> -<td>W</td> -<td>X</td> -<td>Y</td> -<td><a href="index_section_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(1140 entries)</td> -</tr> -<tr> -<td>Abbreviation Index</td> -<td><a href="index_abbreviation_A.html">A</a></td> -<td><a href="index_abbreviation_B.html">B</a></td> -<td><a href="index_abbreviation_C.html">C</a></td> -<td><a href="index_abbreviation_D.html">D</a></td> -<td><a href="index_abbreviation_E.html">E</a></td> -<td><a href="index_abbreviation_F.html">F</a></td> -<td><a href="index_abbreviation_G.html">G</a></td> -<td><a href="index_abbreviation_H.html">H</a></td> -<td><a href="index_abbreviation_I.html">I</a></td> -<td><a href="index_abbreviation_J.html">J</a></td> -<td><a href="index_abbreviation_K.html">K</a></td> -<td><a href="index_abbreviation_L.html">L</a></td> -<td><a href="index_abbreviation_M.html">M</a></td> -<td><a href="index_abbreviation_N.html">N</a></td> -<td><a href="index_abbreviation_O.html">O</a></td> -<td><a href="index_abbreviation_P.html">P</a></td> -<td><a href="index_abbreviation_Q.html">Q</a></td> -<td><a href="index_abbreviation_R.html">R</a></td> -<td><a href="index_abbreviation_S.html">S</a></td> -<td><a href="index_abbreviation_T.html">T</a></td> -<td><a href="index_abbreviation_U.html">U</a></td> -<td><a href="index_abbreviation_V.html">V</a></td> -<td><a href="index_abbreviation_W.html">W</a></td> -<td><a href="index_abbreviation_X.html">X</a></td> -<td>Y</td> -<td><a href="index_abbreviation_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(728 entries)</td> -</tr> -<tr> -<td>Definition Index</td> -<td><a href="index_definition_A.html">A</a></td> -<td><a href="index_definition_B.html">B</a></td> -<td><a href="index_definition_C.html">C</a></td> -<td><a href="index_definition_D.html">D</a></td> -<td><a href="index_definition_E.html">E</a></td> -<td><a href="index_definition_F.html">F</a></td> -<td><a href="index_definition_G.html">G</a></td> -<td><a href="index_definition_H.html">H</a></td> -<td><a href="index_definition_I.html">I</a></td> -<td><a href="index_definition_J.html">J</a></td> -<td><a href="index_definition_K.html">K</a></td> -<td><a href="index_definition_L.html">L</a></td> -<td><a href="index_definition_M.html">M</a></td> -<td><a href="index_definition_N.html">N</a></td> -<td><a href="index_definition_O.html">O</a></td> -<td><a href="index_definition_P.html">P</a></td> -<td><a href="index_definition_Q.html">Q</a></td> -<td><a href="index_definition_R.html">R</a></td> -<td><a href="index_definition_S.html">S</a></td> -<td><a href="index_definition_T.html">T</a></td> -<td><a href="index_definition_U.html">U</a></td> -<td><a href="index_definition_V.html">V</a></td> -<td><a href="index_definition_W.html">W</a></td> -<td><a href="index_definition_X.html">X</a></td> -<td>Y</td> -<td><a href="index_definition_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(3596 entries)</td> -</tr> -<tr> -<td>Record Index</td> -<td><a href="index_record_A.html">A</a></td> -<td>B</td> -<td><a href="index_record_C.html">C</a></td> -<td><a href="index_record_D.html">D</a></td> -<td><a href="index_record_E.html">E</a></td> -<td><a href="index_record_F.html">F</a></td> -<td><a href="index_record_G.html">G</a></td> -<td>H</td> -<td><a href="index_record_I.html">I</a></td> -<td>J</td> -<td>K</td> -<td>L</td> -<td><a href="index_record_M.html">M</a></td> -<td><a href="index_record_N.html">N</a></td> -<td>O</td> -<td><a href="index_record_P.html">P</a></td> -<td><a href="index_record_Q.html">Q</a></td> -<td><a href="index_record_R.html">R</a></td> -<td><a href="index_record_S.html">S</a></td> -<td><a href="index_record_T.html">T</a></td> -<td><a href="index_record_U.html">U</a></td> -<td><a href="index_record_V.html">V</a></td> -<td>W</td> -<td>X</td> -<td>Y</td> -<td><a href="index_record_Z.html">Z</a></td> -<td>_</td> -<td>other</td> -<td>(189 entries)</td> -</tr> -</table> -<hr/><a name="lemma_S"></a><h2>S (lemma)</h2> -<a href="mathcomp.ssreflect.fingraph.html#same_fconnect1_r">same_fconnect1_r</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#same_fconnect1">same_fconnect1</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#same_fconnect_finv">same_fconnect_finv</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#same_connect_rev">same_connect_rev</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#same_connect1r">same_connect1r</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#same_connect1">same_connect1</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#same_connect_r">same_connect_r</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#same_connect">same_connect</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#same_pblock">same_pblock</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#scalar_mx_hom">scalar_mx_hom</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mx_comm">scalar_mx_comm</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mxC">scalar_mxC</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mx_is_multiplicative">scalar_mx_is_multiplicative</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mxM">scalar_mxM</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mx_block">scalar_mx_block</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mx_is_scalar">scalar_mx_is_scalar</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mx_sum_delta">scalar_mx_sum_delta</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mx_is_additive">scalar_mx_is_additive</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalar_mx_key">scalar_mx_key</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#scalar_mx_cent">scalar_mx_cent</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemxA">scalemxA</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemxAl">scalemxAl</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemxAr">scalemxAr</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemxDl">scalemxDl</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemxDr">scalemxDr</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemx_inj">scalemx_inj</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemx_eq0">scalemx_eq0</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemx_const">scalemx_const</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemx_key">scalemx_key</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#scalemx_sub">scalemx_sub</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scalemx1">scalemx1</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#scalerMzl">scalerMzl</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#scalerMzr">scalerMzr</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#scaler_int">scaler_int</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#scalezrE">scalezrE</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.character.vcharacter.html#scale_zchar">scale_zchar</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> -<a href="mathcomp.algebra.vector.html#scale_lfunE">scale_lfunE</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scale_scalar_mx">scale_scalar_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scale_block_mx">scale_block_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scale_col_mx">scale_col_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scale_row_mx">scale_row_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.poly.html#scale_poly_eq0">scale_poly_eq0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#scale_polyAl">scale_polyAl</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#scale_polyDl">scale_polyDl</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#scale_polyDr">scale_polyDr</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#scale_1poly">scale_1poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#scale_polyA">scale_polyA</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#scale_polyE">scale_polyE</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#scale_poly_key">scale_poly_key</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.character.mxabelem.html#scale_is_groupAction">scale_is_groupAction</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.character.mxabelem.html#scale_is_action">scale_is_action</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.character.mxabelem.html#scale_actE">scale_actE</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.algebra.matrix.html#scale1mx">scale1mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.rat.html#scalqE">scalqE</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.algebra.rat.html#scalq_eq0">scalq_eq0</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.algebra.rat.html#scalq_key">scalq_key</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#scanlK">scanlK</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.tuple.html#scanl_tupleP">scanl_tupleP</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#scanl_cat">scanl_cat</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.solvable.hall.html#SchurZassenhaus_trans_actsol">SchurZassenhaus_trans_actsol</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> -<a href="mathcomp.solvable.hall.html#SchurZassenhaus_trans_sol">SchurZassenhaus_trans_sol</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> -<a href="mathcomp.solvable.hall.html#SchurZassenhaus_split">SchurZassenhaus_split</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> -<a href="mathcomp.solvable.maximal.html#SCN_max">SCN_max</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.solvable.maximal.html#SCN_abelian">SCN_abelian</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.solvable.maximal.html#SCN_P">SCN_P</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdpairE">sdpairE</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdpair_setact">sdpair_setact</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdpair_act">sdpair_act</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdpair1_morphM">sdpair1_morphM</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdpair2_morphM">sdpair2_morphM</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodE">sdprodE</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodEY">sdprodEY</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodg1">sdprodg1</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodJ">sdprodJ</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodmE">sdprodmE</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodmEl">sdprodmEl</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodmEr">sdprodmEr</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodm_eqf">sdprodm_eqf</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodm_sub">sdprodm_sub</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodm_norm">sdprodm_norm</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodP">sdprodP</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodW">sdprodW</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodWC">sdprodWC</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodWpp">sdprodWpp</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprodWY">sdprodWY</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sdprod_p'core_HallP">sdprod_p'core_HallP</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sdprod_Hall_p'coreP">sdprod_Hall_p'coreP</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sdprod_pcore_HallP">sdprod_pcore_HallP</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sdprod_Hall_pcoreP">sdprod_Hall_pcoreP</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sdprod_normal_pHallP">sdprod_normal_pHallP</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sdprod_normal_p'HallP">sdprod_normal_p'HallP</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sdprod_Hall">sdprod_Hall</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_sdpair">sdprod_sdpair</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_mulgA">sdprod_mulgA</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_mulVg">sdprod_mulVg</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_mul1g">sdprod_mul1g</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_mul_proof">sdprod_mul_proof</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_inv_proof">sdprod_inv_proof</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_recr">sdprod_recr</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_recl">sdprod_recl</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_modr">sdprod_modr</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_modl">sdprod_modl</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_subr">sdprod_subr</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_isog">sdprod_isog</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_isom">sdprod_isom</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_card">sdprod_card</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_normal_complP">sdprod_normal_complP</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_compl">sdprod_compl</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod_context">sdprod_context</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.character.character.html#sdprod_Res_IirrK">sdprod_Res_IirrK</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.character.html#sdprod_Res_IirrE">sdprod_Res_IirrE</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.character.html#sdprod_Iirr0">sdprod_Iirr0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.character.html#sdprod_Iirr_eq0">sdprod_Iirr_eq0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.character.html#sdprod_Iirr_inj">sdprod_Iirr_inj</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.character.html#sdprod_IirrK">sdprod_IirrK</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.character.html#sdprod_IirrE">sdprod_IirrE</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.classfun.html#sdprod_cfker">sdprod_cfker</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#sdprod1g">sdprod1g</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#sd1_inv">sd1_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#Sd1_inj">Sd1_inj</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#sd2_inv">sd2_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#Sd2_inj">Sd2_inj</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.fingroup.quotient.html#second_isog">second_isog</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> -<a href="mathcomp.fingroup.quotient.html#second_isom">second_isom</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> -<a href="mathcomp.character.character.html#second_orthogonality_relation">second_orthogonality_relation</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#section_eqmx">section_eqmx</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#section_eqmx_add">section_eqmx_add</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#section_module">section_module</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.solvable.jordanholder.html#section_repr_isog">section_repr_isog</a> [in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> -<a href="mathcomp.solvable.jordanholder.html#section_reprP">section_reprP</a> [in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> -<a href="mathcomp.solvable.extremal.html#semidihedral_classP">semidihedral_classP</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> -<a href="mathcomp.solvable.extremal.html#semidihedral_structure">semidihedral_structure</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiprimeJ">semiprimeJ</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiprimeS">semiprimeS</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiprime_regular">semiprime_regular</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiregularJ">semiregularJ</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiregularS">semiregularS</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiregular_prime">semiregular_prime</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiregular_sym">semiregular_sym</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiregular1l">semiregular1l</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#semiregular1r">semiregular1r</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#semisimple_Socle">semisimple_Socle</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.field.separable.html#separableP">separableP</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separablePn">separablePn</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separableS">separableS</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separableSl">separableSl</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separableSr">separableSr</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_Fadjoin_seq">separable_Fadjoin_seq</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_trans">separable_trans</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_refl">separable_refl</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_generator_maximal">separable_generator_maximal</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_generatorP">separable_generatorP</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_generator_mem">separable_generator_mem</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_inseparable_decomposition">separable_inseparable_decomposition</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_sum">separable_sum</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_add">separable_add</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_inseparable_element">separable_inseparable_element</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_exponent">separable_exponent</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_elementS">separable_elementS</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_root_der">separable_root_der</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_nz_der">separable_nz_der</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_elementP">separable_elementP</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_map">separable_map</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_prod_XsubC">separable_prod_XsubC</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_root">separable_root</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_mul">separable_mul</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_deriv_eq0">separable_deriv_eq0</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_nosquare">separable_nosquare</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_coprime">separable_coprime</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_polyP">separable_polyP</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#separable_poly_neq0">separable_poly_neq0</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.cyclotomic.html#separable_Xn_sub_1">separable_Xn_sub_1</a> [in <a href="mathcomp.field.cyclotomic.html">mathcomp.field.cyclotomic</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#seqs1">seqs1</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.field.falgebra.html#seqv_sub_adjoin">seqv_sub_adjoin</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.ssreflect.tuple.html#seq_tnthP">seq_tnthP</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#seq_ind2">seq_ind2</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.choice.html#seq_choiceMixin">seq_choiceMixin</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> -<a href="mathcomp.ssreflect.choice.html#seq_of_optK">seq_of_optK</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#seq_sub_axiom">seq_sub_axiom</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#seq_sub_pickleK">seq_sub_pickleK</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.algebra.vector.html#seq1_basis">seq1_basis</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#seq1_free">seq1_free</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.solvable.nilpotent.html#series_sol">series_sol</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> -<a href="mathcomp.fingroup.action.html#setactE">setactE</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#setactJ">setactJ</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#setactVin">setactVin</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#setact_orbit">setact_orbit</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#setact_is_action">setact_is_action</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setCD">setCD</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setCI">setCI</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setCK">setCK</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setCP">setCP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setCS">setCS</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setCT">setCT</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setCU">setCU</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setC_bigcap">setC_bigcap</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setC_bigcup">setC_bigcup</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setC_inj">setC_inj</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setC0">setC0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setC11">setC11</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDDl">setDDl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDDr">setDDr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDE">setDE</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#SetDef.finsetE">SetDef.finsetE</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#SetDef.pred_of_setE">SetDef.pred_of_setE</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDidPl">setDidPl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDIl">setDIl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDIr">setDIr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDP">setDP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDS">setDS</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDSS">setDSS</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDT">setDT</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDUl">setDUl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDUr">setDUr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setDv">setDv</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setD_eq0">setD_eq0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setD0">setD0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setD1K">setD1K</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setD1P">setD1P</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setD11">setD11</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIA">setIA</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIAC">setIAC</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIACA">setIACA</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIC">setIC</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setICA">setICA</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setICr">setICr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setID">setID</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIDA">setIDA</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIDAC">setIDAC</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIdE">setIdE</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIdP">setIdP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setId2P">setId2P</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#setIg1">setIg1</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIid">setIid</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIidPl">setIidPl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIidPr">setIidPr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIIl">setIIl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIIr">setIIr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIK">setIK</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIP">setIP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIS">setIS</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setISS">setISS</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIT">setIT</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIUl">setIUl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setIUr">setIUr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#setI_normal_Hall">setI_normal_Hall</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.gseries.html#setI_subnormal">setI_subnormal</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.center.html#setI_im_cpair">setI_im_cpair</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setI_transversal_pblock">setI_transversal_pblock</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setI_eq0">setI_eq0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setI_powerset">setI_powerset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setI0">setI0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#setI1g">setI1g</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setKI">setKI</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setKU">setKU</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setP">setP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setSD">setSD</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setSI">setSI</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setSU">setSU</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setTD">setTD</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setTI">setTI</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setTU">setTU</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUA">setUA</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUAC">setUAC</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUACA">setUACA</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUC">setUC</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUCA">setUCA</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUCr">setUCr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUid">setUid</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUidPl">setUidPl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUidPr">setUidPr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUIl">setUIl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUIr">setUIr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUK">setUK</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUP">setUP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUS">setUS</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUSS">setUSS</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUT">setUT</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUUl">setUUl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setUUr">setUUr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setU_eq0">setU_eq0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setU0">setU0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setU1K">setU1K</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setU1P">setU1P</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setU1r">setU1r</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setU11">setU11</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setXP">setXP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#setXS">setXS</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#setX_gen">setX_gen</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#setX_dprod">setX_dprod</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#setX_prod">setX_prod</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.character.integral_char.html#set_gring_classM_coef">set_gring_classM_coef</a> [in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#set_Frobenius_compl">set_Frobenius_compl</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#set_nth_default">set_nth_default</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#set_set_nth">set_set_nth</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#set_nth_nil">set_nth_nil</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#set_invgM">set_invgM</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#set_invgK">set_invgK</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#set_mulgA">set_mulgA</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#set_mul1g">set_mul1g</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set_partition_big">set_partition_big</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set_partition_big_cond">set_partition_big_cond</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set_cons">set_cons</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set_0Vmem">set_0Vmem</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set0D">set0D</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set0I">set0I</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set0Pn">set0Pn</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set0U">set0U</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#set1gE">set1gE</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#set1gP">set1gP</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set1P">set1P</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set1Ul">set1Ul</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set1Ur">set1Ur</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set1_inj">set1_inj</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set11">set11</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set2P">set2P</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set21">set21</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#set22">set22</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgrEz">sgrEz</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgrMz">sgrMz</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgrz">sgrz</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.rat.html#sgr_numq">sgr_numq</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.algebra.rat.html#sgr_numq_div">sgr_numq_div</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.algebra.rat.html#sgr_denq">sgr_denq</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.algebra.rat.html#sgr_scalq">sgr_scalq</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sgvalK">sgvalK</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sgvalM">sgvalM</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.morphism.html#sgvalmK">sgvalmK</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> -<a href="mathcomp.fingroup.morphism.html#sgval_sub">sgval_sub</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgzM">sgzM</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgzN">sgzN</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgzN1">sgzN1</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgzP">sgzP</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgzX">sgzX</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.intdiv.html#sgz_lead_primitive">sgz_lead_primitive</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/> -<a href="mathcomp.algebra.intdiv.html#sgz_contents">sgz_contents</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_eq">sgz_eq</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_smul">sgz_smul</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_le0">sgz_le0</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_ge0">sgz_ge0</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_lt0">sgz_lt0</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_gt0">sgz_gt0</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_odd">sgz_odd</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_eq0">sgz_eq0</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_cp0">sgz_cp0</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_id">sgz_id</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_int">sgz_int</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_sgr">sgz_sgr</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz_def">sgz_def</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz0">sgz0</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sgz1">sgz1</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#shape_rev">shape_rev</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.path.html#shortenP">shortenP</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#sh_inv">sh_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#Sh_inj">Sh_inj</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.algebra.rat.html#signr_scalq">signr_scalq</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.ssreflect.choice.html#sigW">sigW</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> -<a href="mathcomp.ssreflect.choice.html#sig_eqW">sig_eqW</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> -<a href="mathcomp.ssreflect.choice.html#sig2W">sig2W</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> -<a href="mathcomp.ssreflect.choice.html#sig2_eqW">sig2_eqW</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> -<a href="mathcomp.solvable.gseries.html#simpleP">simpleP</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.alt.html#simple_Alt5">simple_Alt5</a> [in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> -<a href="mathcomp.solvable.alt.html#simple_Alt5_base">simple_Alt5_base</a> [in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> -<a href="mathcomp.solvable.alt.html#simple_Alt_3">simple_Alt_3</a> [in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#simple_Socle">simple_Socle</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.solvable.jordanholder.html#simple_compsP">simple_compsP</a> [in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> -<a href="mathcomp.solvable.gseries.html#simple_maxnormal">simple_maxnormal</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.maximal.html#simple_sol_prime">simple_sol_prime</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.ssreflect.ssrbool.html#simpl_pred_sortE">simpl_pred_sortE</a> [in <a href="mathcomp.ssreflect.ssrbool.html">mathcomp.ssreflect.ssrbool</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#sizeYE">sizeYE</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#sizeY_mulX">sizeY_mulX</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#sizeY_eq0">sizeY_eq0</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.field.algC.html#size_minCpoly">size_minCpoly</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> -<a href="mathcomp.ssreflect.path.html#size_traject">size_traject</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#size_sort">size_sort</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#size_merge">size_merge</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.field.fieldext.html#size_minPoly">size_minPoly</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#size_Fadjoin_poly">size_Fadjoin_poly</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.algebra.vector.html#size_basis">size_basis</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.intdiv.html#size_rat_int_poly">size_rat_int_poly</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/> -<a href="mathcomp.algebra.intdiv.html#size_zprimitive">size_zprimitive</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/> -<a href="mathcomp.ssreflect.tuple.html#size_tuple">size_tuple</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> -<a href="mathcomp.algebra.mxpoly.html#size_mod_mxminpoly">size_mod_mxminpoly</a> [in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> -<a href="mathcomp.algebra.mxpoly.html#size_mxminpoly">size_mxminpoly</a> [in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> -<a href="mathcomp.algebra.mxpoly.html#size_char_poly">size_char_poly</a> [in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#size_poly_XmY">size_poly_XmY</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#size_poly_XaY">size_poly_XaY</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.field.cyclotomic.html#size_Cyclotomic">size_Cyclotomic</a> [in <a href="mathcomp.field.cyclotomic.html">mathcomp.field.cyclotomic</a>]<br/> -<a href="mathcomp.field.cyclotomic.html#size_cyclotomic">size_cyclotomic</a> [in <a href="mathcomp.field.cyclotomic.html">mathcomp.field.cyclotomic</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_permutations">size_permutations</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_tally_seq">size_tally_seq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_allpairs">size_allpairs</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_allpairs_dep">size_allpairs_dep</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_reshape">size_reshape</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_flatten">size_flatten</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_zip">size_zip</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_scanl">size_scanl</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_pairmap">size_pairmap</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_mkseq">size_mkseq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_iota">size_iota</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_pmap_sub">size_pmap_sub</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_pmap">size_pmap</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_map">size_map</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_rem">size_rem</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_subseq_leqif">size_subseq_leqif</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_subseq">size_subseq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_mask">size_mask</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_rotr">size_rotr</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_incr_nth">size_incr_nth</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_undup">size_undup</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_eq0">size_eq0</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_rev">size_rev</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_rot">size_rot</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_take">size_take</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_takel">size_takel</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_drop">size_drop</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_filter">size_filter</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_set_nth">size_set_nth</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_belast">size_belast</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_rcons">size_rcons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_cat">size_cat</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_nseq">size_nseq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_ncons">size_ncons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size_behead">size_behead</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.character.inertia.html#size_cfclass">size_cfclass</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/> -<a href="mathcomp.solvable.abelian.html#size_abelian_type">size_abelian_type</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#size_enum_ord">size_enum_ord</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#size_codom">size_codom</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#size_image">size_image</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_map_poly">size_map_poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_comp_poly2">size_comp_poly2</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_comp_poly">size_comp_poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_exp">size_exp</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_prod_eq1">size_prod_eq1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_prod_seq_eq1">size_prod_seq_eq1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_mul_eq1">size_mul_eq1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_prod_seq">size_prod_seq</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_prod">size_prod</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_Cmul">size_Cmul</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_scale">size_scale</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_mul">size_mul</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_comp_poly_leq">size_comp_poly_leq</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_map_polyC">size_map_polyC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_map_inj_poly">size_map_inj_poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_map_poly_id0">size_map_poly_id0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_Xn_sub_1">size_Xn_sub_1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_exp_XsubC">size_exp_XsubC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_prod_XsubC">size_prod_XsubC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_Mmonic">size_Mmonic</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_monicM">size_monicM</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_polyXn">size_polyXn</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_XmulC">size_XmulC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_mulX">size_mulX</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_MXaddC">size_MXaddC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_XaddC">size_XaddC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_XsubC">size_XsubC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_polyX">size_polyX</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_scale_leq">size_scale_leq</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_Msign">size_Msign</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_exp_leq">size_exp_leq</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_prod_leq">size_prod_leq</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_proper_mul">size_proper_mul</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_mul_leq">size_mul_leq</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly1">size_poly1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_sum">size_sum</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_addl">size_addl</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_add">size_add</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_opp">size_opp</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_polyC_leq1">size_polyC_leq1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly1P">size_poly1P</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly_gt0">size_poly_gt0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly_leq0P">size_poly_leq0P</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly_leq0">size_poly_leq0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly_eq0">size_poly_eq0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly0">size_poly0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly_eq">size_poly_eq</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_poly">size_poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_Poly">size_Poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_cons_poly">size_cons_poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#size_polyC">size_polyC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#size_orbit">size_orbit</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size0nil">size0nil</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size1_zip">size1_zip</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.algebra.poly.html#size1_polyC">size1_polyC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#size2_zip">size2_zip</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.field.falgebra.html#skew_field_dimS">skew_field_dimS</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#skew_field_module_dimS">skew_field_module_dimS</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#skew_field_module_semisimple">skew_field_module_semisimple</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#skew_field_algid1">skew_field_algid1</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.solvable.sylow.html#small_nil_class">small_nil_class</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#snd_morphM">snd_morphM</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#socleP">socleP</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#socle_rsimP">socle_rsimP</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#socle_irr">socle_irr</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#Socle_iso">Socle_iso</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#Socle_direct">Socle_direct</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#Socle_semisimple">Socle_semisimple</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#Socle_module">Socle_module</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#socle_finType_subproof">socle_finType_subproof</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#socle_mem">socle_mem</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#socle_simple">socle_simple</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#socle_exists">socle_exists</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.character.html#socle_of_Iirr_bij">socle_of_Iirr_bij</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.character.html#socle_of_IirrK">socle_of_IirrK</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.character.html#socle_Iirr0">socle_Iirr0</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.solvable.nilpotent.html#solvableS">solvableS</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> -<a href="mathcomp.character.character.html#solvable_has_lin_char">solvable_has_lin_char</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.character.inertia.html#solvable_irr_extendible_from_det">solvable_irr_extendible_from_det</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/> -<a href="mathcomp.solvable.maximal.html#solvable_norm_abelem">solvable_norm_abelem</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.solvable.nilpotent.html#solvable1">solvable1</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> -<a href="mathcomp.solvable.hall.html#sol_coprime_Sylow_subset">sol_coprime_Sylow_subset</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> -<a href="mathcomp.solvable.hall.html#sol_coprime_Sylow_trans">sol_coprime_Sylow_trans</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> -<a href="mathcomp.solvable.hall.html#sol_coprime_Sylow_exists">sol_coprime_Sylow_exists</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> -<a href="mathcomp.solvable.maximal.html#sol_prime_factor_exists">sol_prime_factor_exists</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.solvable.nilpotent.html#sol_der1_proper">sol_der1_proper</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> -<a href="mathcomp.ssreflect.ssrfun.html#Some_inj">Some_inj</a> [in <a href="mathcomp.ssreflect.ssrfun.html">mathcomp.ssreflect.ssrfun</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#sop_morph">sop_morph</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#sop_spec">sop_spec</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#sop_inj">sop_inj</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.ssreflect.path.html#sorted_le_nth">sorted_le_nth</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#sorted_lt_nth">sorted_lt_nth</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#sorted_uniq">sorted_uniq</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#sorted_filter">sorted_filter</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#sorted_divisors_ltn">sorted_divisors_ltn</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#sorted_divisors">sorted_divisors</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#sorted_primes">sorted_primes</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.path.html#sort_uniq">sort_uniq</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#sort_sorted">sort_sorted</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_bigcat">span_bigcat</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_basis">span_basis</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_cat">span_cat</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_cons">span_cons</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_seq1">span_seq1</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_nil">span_nil</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_def">span_def</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_subvP">span_subvP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#span_key">span_key</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.character.classfun.html#span_orthogonal">span_orthogonal</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#splitK">splitK</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.path.html#splitP">splitP</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#splitP">splitP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.path.html#splitPl">splitPl</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#splitPr">splitPr</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#splitP2r">splitP2r</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#splitsP">splitsP</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.field.galois.html#splittingFieldForS">splittingFieldForS</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.field.galois.html#splittingFieldP">splittingFieldP</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.field.galois.html#splittingPoly">splittingPoly</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.field.galois.html#splitting_galoisField">splitting_galoisField</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.field.galois.html#splitting_normalField">splitting_normalField</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.field.galois.html#splitting_field_normal">splitting_field_normal</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#splitting_cyclic_primitive_root">splitting_cyclic_primitive_root</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#split_subproof">split_subproof</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.algebra.zmodp.html#split1">split1</a> [in <a href="mathcomp.algebra.zmodp.html">mathcomp.algebra.zmodp</a>]<br/> -<a href="mathcomp.solvable.maximal.html#split1_extraspecial">split1_extraspecial</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#sqrnD">sqrnD</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#sqrnD_sub">sqrnD_sub</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#sqrn_inj">sqrn_inj</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#sqrn_gt0">sqrn_gt0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#sqrn_sub">sqrn_sub</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.character.classfun.html#sqrt_cfnorm_gt0">sqrt_cfnorm_gt0</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sqrt_cfnorm_eq0">sqrt_cfnorm_eq0</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sqrt_cfnorm_ge0">sqrt_cfnorm_ge0</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.field.algC.html#sqr_Cint_ge1">sqr_Cint_ge1</a> [in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#stable">stable</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.character.mxabelem.html#stable_rowg_mxK">stable_rowg_mxK</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.solvable.frobenius.html#stab_semiprime">stab_semiprime</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> -<a href="mathcomp.solvable.primitive_action.html#stab_ntransitiveI">stab_ntransitiveI</a> [in <a href="mathcomp.solvable.primitive_action.html">mathcomp.solvable.primitive_action</a>]<br/> -<a href="mathcomp.solvable.primitive_action.html#stab_ntransitive">stab_ntransitive</a> [in <a href="mathcomp.solvable.primitive_action.html">mathcomp.solvable.primitive_action</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#strict_adjunction">strict_adjunction</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.solvable.hall.html#strongest_coprime_quotient_cent">strongest_coprime_quotient_cent</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> -<a href="mathcomp.solvable.jordanholder.html#StrongJordanHolderUniqueness">StrongJordanHolderUniqueness</a> [in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> -<a href="mathcomp.field.separable.html#strong_Primitive_Element_Theorem">strong_Primitive_Element_Theorem</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.fingroup.action.html#subact_is_action">subact_is_action</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.solvable.center.html#subcentP">subcentP</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#subcent_dprod">subcent_dprod</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#subcent_sdprod">subcent_sdprod</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.fingroup.gproduct.html#subcent_TImulg">subcent_TImulg</a> [in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent_char">subcent_char</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent_normal">subcent_normal</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent_norm">subcent_norm</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent_sub">subcent_sub</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent1C">subcent1C</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent1P">subcent1P</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.maximal.html#subcent1_extraspecial_maximal">subcent1_extraspecial_maximal</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent1_cycle_normal">subcent1_cycle_normal</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent1_cycle_norm">subcent1_cycle_norm</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent1_cycle_sub">subcent1_cycle_sub</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent1_sub">subcent1_sub</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.solvable.center.html#subcent1_id">subcent1_id</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subCset">subCset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subDset">subDset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subD1set">subD1set</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subEproper">subEproper</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfield_closed">subfield_closed</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfxE">subfxE</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfxEroot">subfxEroot</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_irreducibleP">subfx_irreducibleP</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_inj_base">subfx_inj_base</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_injZ">subfx_injZ</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_inj_root">subfx_inj_root</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_inj_eval">subfx_inj_eval</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_evalZ">subfx_evalZ</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_scaleAr">subfx_scaleAr</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_scaleAl">subfx_scaleAl</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_scalerDl">subfx_scalerDl</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_scalerDr">subfx_scalerDr</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_scaler1r">subfx_scaler1r</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_scalerA">subfx_scalerA</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_eval_is_rmorphism">subfx_eval_is_rmorphism</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_inj_is_rmorphism">subfx_inj_is_rmorphism</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_inv0">subfx_inv0</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#subfx_fieldAxiom">subfx_fieldAxiom</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.fingroup.action.html#subgacentE">subgacentE</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#subgacent1E">subgacent1E</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.character.character.html#subGcfker">subGcfker</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subgK">subgK</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subgM">subgM</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.morphism.html#subgmK">subgmK</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subgP">subgP</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.action.html#subgroup_transitiveP">subgroup_transitiveP</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#subgroup_transitivePin">subgroup_transitivePin</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#subg_mx_abs_irr">subg_mx_abs_irr</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#subg_mx_irr">subg_mx_irr</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#subg_mx_faithful">subg_mx_faithful</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#subg_mx_repr">subg_mx_repr</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subg_default">subg_default</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subg_mulP">subg_mulP</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subg_invP">subg_invP</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subg_oneP">subg_oneP</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subg_inj">subg_inj</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subG1">subG1</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subG1_contra">subG1_contra</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#subHall_Sylow">subHall_Sylow</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#subHall_Hall">subHall_Hall</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subIset">subIset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.algebra.interval.html#subitvP">subitvP</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> -<a href="mathcomp.algebra.interval.html#subitvPl">subitvPl</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> -<a href="mathcomp.algebra.interval.html#subitvPr">subitvPr</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#SubK">SubK</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subKn">subKn</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#submod_mx_irr">submod_mx_irr</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#submod_mx_faithful">submod_mx_faithful</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#submod_mx_repr">submod_mx_repr</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submxE">submxE</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submxElt">submxElt</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.matrix.html#submxK">submxK</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submxMfree">submxMfree</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submxMl">submxMl</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submxMr">submxMr</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submxP">submxP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submx_full">submx_full</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submx_trans">submx_trans</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submx_refl">submx_refl</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submx_key">submx_key</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submx0">submx0</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submx0null">submx0null</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#submx1">submx1</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnAC">subnAC</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnBA">subnBA</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnDA">subnDA</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnDl">subnDl</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnDr">subnDr</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnE">subnE</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnK">subnK</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnKC">subnKC</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnn">subnn</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.solvable.gseries.html#subnormalEl">subnormalEl</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.gseries.html#subnormalEr">subnormalEr</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.gseries.html#subnormalEsupport">subnormalEsupport</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.gseries.html#subnormalP">subnormalP</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.gseries.html#subnormal_sub">subnormal_sub</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.gseries.html#subnormal_trans">subnormal_trans</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.solvable.gseries.html#subnormal_refl">subnormal_refl</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnS">subnS</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subnSK">subnSK</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.binomial.html#subn_exp">subn_exp</a> [in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subn_sqr">subn_sqr</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subn_if_gt">subn_if_gt</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subn_eq0">subn_eq0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subn_gt0">subn_gt0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subn0">subn0</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subn1">subn1</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subn2">subn2</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#SubP">SubP</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.algebra.rat.html#subq_ge0">subq_ge0</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> -<a href="mathcomp.algebra.interval.html#subr_lersif0r">subr_lersif0r</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> -<a href="mathcomp.algebra.interval.html#subr_lersifr0">subr_lersifr0</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseqP">subseqP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.path.html#subseq_sorted">subseq_sorted</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.path.html#subseq_order_path">subseq_order_path</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_uniqP">subseq_uniqP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_filter">subseq_filter</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_uniq">subseq_uniq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_rcons">subseq_rcons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_cons">subseq_cons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_trans">subseq_trans</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_refl">subseq_refl</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq0">subseq0</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetC">subsetC</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetD">subsetD</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetDl">subsetDl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetDP">subsetDP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetDr">subsetDr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetD1">subsetD1</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetD1P">subsetD1P</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subsetE">subsetE</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetI">subsetI</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetIidl">subsetIidl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetIidr">subsetIidr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetIl">subsetIl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetIP">subsetIP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetIr">subsetIr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subsetP">subsetP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subsetPn">subsetPn</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsets_disjoint">subsets_disjoint</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetT">subsetT</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetT_hint">subsetT_hint</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetU">subsetU</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetUl">subsetUl</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetUr">subsetUr</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subsetU1">subsetU1</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_disjoint">subset_disjoint</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_all">subset_all</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_trans">subset_trans</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_leqif_card">subset_leqif_card</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_cardP">subset_cardP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_eqP">subset_eqP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_pred1">subset_pred1</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_predT">subset_predT</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subset_leq_card">subset_leq_card</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.fingroup.action.html#subset_faithful">subset_faithful</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#subset_gen">subset_gen</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#subset_closure">subset_closure</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.fingraph.html#subset_dfs">subset_dfs</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subset_neq0">subset_neq0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subset_leqif_cards">subset_leqif_cards</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subset0">subset0</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subset1">subset1</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subSKn">subSKn</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subSn">subSn</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subSnn">subSnn</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#subSocle_direct">subSocle_direct</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#subSocle_iso">subSocle_iso</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#subSocle_semisimple">subSocle_semisimple</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#subSocle_module">subSocle_module</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#subSS">subSS</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subTset">subTset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subUset">subUset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#subUsetP">subUsetP</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.algebra.vector.html#subvf">subvf</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subvP">subvP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subvPn">subvPn</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.field.falgebra.html#subvP_adjoin">subvP_adjoin</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.algebra.vector.html#subvsP">subvsP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.field.fieldext.html#subvs_fieldMixin">subvs_fieldMixin</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.algebra.vector.html#subvs_vect_iso">subvs_vect_iso</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subvs_inj">subvs_inj</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.field.falgebra.html#subvs_scaleAr">subvs_scaleAr</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#subvs_scaleAl">subvs_scaleAl</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#subvs_mulDr">subvs_mulDr</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#subvs_mulDl">subvs_mulDl</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#subvs_mul1">subvs_mul1</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#subvs_mu1l">subvs_mu1l</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#subvs_mulA">subvs_mulA</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.algebra.vector.html#subvv">subvv</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subv_bigcapP">subv_bigcapP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subv_cap">subv_cap</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subv_sumP">subv_sumP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subv_add">subv_add</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subv_anti">subv_anti</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#subv_trans">subv_trans</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.field.falgebra.html#subv_adjoin_seq">subv_adjoin_seq</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#subv_adjoin">subv_adjoin</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#subv_cent1">subv_cent1</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.algebra.vector.html#subv0">subv0</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subxx">subxx</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#subxx_hint">subxx_hint</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.field.falgebra.html#subX_agenv">subX_agenv</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#subzn">subzn</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#subzSS">subzSS</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sub_pcore">sub_pcore</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sub_in_pcore">sub_in_pcore</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sub_Hall_pcore">sub_Hall_pcore</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sub_normal_Hall">sub_normal_Hall</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sub_pHall">sub_pHall</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sub_in_constt">sub_in_constt</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sub_p_elt">sub_p_elt</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#sub_pgroup">sub_pgroup</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.fingroup.quotient.html#sub_cosetpre_quo">sub_cosetpre_quo</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> -<a href="mathcomp.fingroup.quotient.html#sub_quotient_pre">sub_quotient_pre</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> -<a href="mathcomp.fingroup.quotient.html#sub_cosetpre">sub_cosetpre</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> -<a href="mathcomp.fingroup.quotient.html#sub_im_coset">sub_im_coset</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> -<a href="mathcomp.ssreflect.path.html#sub_path">sub_path</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> -<a href="mathcomp.character.vcharacter.html#sub_conjC_vchar">sub_conjC_vchar</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> -<a href="mathcomp.character.vcharacter.html#sub_aut_zchar">sub_aut_zchar</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> -<a href="mathcomp.field.fieldext.html#sub_baseField">sub_baseField</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#sub_adjoin1v">sub_adjoin1v</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#sub_pnat_coprime">sub_pnat_coprime</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#sub_in_pnat">sub_in_pnat</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#sub_in_partn">sub_in_partn</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.field.separable.html#sub_adjoin_separable_generator">sub_adjoin_separable_generator</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.separable.html#sub_inseparable">sub_inseparable</a> [in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.algebra.vector.html#sub_span">sub_span</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#sub_annihilant_neq0">sub_annihilant_neq0</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#sub_annihilantP">sub_annihilantP</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#sub_annihilant_in_ideal">sub_annihilant_in_ideal</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sub_all">sub_all</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sub_count">sub_count</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sub_has">sub_has</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sub_find">sub_find</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.character.inertia.html#sub_inertia_Ind">sub_inertia_Ind</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/> -<a href="mathcomp.character.inertia.html#sub_inertia_Res">sub_inertia_Res</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/> -<a href="mathcomp.character.inertia.html#sub_Inertia">sub_Inertia</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/> -<a href="mathcomp.character.inertia.html#sub_inertia">sub_inertia</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/> -<a href="mathcomp.solvable.abelian.html#sub_Ldiv">sub_Ldiv</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> -<a href="mathcomp.solvable.abelian.html#sub_LdivT">sub_LdivT</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#sub_ordK">sub_ordK</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#sub_ord_proof">sub_ord_proof</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#sub_enum_uniq">sub_enum_uniq</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#sub_proper_trans">sub_proper_trans</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.fingroup.action.html#sub_astabQR">sub_astabQR</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#sub_astabQ">sub_astabQ</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#sub_afixRs_norm">sub_afixRs_norm</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#sub_afixRs_norms">sub_afixRs_norms</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#sub_act_proof">sub_act_proof</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#sub_astab1">sub_astab1</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#sub_astab1_in">sub_astab1_in</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.character.classfun.html#sub_cfker_mod">sub_cfker_mod</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sub_morphim_cfker">sub_morphim_cfker</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sub_cfker_morph">sub_cfker_morph</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sub_cfker_Res">sub_cfker_Res</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sub_iso_to">sub_iso_to</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sub_orthonormal">sub_orthonormal</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sub_pairwise_orthogonal">sub_pairwise_orthogonal</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.mxabelem.html#sub_abelem_rV_im">sub_abelem_rV_im</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.character.mxabelem.html#sub_rVabelem_im">sub_rVabelem_im</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.character.mxabelem.html#sub_rVabelem">sub_rVabelem</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.character.mxabelem.html#sub_im_abelem_rV">sub_im_abelem_rV</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.character.mxabelem.html#sub_rowg_mx">sub_rowg_mx</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.solvable.commutator.html#sub_der1_abelian">sub_der1_abelian</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/> -<a href="mathcomp.solvable.commutator.html#sub_der1_normal">sub_der1_normal</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/> -<a href="mathcomp.solvable.commutator.html#sub_der1_norm">sub_der1_norm</a> [in <a href="mathcomp.solvable.commutator.html">mathcomp.solvable.commutator</a>]<br/> -<a href="mathcomp.fingroup.morphism.html#sub_isog">sub_isog</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> -<a href="mathcomp.fingroup.morphism.html#sub_isom">sub_isom</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> -<a href="mathcomp.fingroup.morphism.html#sub_morphpre_injm">sub_morphpre_injm</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> -<a href="mathcomp.fingroup.morphism.html#sub_morphpre_im">sub_morphpre_im</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> -<a href="mathcomp.fingroup.morphism.html#sub_morphim_pre">sub_morphim_pre</a> [in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_abelian_normal">sub_abelian_normal</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_abelian_norm">sub_abelian_norm</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_abelian_cent2">sub_abelian_cent2</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_abelian_cent">sub_abelian_cent</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_cent1">sub_cent1</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_gcore">sub_gcore</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_gen">sub_gen</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_class_support">sub_class_support</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_conjgV">sub_conjgV</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_conjg">sub_conjg</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_rcosetV">sub_rcosetV</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_rcoset">sub_rcoset</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_lcosetV">sub_lcosetV</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub_lcoset">sub_lcoset</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.solvable.center.html#sub_center_normal">sub_center_normal</a> [in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/> -<a href="mathcomp.field.falgebra.html#sub_agenv">sub_agenv</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.solvable.cyclic.html#sub_cyclic_char">sub_cyclic_char</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_dsumsmx">sub_dsumsmx</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_daddsmx">sub_daddsmx</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_bigcapmxP">sub_bigcapmxP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_capmx">sub_capmx</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_capmx_gen">sub_capmx_gen</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_kermxP">sub_kermxP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_sumsmxP">sub_sumsmxP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_addsmxP">sub_addsmxP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_rVP">sub_rVP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub_ltmx_trans">sub_ltmx_trans</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#sub_imset_pre">sub_imset_pre</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.solvable.sylow.html#sub_nilpotent_cent2">sub_nilpotent_cent2</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub0mx">sub0mx</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#sub0n">sub0n</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sub0seq">sub0seq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#sub0set">sub0set</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.algebra.vector.html#sub0v">sub0v</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#sub1b">sub1b</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#sub1G">sub1G</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sub1mx">sub1mx</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sub1seq">sub1seq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#sub1set">sub1set</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.field.fieldext.html#sub1v">sub1v</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.falgebra.html#sub1_agenv">sub1_agenv</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#succnK">succnK</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#succn_inj">succn_inj</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#suffix_subseq">suffix_subseq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.algebra.vector.html#sumfv">sumfv</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.matrix.html#summxE">summxE</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#summx_sub_sums">summx_sub_sums</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#summx_sub">summx_sub</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#sumMz">sumMz</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#sumnE">sumnE</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sumn_flatten">sumn_flatten</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sumn_rev">sumn_rev</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sumn_rot">sumn_rot</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sumn_rcons">sumn_rcons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sumn_count">sumn_count</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sumn_cat">sumn_cat</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#sumn_nseq">sumn_nseq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sumsmxMr">sumsmxMr</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sumsmxMr_gen">sumsmxMr_gen</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sumsmxS">sumsmxS</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#sumsmx_semisimple">sumsmx_semisimple</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#sumsmx_module">sumsmx_module</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sumsmx_subP">sumsmx_subP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#sumsmx_sup">sumsmx_sup</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.vector.html#sumv_pi_nat_sum">sumv_pi_nat_sum</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#sumv_pi_sum">sumv_pi_sum</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#sumv_pi_uniq_sum">sumv_pi_uniq_sum</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.algebra.vector.html#sumv_sup">sumv_sup</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.character.integral_char.html#sum_norm2_char_generators">sum_norm2_char_generators</a> [in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#sum_ffun">sum_ffun</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#sum_ffunE">sum_ffunE</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#sum_irr_degree">sum_irr_degree</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#sum_mxsimple_direct_sub">sum_mxsimple_direct_sub</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#sum_mxsimple_direct_compl">sum_mxsimple_direct_compl</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.algebra.vector.html#sum_lfunE">sum_lfunE</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.character.character.html#sum_norm_irr_quo">sum_norm_irr_quo</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#sum_enum_uniq">sum_enum_uniq</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.fingroup.action.html#sum_card_class">sum_card_class</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.character.classfun.html#sum_by_classes">sum_by_classes</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#sum_cfunE">sum_cfunE</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#sum_nat_eq0">sum_nat_eq0</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#sum_nat_const_nat">sum_nat_const_nat</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#sum_nat_const">sum_nat_const</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.solvable.finmodule.html#sum_index_rcosets_cycle">sum_index_rcosets_cycle</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#sum_eqE">sum_eqE</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#sum_eqP">sum_eqP</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.solvable.cyclic.html#sum_totient_dvd">sum_totient_dvd</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> -<a href="mathcomp.solvable.cyclic.html#sum_ncycle_totient">sum_ncycle_totient</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#sum_nat_cond_const">sum_nat_cond_const</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#sum1dep_card">sum1dep_card</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#sum1_size">sum1_size</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#sum1_count">sum1_count</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#sum1_card">sum1_card</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#supportE">supportE</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#supportP">supportP</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.character.vcharacter.html#support_zchar">support_zchar</a> [in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> -<a href="mathcomp.character.classfun.html#support_cfAut">support_cfAut</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#support_cfuni">support_cfuni</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#support_cfun">support_cfun</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.field.fieldext.html#sup_field_module">sup_field_module</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#svalP">svalP</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#sv_inv">sv_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#Sv_inj">Sv_inj</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXYK">swapXYK</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_map">swapXY_map</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_poly_XmY">swapXY_poly_XmY</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_poly_XaY">swapXY_poly_XaY</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_comp_poly">swapXY_comp_poly</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_is_scalable">swapXY_is_scalable</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_is_multiplicative">swapXY_is_multiplicative</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_eq0">swapXY_eq0</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_map_polyC">swapXY_map_polyC</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_is_additive">swapXY_is_additive</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_Y">swapXY_Y</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_X">swapXY_X</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_polyC">swapXY_polyC</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.polyXY.html#swapXY_key">swapXY_key</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> -<a href="mathcomp.algebra.matrix.html#swizzle_mx_is_scalable">swizzle_mx_is_scalable</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#swizzle_mx_is_additive">swizzle_mx_is_additive</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#SylowJ">SylowJ</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#SylowP">SylowP</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_subnorm">Sylow_subnorm</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_gen">Sylow_gen</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_transversal_gen">Sylow_transversal_gen</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_setI_normal">Sylow_setI_normal</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_Jsub">Sylow_Jsub</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_subJ">Sylow_subJ</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_trans">Sylow_trans</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_exists">Sylow_exists</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow_superset">Sylow_superset</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Sylow's_theorem">Sylow's_theorem</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.pgroup.html#Sylow1">Sylow1</a> [in <a href="mathcomp.solvable.pgroup.html">mathcomp.solvable.pgroup</a>]<br/> -<a href="mathcomp.algebra.mxpoly.html#Sylvester_mxE">Sylvester_mxE</a> [in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> -<a href="mathcomp.solvable.sylow.html#Syl_trans">Syl_trans</a> [in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> -<a href="mathcomp.solvable.extremal.html#symplectic_type_group_structure">symplectic_type_group_structure</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> -<a href="mathcomp.solvable.alt.html#Sym_trans">Sym_trans</a> [in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S0_inv">S0_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S05_inj">S05_inj</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S1_inv">S1_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S14_inj">S14_inj</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#s2valP">s2valP</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#s2valP'">s2valP'</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S2_inv">S2_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#s23_inv">s23_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S23_inv">S23_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S3_inv">S3_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S4_inv">S4_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S5_inv">S5_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> -<a href="mathcomp.solvable.burnside_app.html#S6_inv">S6_inv</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</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 |