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_notation_G.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/index_notation_G.html')
| -rw-r--r-- | docs/htmldoc/index_notation_G.html | 1054 |
1 files changed, 0 insertions, 1054 deletions
diff --git a/docs/htmldoc/index_notation_G.html b/docs/htmldoc/index_notation_G.html deleted file mode 100644 index 9287491..0000000 --- a/docs/htmldoc/index_notation_G.html +++ /dev/null @@ -1,1054 +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="notation_G"></a><h2>G (notation)</h2> -<a href="mathcomp.field.galois.html#834b93517c3b719105b280284d33841a">'Gal ( _ / _ ) (Group_scope)</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.field.galois.html#eb63e7cabb476068136e59e10351a997">'Gal ( _ / _ ) (group_scope)</a> [in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060">'K_ _ (ring_scope)</a> [in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#703ce4e21f8af3122d8da8159ae55c98">[ mgFun of _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa">[ mgFun by _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#09ca9041b424fb3a198e2a775c1edfdd">[ pgFun of _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#f4a0ec7c18bd128b271d4428328fd43b">[ pgFun by _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#b978f29f27d17b625bd1a96535c57314">[ gFun of _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#cecbde1597e0d77a491e8c4f94033af4">[ gFun by _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#0a3c3d64903581df0193a363279f22cc">[ igFun of _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#8dd9a311237b4fd5bc515a2cbf48517e">[ igFun by _ & ! _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.solvable.gfunctor.html#c0205c751a17b7793ccdaf02cc4999e3">[ igFun by _ & _ ] (form_scope)</a> [in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#1f39c3338430de1e4f0dd19d42cfade9">[ additive of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#9242c465b1ba475eb872a4f54d4904f7">[ additive of _ as _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#b15d1bebaaff5b5ed693647b6d36f348">{ additive _ } (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#205d21d03e723fd656efd69d615cdfd2">[ algType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#93568324863779f91a1c79d8a55f7d2b">[ algType _ of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#4fcb7e9ad725fb7730e1c5fbb1867235">[ closedFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#7337068ceeff2a313d9f8cc737452bc8">[ closedFieldType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d">[ comRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#10459c1b5042aa99a4ad9b14b5d55ba2">[ comRingType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc">[ comUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#e40d136c069cdf352d78bc69141aeefa">[ decFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#29a9c5427a3ebd772d1548a40a20219d">[ decFieldType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#ad32e01476f8d2c74998482c543d7f39">[ rec _ , _ ]</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2">[ fieldType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#47ab34bf5497a33543a0c8593815a525">[ fieldType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de">[ idomainType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#d2f06a45025b5a16ce20033996a7b507">[ idomainType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#c3932ab7d4b1953f142288e718bebbc4">[ lalgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#ac25e41f1dd8deef399bcb0123249366">[ lalgType _ of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#6190fe21ffbd3dab252b4f744e9e9c11">[ linear of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#207c4f83c4cbc5a63a51367b095e08b4">[ linear of _ as _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#09fcb2ff53297f611c9440c05c397a76">_ *^ _ _ (linear_ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#34bba9fc83736a2ae54eedc9403c7ffa">_ *:^ _ _ (linear_ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#751e095f871b75182d9f960cbc38311e">_ * _ (linear_ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#18d5a37ddb86b27d9a3e716fcbda4ee7">_ *: _ (linear_ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#46175849544ed868533ead6f2ac4a179">{ scalar _ } (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#b9a9030f88e15d1a3aacd4e8ec9a2391">{ linear _ } (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#aabc8eba9c2cbefac5d796739c9a54bd">{ linear _ | _ } (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#30f6d8f9ddb331fb2136ef9c13244e1c">*:%R</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#f564c8972b813e490c7ba0cd5a233f85">[ lmodType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#69479875cda47ffe3dea9a209ad2d298">[ lmodType _ of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566">[ lrmorphism of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#c998d6ecd14e902f7fd2311ac585dfed">{ lrmorphism _ } (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#be490f36b8d971894ee8495ffc283566">{ lrmorphism _ | _ } (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#0a9ddc310d4a9a62484de48da8431046">_ ^f</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071">[ ringType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#ecf0b15322b67c769ef6213b9b1c1517">[ ringType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#f59994a9f1c6ff43f3de0a3cea89bb6b">[ rmorphism of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#5038fd6baf0faad94b37e6421e96b65c">[ rmorphism of _ as _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5">{ rmorphism _ } (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#83cca6b725db9972b036f288f094080c">[ fieldMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#5b251e8f030769055bfe05ad2f695eba">[ idomainMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#b301713c2aba0b85ce0f12fd24d9fa6c">[ unitRingMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#26e6b9f0e308a1d93a5b9cc3600f1f94">[ algMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#4c5a69764ef57db08f25bb13c5922bb9">[ comRingMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#9aac47d9eeb1b3e6d5a5febc761ef694">[ lalgMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#38b3ea7fc6d29c65cc1ec0b680489dc7">[ lmodMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#f625c62aceb0354308865d5dd53ab01f">[ ringMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#f379225ec8dfc5d660cf07deb0b2efb4">[ zmodMixin of _ by <: ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#53130370ad22aac4f3ee8434dbc4850d">[ unitAlgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e">[ unitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#76902b774c7fc1cb3d8cfbe482949a53">[ unitRingType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac">[ zmodType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#39c4486aeb13eba38054a2f7092a4a46">[ zmodType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#fc74b441e09df14f29dadaaae6a85505">_ \o* _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#bc3112e15c615abd16fe817a85e6c0fd">_ \*o _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#4f2c8844bdca193370eeb7e4ed6c690a">_ \*: _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#8934e834fc8aae356ef1d8f2b3bd03ed">_ \- _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#e2061ffc5a4c809cf18bbafb8211e59f">_ \+ _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#2fadffc111e97bfa2ac21311dff6237b">\0 (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#b328a5aed2733481ae9bfe9f2b7cc645">_ %:A (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#10f331d2d40399852634935b8aa18b88">_ *: _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#7cf08e2f41bbb95903802050d3919698">[ char _ ] (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#a1ff23c95130eb62e8ce3bc8a42b5e38">_ ^+ _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#f99a2dc6d143aa8f1021ab57e4a19eee">_ * _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#512a31305e556a90e0ad0550ee623cbc">_ %:R (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#f51fd4f778bf0ac24a682f5e5bb9e825">- 1 (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#64d179658494c6d58eedb3b196ceab5a">1 (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#ba78b96b099a9672a88803cbbfa90ebc">_ `_ _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#0c0f4a48fca1c1f27e9d71f54b6b8bd3">_ *- _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#506f68330939db1f655609b68b37b467">_ *+ _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#4a5fc7f0d0a33bc3822357a38c953c9e">_ - _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#730bbb3cf1092122fa1a208d3879e5e8">_ + _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#89db507031b6d4a3d916a0f1c8eeaac2">+%R (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#aa58dfcfb323e1f070c38e31f9efddbe">- _ (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#f6c07ffdcee3462925d63c623b06b027">-%R (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#a4731bf93645db2d12d8aa577c913a83">0 (ring_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#662c07b5d0726d21c8edce4d5fbaa087">'forall 'X_ _ , _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#3a3c189a0c88aa572171a0bae2912beb">'exists 'X_ _ , _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#0097d74fdc44ca768502e9edebe7e195">_ != _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#8fd8345f0bd0f50ba5171cc7c1b45aca">~ _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#33d69901017412abb2c3513a87e991c1">_ ==> _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#bef44b50d3f3917949ecad5e3e01309c">_ \/ _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#ab32bd0aebe6dabd4efe45ce35759537">_ /\ _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#e6bce7853a73484fa8c54c3b3d0fe8f6">_ == _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#d56cb9de8d42b54fdfaa24a15d81424e">_ ^+ _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#1d3f5aaba0b5415b38ef086fecc784cc">_ / _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#ae816e3b24c797f519ce51141978e695">_ ^-1 (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#74b863100f00ebe6b6a91299397f9af3">_ *+ _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#a9e0394c049f1992b539cb7717095281">_ * _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#cb78c0285370423798e088d285c922f5">_ - _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#e2d8b10a7f82d8520cd39f5ef78702a0">- _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#dbf4583bf7f5ea301319678efa885505">_ + _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#eb428fcfecf865b66549cce36cfaa418">1 (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#97dbe2955d24055fd83c970067919944">0 (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#a4e52005e26c4b25ab5e860f94c039f7">_ %:T (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#8f212249fc4cb1d481e8d42f00523dbd">_ %:R (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#2d5cc450d76596e00ba9d438af4e1dc5">'X_ _ (term_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#44117511dc5f0eff9d2bcbcfcdd33874">_ ^o (type_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#a5048fbb5749bbf342aa41d2111c50c8">_ ^c (type_scope)</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#1e3664ff5a0845564dcf20fcc71a269d">_ ^- _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#705c00ff5a03bf84d6828df21a7a7942">_ / _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#139f286ff80df5d41ea22851b1826860">_ ^-1</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#bae191a5c954d16cccd67244cf8a6ceb">*%R</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#38480d07e3193b4bc897687500c6bc9c">*:%R</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#483796999382d9671d4ef0e14aab5328">\prod_ ( _ <= _ < _ ) _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#ffaead03d6bc40b2e0dc2c448b2f18da">\prod_ ( _ in _ ) _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#ba1581e43a210b25c8f779050e03b92e">\prod_ ( _ | _ ) _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#5e0b538209a51fa2bd900767b9312dd8">\prod_ ( _ <- _ | _ ) _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#3f77cb0ecca797dabe8a89fee7b1337b">\sum_ ( _ in _ ) _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#2212b29e1a046120b3e8fdf5f4fbcd1f">\sum_ ( _ < _ ) _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#b6b1fbfe788a2b1990c0d8b2548df5eb">\sum_ ( _ <= _ < _ ) _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.algebra.ssralg.html#dcb91d0b08ece8369cc6084787184d13">\sum_ ( _ <- _ | _ ) _</a> [in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</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 |