diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_global_M.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_M.html')
| -rw-r--r-- | docs/htmldoc/index_global_M.html | 192 |
1 files changed, 120 insertions, 72 deletions
diff --git a/docs/htmldoc/index_global_M.html b/docs/htmldoc/index_global_M.html index bf4aaf2..18c6494 100644 --- a/docs/htmldoc/index_global_M.html +++ b/docs/htmldoc/index_global_M.html @@ -4,7 +4,7 @@ <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.ssreflect.tuple</title> +<title>mathcomp.test_suite.hierarchy_test</title> </head> <body> @@ -47,7 +47,7 @@ <td><a href="index_global_Z.html">Z</a></td> <td>_</td> <td><a href="index_global_*.html">other</a></td> -<td>(23233 entries)</td> +<td>(23836 entries)</td> </tr> <tr> <td>Notation Index</td> @@ -79,14 +79,14 @@ <td><a href="index_notation_Z.html">Z</a></td> <td>_</td> <td><a href="index_notation_*.html">other</a></td> -<td>(1373 entries)</td> +<td>(1409 entries)</td> </tr> <tr> <td>Module Index</td> <td><a href="index_module_A.html">A</a></td> <td><a href="index_module_B.html">B</a></td> <td><a href="index_module_C.html">C</a></td> -<td>D</td> +<td><a href="index_module_D.html">D</a></td> <td><a href="index_module_E.html">E</a></td> <td><a href="index_module_F.html">F</a></td> <td><a href="index_module_G.html">G</a></td> @@ -111,7 +111,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -143,7 +143,7 @@ <td><a href="index_variable_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3475 entries)</td> +<td>(3574 entries)</td> </tr> <tr> <td>Library Index</td> @@ -175,7 +175,7 @@ <td><a href="index_library_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(89 entries)</td> +<td>(90 entries)</td> </tr> <tr> <td>Lemma Index</td> @@ -207,7 +207,7 @@ <td><a href="index_lemma_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(11853 entries)</td> +<td>(12096 entries)</td> </tr> <tr> <td>Constructor Index</td> @@ -239,7 +239,7 @@ <td><a href="index_constructor_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(359 entries)</td> +<td>(368 entries)</td> </tr> <tr> <td>Axiom Index</td> @@ -271,7 +271,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -303,14 +303,14 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(103 entries)</td> +<td>(107 entries)</td> </tr> <tr> <td>Projection Index</td> <td><a href="index_projection_A.html">A</a></td> <td><a href="index_projection_B.html">B</a></td> <td><a href="index_projection_C.html">C</a></td> -<td>D</td> +<td><a href="index_projection_D.html">D</a></td> <td><a href="index_projection_E.html">E</a></td> <td><a href="index_projection_F.html">F</a></td> <td><a href="index_projection_G.html">G</a></td> @@ -335,7 +335,7 @@ <td><a href="index_projection_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(266 entries)</td> +<td>(273 entries)</td> </tr> <tr> <td>Section Index</td> @@ -367,7 +367,7 @@ <td><a href="index_section_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(1118 entries)</td> +<td>(1140 entries)</td> </tr> <tr> <td>Abbreviation Index</td> @@ -399,7 +399,7 @@ <td><a href="index_abbreviation_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(691 entries)</td> +<td>(728 entries)</td> </tr> <tr> <td>Definition Index</td> @@ -431,14 +431,14 @@ <td><a href="index_definition_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3461 entries)</td> +<td>(3596 entries)</td> </tr> <tr> <td>Record Index</td> <td><a href="index_record_A.html">A</a></td> <td>B</td> <td><a href="index_record_C.html">C</a></td> -<td>D</td> +<td><a href="index_record_D.html">D</a></td> <td><a href="index_record_E.html">E</a></td> <td><a href="index_record_F.html">F</a></td> <td><a href="index_record_G.html">G</a></td> @@ -463,7 +463,7 @@ <td><a href="index_record_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(185 entries)</td> +<td>(189 entries)</td> </tr> </table> <hr/><a name="global_M"></a><h2>M </h2> @@ -496,7 +496,7 @@ <a href="mathcomp.algebra.mxpoly.html#MapComRing.f">MapComRing.f</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapComRing.n'">MapComRing.n'</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapComRing.rR">MapComRing.rR</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> -<a href="mathcomp.algebra.mxpoly.html#434323eabd83251a96adefe7e9c505c5">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> +<a href="mathcomp.algebra.mxpoly.html#e4e440bd0e6055cffe6740e4a836968e">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.ssreflect.path.html#MapEqPath">MapEqPath</a> [section, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#MapEqPath.e">MapEqPath.e</a> [variable, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#MapEqPath.e'">MapEqPath.e'</a> [variable, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> @@ -509,25 +509,26 @@ <a href="mathcomp.algebra.matrix.html#MapFieldMatrix.aF">MapFieldMatrix.aF</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapFieldMatrix.f">MapFieldMatrix.f</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapFieldMatrix.rF">MapFieldMatrix.rF</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#f87866ba8cd1624e1947136fd0b7ea04">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#9d3374d589a13133fdaed07caecf4d33">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.poly.html#MapFieldPoly">MapFieldPoly</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapFieldPoly.f">MapFieldPoly.f</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapFieldPoly.F">MapFieldPoly.F</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapFieldPoly.R">MapFieldPoly.R</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#6808a1f3c4c980ac2ccb289ca5e44206">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#972c6bc88e7a669e15352d4d2f4bf8cb">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapField.A">MapField.A</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapField.aF">MapField.aF</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapField.f">MapField.f</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapField.n'">MapField.n'</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> +<a href="mathcomp.algebra.mxpoly.html#MapField.p">MapField.p</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapField.rF">MapField.rF</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> -<a href="mathcomp.algebra.mxpoly.html#041fb544cfc5686d5af02f919429c54f">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> +<a href="mathcomp.algebra.mxpoly.html#5f1925a9c24ff4e03a5528db5ad9eddc">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mapK">mapK</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapMatrix">MapMatrix</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#MapMatrixSpaces">MapMatrixSpaces</a> [section, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#MapMatrixSpaces.aF">MapMatrixSpaces.aF</a> [variable, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#MapMatrixSpaces.f">MapMatrixSpaces.f</a> [variable, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#MapMatrixSpaces.rF">MapMatrixSpaces.rF</a> [variable, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#b131265909f3a801cb4367eec910d732">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> +<a href="mathcomp.algebra.mxalgebra.html#64a7caee0a3cf4d848aa409baa5e70f5">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapMatrix.aT">MapMatrix.aT</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapMatrix.Block">MapMatrix.Block</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapMatrix.Block.Adl">MapMatrix.Block.Adl</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> @@ -547,7 +548,7 @@ <a href="mathcomp.algebra.matrix.html#MapMatrix.OneMatrix.m">MapMatrix.OneMatrix.m</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapMatrix.OneMatrix.n">MapMatrix.OneMatrix.n</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapMatrix.rT">MapMatrix.rT</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#b445d3501620da3b306ed068f7c864a7">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#d36c85c08e6bc06a03a0af528e062f26">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.field.fieldext.html#MapMinPoly">MapMinPoly</a> [section, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#MapMinPoly.f">MapMinPoly.f</a> [variable, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#MapMinPoly.F0">MapMinPoly.F0</a> [variable, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> @@ -570,14 +571,14 @@ <a href="mathcomp.algebra.poly.html#MapPoly.Additive">MapPoly.Additive</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Additive.f">MapPoly.Additive.f</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Additive.iR">MapPoly.Additive.iR</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#7d2b3e616181246d58c271ab24bc9d56">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#f96de40aa5b46ab228915f8026ade3b8">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.aR">MapPoly.aR</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Combinatorial">MapPoly.Combinatorial</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Combinatorial.f">MapPoly.Combinatorial.f</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Combinatorial.f_0">MapPoly.Combinatorial.f_0</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Combinatorial.inj_f">MapPoly.Combinatorial.inj_f</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Combinatorial.iR">MapPoly.Combinatorial.iR</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#655a5cbe5192b668144a8107711db834">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#77bee8efe57fbb5773ae6e32ab3a0709">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Definitions">MapPoly.Definitions</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Definitions.aR">MapPoly.Definitions.aR</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.Definitions.f">MapPoly.Definitions.f</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -587,7 +588,7 @@ <a href="mathcomp.algebra.poly.html#MapPoly.HornerMorph.cfu">MapPoly.HornerMorph.cfu</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.HornerMorph.u">MapPoly.HornerMorph.u</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#MapPoly.rR">MapPoly.rR</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#b0a4b98f65b912dc010655ba49aed12f">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#08484e31d7e3ec6a6712aaeb95848c94">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapResultant">MapResultant</a> [section, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapRingMatrix">MapRingMatrix</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapRingMatrix">MapRingMatrix</a> [section, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> @@ -604,15 +605,15 @@ <a href="mathcomp.algebra.mxpoly.html#MapRingMatrix.n">MapRingMatrix.n</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapRingMatrix.rR">MapRingMatrix.rR</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#MapRingMatrix.rR">MapRingMatrix.rR</a> [variable, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> -<a href="mathcomp.algebra.matrix.html#9f6c421a139de435ca847198e46df8c0">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.mxpoly.html#9f6c421a139de435ca847198e46df8c0">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> +<a href="mathcomp.algebra.matrix.html#9ade10a0869c3a521d87ab9890c112dd">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.mxpoly.html#9ade10a0869c3a521d87ab9890c112dd">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapZmodMatrix">MapZmodMatrix</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapZmodMatrix.aR">MapZmodMatrix.aR</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapZmodMatrix.f">MapZmodMatrix.f</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapZmodMatrix.m">MapZmodMatrix.m</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapZmodMatrix.n">MapZmodMatrix.n</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MapZmodMatrix.rR">MapZmodMatrix.rR</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#479b17b45199ea1ed1c4afe064416af1">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#76b5aeafe828ce631ffccd8f78f059ea">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.ssreflect.path.html#map_path">map_path</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.character.vcharacter.html#map_orthonormal">map_orthonormal</a> [lemma, in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> <a href="mathcomp.character.vcharacter.html#map_pairwise_orthogonal">map_pairwise_orthogonal</a> [lemma, in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> @@ -691,6 +692,7 @@ <a href="mathcomp.algebra.matrix.html#map_mx">map_mx</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#map_mx_key">map_mx_key</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#map_mx_inv_horner">map_mx_inv_horner</a> [lemma, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> +<a href="mathcomp.algebra.mxpoly.html#map_mx_companion">map_mx_companion</a> [lemma, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#map_horner_mx">map_horner_mx</a> [lemma, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#map_powers_mx">map_powers_mx</a> [lemma, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#map_resultant">map_resultant</a> [lemma, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> @@ -701,6 +703,7 @@ <a href="mathcomp.algebra.polyXY.html#map_div_annihilantP">map_div_annihilantP</a> [lemma, in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.algebra.polyXY.html#map_sub_annihilantP">map_sub_annihilantP</a> [lemma, in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.field.algnum.html#map_Qnum_poly">map_Qnum_poly</a> [lemma, in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#map_allpairs">map_allpairs</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#map_reshape">map_reshape</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#map_flatten">map_flatten</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#map_pK">map_pK</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -824,21 +827,21 @@ <a href="mathcomp.algebra.matrix.html#MatrixAlgebra.RingModule">MatrixAlgebra.RingModule</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixAlgebra.RingModule.m">MatrixAlgebra.RingModule.m</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixAlgebra.RingModule.n">MatrixAlgebra.RingModule.n</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#9f61d450b1c16584e53d42e9b80b7e9e">_ *m: _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#9debb1fd6a4126e6680903c55c018a93">_ *m: _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixAlgebra.ScalarMx">MatrixAlgebra.ScalarMx</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixAlgebra.ScalarMx.n">MatrixAlgebra.ScalarMx.n</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#7e0a687e8b3ecbe9dc390072328f2a02">_ %:M (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#7e03ba8094ca395d410e19b2de7bc7f0">_ %:M (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixAlgebra.StructuralLinear">MatrixAlgebra.StructuralLinear</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixAlgebra.Trace">MatrixAlgebra.Trace</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixAlgebra.Trace.n">MatrixAlgebra.Trace.n</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#dddd04618622462b0f6d04a328c9ed37">\tr _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#9fdeed72b47a12f54ffaf8faf3f4e8a4">'Z ( _ ) (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#6f6a817e8af480225304556c4b1a37bc">'C ( _ ) (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#fd554c34965aa6852b3a09f211aef8b0">_ * _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.algebra.matrix.html#96a53c40395815f168804b3e9251775e">\tr _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#214a0bf07a0a0de5c6aebf03e1f2a5c7">_ *m _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#f0439935524a049a771823d6a7a44496">_ %:M (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.mxalgebra.html#002b20fea7ea6146f072b539b8de9620">_ \in _</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> +<a href="mathcomp.algebra.matrix.html#4a3574d5d59f5b06ea258779cba9ae4a">\tr _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.mxalgebra.html#59d3f372b35ea6f62351d739453bd3ac">'Z ( _ ) (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> +<a href="mathcomp.algebra.mxalgebra.html#5580b74451c106276b6637b4c3d0e16a">'C ( _ ) (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> +<a href="mathcomp.algebra.mxalgebra.html#90d438ddb283d0b7a7b8496794bbb81b">_ * _ (matrix_set_scope)</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> +<a href="mathcomp.algebra.matrix.html#18306fb4f25d05e26085dcdbda0e43a4">\tr _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#94b466ee24f49d7e561171fc23a36c8d">_ *m _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#71bd40847c76c3652311fa22e057bab2">_ %:M (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.mxalgebra.html#7aed6abca956bf1cb53b7f7024bbdd8c">_ \in _</a> [notation, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixDef">MatrixDef</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixDef.m">MatrixDef.m</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixDef.n">MatrixDef.n</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> @@ -938,9 +941,9 @@ <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField">MatrixGenField.GenField</a> [section, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.A">MatrixGenField.GenField.A</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.Bijection">MatrixGenField.GenField.Bijection</a> [section, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.Bijection.m1">MatrixGenField.GenField.Bijection.m1</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.Bijection.m">MatrixGenField.GenField.Bijection.m</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.Bijection2">MatrixGenField.GenField.Bijection2</a> [section, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.Bijection2.m1">MatrixGenField.GenField.Bijection2.m1</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.Bijection2.m">MatrixGenField.GenField.Bijection2.m</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.cGA">MatrixGenField.GenField.cGA</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.d_gt0">MatrixGenField.GenField.d_gt0</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.GenField.F">MatrixGenField.GenField.F</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -1007,7 +1010,6 @@ <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.in_genK">MatrixGenField.in_genK</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.in_gen">MatrixGenField.in_gen</a> [definition, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.irr">MatrixGenField.irr</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#MatrixGenField.m">MatrixGenField.m</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.map_mxminpoly_groot">MatrixGenField.map_mxminpoly_groot</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.morphAnd">MatrixGenField.morphAnd</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.mxmodule_rowval_gen">MatrixGenField.mxmodule_rowval_gen</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -1031,6 +1033,7 @@ <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.n">MatrixGenField.n</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.n">MatrixGenField.n</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.n">MatrixGenField.n</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#MatrixGenField.nA">MatrixGenField.nA</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.non_linear_gen_reducible">MatrixGenField.non_linear_gen_reducible</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.nth_map_rVval">MatrixGenField.nth_map_rVval</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#MatrixGenField.pA">MatrixGenField.pA</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -1114,7 +1117,7 @@ <a href="mathcomp.algebra.matrix.html#MatrixStructural.VecMatrix">MatrixStructural.VecMatrix</a> [section, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixStructural.VecMatrix.m">MatrixStructural.VecMatrix.m</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#MatrixStructural.VecMatrix.n">MatrixStructural.VecMatrix.n</a> [variable, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> -<a href="mathcomp.algebra.matrix.html#445ad0600a9fd3b438aa099d79ca3f3a">_ ^T (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#82d06d97ea622769b781f4bb9951aa48">_ ^T (ring_scope)</a> [notation, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.vector.html#MatrixVectType">MatrixVectType</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#MatrixVectType.m">MatrixVectType.m</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#MatrixVectType.n">MatrixVectType.n</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> @@ -1324,11 +1327,14 @@ <a href="mathcomp.field.algnum.html#mem_Cint_span">mem_Cint_span</a> [lemma, in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/> <a href="mathcomp.field.algnum.html#mem_Crat_span">mem_Crat_span</a> [lemma, in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/> <a href="mathcomp.character.character.html#mem_irr">mem_irr</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#mem_permutations">mem_permutations</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_allpairs">mem_allpairs</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#mem_allpairs_dep">mem_allpairs_dep</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_iota">mem_iota</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_pmap_sub">mem_pmap_sub</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_pmap">mem_pmap</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_map">mem_map</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#mem_rem_uniqF">mem_rem_uniqF</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_rem_uniq">mem_rem_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_rem">mem_rem</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_subseq">mem_subseq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1338,6 +1344,7 @@ <a href="mathcomp.ssreflect.seq.html#mem_rotr">mem_rotr</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_rot">mem_rot</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_undup">mem_undup</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#mem_nseq">mem_nseq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_rev">mem_rev</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_filter">mem_filter</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#mem_drop">mem_drop</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1665,19 +1672,42 @@ <a href="mathcomp.algebra.poly.html#monic_neq0">monic_neq0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#monic_key">monic_key</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#monic1">monic1</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory">MonoHomoTheory</a> [section, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.aR">MonoHomoTheory.aR</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.aRE">MonoHomoTheory.aRE</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.aR_anti">MonoHomoTheory.aR_anti</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.aR_refl">MonoHomoTheory.aR_refl</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.aR'">MonoHomoTheory.aR'</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.aR'E">MonoHomoTheory.aR'E</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.aT">MonoHomoTheory.aT</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.D">MonoHomoTheory.D</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.f">MonoHomoTheory.f</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.InDom">MonoHomoTheory.InDom</a> [section, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.InDom.aR_anti">MonoHomoTheory.InDom.aR_anti</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.InDom.D">MonoHomoTheory.InDom.D</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.InDom.DifferentDom">MonoHomoTheory.InDom.DifferentDom</a> [section, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.InDom.DifferentDom.D'">MonoHomoTheory.InDom.DifferentDom.D'</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.InDom.rR_anti">MonoHomoTheory.InDom.rR_anti</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.rR">MonoHomoTheory.rR</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.rRE">MonoHomoTheory.rRE</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.rR_anti">MonoHomoTheory.rR_anti</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.rR_refl">MonoHomoTheory.rR_refl</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.rR'">MonoHomoTheory.rR'</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.rR'E">MonoHomoTheory.rR'E</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#MonoHomoTheory.rT">MonoHomoTheory.rT</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid">Monoid</a> [module, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#MonoidProperties">MonoidProperties</a> [section, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#MonoidProperties.Abelian">MonoidProperties.Abelian</a> [section, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#MonoidProperties.Abelian.op">MonoidProperties.Abelian.op</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#b25ccbc213967b87d966fdb2702413fa">_ * _</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#c82197763a0dd496120819d8f365a45e">*%M</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#fa96cf288c7d631ec59b7d16f33878eb">_ * _</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#4461abbe51a521b546e6aa0e9d87a0f5">*%M</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#MonoidProperties.idx">MonoidProperties.idx</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#MonoidProperties.Plain">MonoidProperties.Plain</a> [section, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#MonoidProperties.Plain.op">MonoidProperties.Plain.op</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#1888fbf7456ea9b1e55b1a456f115da0">_ * _</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#a2acafd8daeae4104c6aac163f1a7c52">*%M</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#d3310823c977c18402e087052356682e">_ * _</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#fc6b31eb5a9c190f3c69acfe152eb8da">*%M</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#MonoidProperties.R">MonoidProperties.R</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#0c654cf4cb20c966a96e17bafbe8e47c">1</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#28f7764b62e7a7fd835da7bb8c5c2e26">1</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid.AddLaw">Monoid.AddLaw</a> [constructor, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid.add_operator">Monoid.add_operator</a> [projection, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid.add_law">Monoid.add_law</a> [record, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> @@ -1701,10 +1731,10 @@ <a href="mathcomp.ssreflect.bigop.html#Monoid.Definitions.op_id">Monoid.Definitions.op_id</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid.Definitions.T">Monoid.Definitions.T</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid.Exports">Monoid.Exports</a> [module, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#3759935094ad0adf0adc03d4027e4a9d">[ add_law _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#6a17f9cab4f53335e165dca6c368f81a">[ mul_law of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#f01f35dc12f1fe626d93029e6534fbf3">[ com_law of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#63ca36d66d47ad202886c7c65c88c378">[ law of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#9817ef3828fb82ac1e3d0b86f80b4caa">[ add_law _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#c8301b47409c0354edf11a5fa45f684e">[ mul_law of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#f6879cc6b2f76829a745ea8ba8f8ac82">[ com_law of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#c0ead7c536b771c2de27837c46f4d177">[ law of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid.law">Monoid.law</a> [record, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid.Law">Monoid.Law</a> [constructor, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Monoid.mulC_dist">Monoid.mulC_dist</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> @@ -1752,7 +1782,25 @@ <a href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F2">MonotonicFunctorTheory.Composition.F2</a> [variable, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> <a href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.F1">MonotonicFunctorTheory.F1</a> [variable, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> <a href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.F2">MonotonicFunctorTheory.F2</a> [variable, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> +<a href="mathcomp.ssreflect.path.html#Monotonicity">Monotonicity</a> [section, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity">Monotonicity</a> [section, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat">Monotonicity.NatToNat</a> [section, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat.anti_geq">Monotonicity.NatToNat.anti_geq</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat.anti_leq">Monotonicity.NatToNat.anti_leq</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat.D">Monotonicity.NatToNat.D</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat.D'">Monotonicity.NatToNat.D'</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat.f">Monotonicity.NatToNat.f</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat.gtn_neqAge">Monotonicity.NatToNat.gtn_neqAge</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat.leq_total">Monotonicity.NatToNat.leq_total</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.NatToNat.ltn_neqAle">Monotonicity.NatToNat.ltn_neqAle</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.path.html#Monotonicity.r">Monotonicity.r</a> [variable, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> +<a href="mathcomp.ssreflect.path.html#Monotonicity.r_refl">Monotonicity.r_refl</a> [variable, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> +<a href="mathcomp.ssreflect.path.html#Monotonicity.r_trans">Monotonicity.r_trans</a> [variable, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> +<a href="mathcomp.ssreflect.path.html#Monotonicity.T">Monotonicity.T</a> [variable, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#Monotonicity.T">Monotonicity.T</a> [variable, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#mono_leqif">mono_leqif</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#mono_inj">mono_inj</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#mono_inj_in">mono_inj_in</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.field.algnum.html#MoreAlgCaut">MoreAlgCaut</a> [section, in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/> <a href="mathcomp.character.character.html#MoreConstt">MoreConstt</a> [section, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> <a href="mathcomp.character.character.html#MoreConstt.G">MoreConstt.G</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> @@ -2185,7 +2233,7 @@ <a href="mathcomp.algebra.ssrint.html#MorphTheory.Frobenius.charFp">MorphTheory.Frobenius.charFp</a> [variable, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.ssrint.html#MorphTheory.Frobenius.p">MorphTheory.Frobenius.p</a> [variable, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.ssrint.html#MorphTheory.Frobenius.R">MorphTheory.Frobenius.R</a> [variable, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> -<a href="mathcomp.algebra.ssrint.html#e0d2a01f79c224eaeeb036c69b97e850">_ ^f</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> +<a href="mathcomp.algebra.ssrint.html#053621076ed59ad170ac70a08190d12e">_ ^f</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.ssrint.html#MorphTheory.Linear">MorphTheory.Linear</a> [section, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.ssrint.html#MorphTheory.Linear.f">MorphTheory.Linear.f</a> [variable, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.ssrint.html#MorphTheory.Linear.R">MorphTheory.Linear.R</a> [variable, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> @@ -2297,6 +2345,7 @@ <a href="mathcomp.algebra.matrix.html#mulmx_sumr">mulmx_sumr</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#mulmx_suml">mulmx_suml</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#mulmx_key">mulmx_key</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.mxpoly.html#mulmx_delta_companion">mulmx_delta_companion</a> [lemma, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#mulmx_ker">mulmx_ker</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#mulmx_sub">mulmx_sub</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#mulmx_coker">mulmx_coker</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> @@ -2350,7 +2399,6 @@ <a href="mathcomp.ssreflect.ssrnat.html#muln0">muln0</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#muln1">muln1</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#muln2">muln2</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.field.closed_field.html#mulpT">mulpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.algebra.ssrint.html#mulpz">mulpz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.rat.html#mulq">mulq</a> [definition, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> <a href="mathcomp.algebra.rat.html#mulqA">mulqA</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> @@ -2761,7 +2809,7 @@ <td><a href="index_global_Z.html">Z</a></td> <td>_</td> <td><a href="index_global_*.html">other</a></td> -<td>(23233 entries)</td> +<td>(23836 entries)</td> </tr> <tr> <td>Notation Index</td> @@ -2793,14 +2841,14 @@ <td><a href="index_notation_Z.html">Z</a></td> <td>_</td> <td><a href="index_notation_*.html">other</a></td> -<td>(1373 entries)</td> +<td>(1409 entries)</td> </tr> <tr> <td>Module Index</td> <td><a href="index_module_A.html">A</a></td> <td><a href="index_module_B.html">B</a></td> <td><a href="index_module_C.html">C</a></td> -<td>D</td> +<td><a href="index_module_D.html">D</a></td> <td><a href="index_module_E.html">E</a></td> <td><a href="index_module_F.html">F</a></td> <td><a href="index_module_G.html">G</a></td> @@ -2825,7 +2873,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -2857,7 +2905,7 @@ <td><a href="index_variable_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3475 entries)</td> +<td>(3574 entries)</td> </tr> <tr> <td>Library Index</td> @@ -2889,7 +2937,7 @@ <td><a href="index_library_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(89 entries)</td> +<td>(90 entries)</td> </tr> <tr> <td>Lemma Index</td> @@ -2921,7 +2969,7 @@ <td><a href="index_lemma_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(11853 entries)</td> +<td>(12096 entries)</td> </tr> <tr> <td>Constructor Index</td> @@ -2953,7 +3001,7 @@ <td><a href="index_constructor_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(359 entries)</td> +<td>(368 entries)</td> </tr> <tr> <td>Axiom Index</td> @@ -2985,7 +3033,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -3017,14 +3065,14 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(103 entries)</td> +<td>(107 entries)</td> </tr> <tr> <td>Projection Index</td> <td><a href="index_projection_A.html">A</a></td> <td><a href="index_projection_B.html">B</a></td> <td><a href="index_projection_C.html">C</a></td> -<td>D</td> +<td><a href="index_projection_D.html">D</a></td> <td><a href="index_projection_E.html">E</a></td> <td><a href="index_projection_F.html">F</a></td> <td><a href="index_projection_G.html">G</a></td> @@ -3049,7 +3097,7 @@ <td><a href="index_projection_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(266 entries)</td> +<td>(273 entries)</td> </tr> <tr> <td>Section Index</td> @@ -3081,7 +3129,7 @@ <td><a href="index_section_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(1118 entries)</td> +<td>(1140 entries)</td> </tr> <tr> <td>Abbreviation Index</td> @@ -3113,7 +3161,7 @@ <td><a href="index_abbreviation_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(691 entries)</td> +<td>(728 entries)</td> </tr> <tr> <td>Definition Index</td> @@ -3145,14 +3193,14 @@ <td><a href="index_definition_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3461 entries)</td> +<td>(3596 entries)</td> </tr> <tr> <td>Record Index</td> <td><a href="index_record_A.html">A</a></td> <td>B</td> <td><a href="index_record_C.html">C</a></td> -<td>D</td> +<td><a href="index_record_D.html">D</a></td> <td><a href="index_record_E.html">E</a></td> <td><a href="index_record_F.html">F</a></td> <td><a href="index_record_G.html">G</a></td> @@ -3177,7 +3225,7 @@ <td><a href="index_record_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(185 entries)</td> +<td>(189 entries)</td> </tr> </table> </div> |