htmldoc regenerated

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_G.html
parent: 415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
1 files changed, 167 insertions, 168 deletions
diff --git a/docs/htmldoc/index_global_G.html b/docs/htmldoc/index_global_G.html
index ad61706..83c302a 100644
--- a/docs/htmldoc/index_global_G.html
+++ b/docs/htmldoc/index_global_G.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_G"></a><h2>G </h2>
@@ -556,8 +556,8 @@
 <a href="mathcomp.field.galois.html#GaloisTheory.TraceAndNormMorphism">GaloisTheory.TraceAndNormMorphism</a> [section, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
 <a href="mathcomp.field.galois.html#GaloisTheory.TraceAndNormMorphism.U">GaloisTheory.TraceAndNormMorphism.U</a> [variable, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
 <a href="mathcomp.field.galois.html#GaloisTheory.TraceAndNormMorphism.V">GaloisTheory.TraceAndNormMorphism.V</a> [variable, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
-<a href="mathcomp.field.galois.html#3af5abd0742b7b040fc8eec799c4f685">'Gal ( _ / _ ) (Group_scope)</a> [notation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
-<a href="mathcomp.field.galois.html#90b3c2a38aa2b5172e5cf7cf964e8989">'Gal ( _ / _ ) (group_scope)</a> [notation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
+<a href="mathcomp.field.galois.html#834b93517c3b719105b280284d33841a">'Gal ( _ / _ ) (Group_scope)</a> [notation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
+<a href="mathcomp.field.galois.html#eb63e7cabb476068136e59e10351a997">'Gal ( _ / _ ) (group_scope)</a> [notation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
 <a href="mathcomp.field.galois.html#galois_fixedField">galois_fixedField</a> [lemma, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
 <a href="mathcomp.field.galois.html#galois_factors">galois_factors</a> [lemma, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
 <a href="mathcomp.field.galois.html#galois_dim">galois_dim</a> [lemma, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/>
@@ -678,7 +678,6 @@
 <a href="mathcomp.algebra.intdiv.html#gcd0z">gcd0z</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
 <a href="mathcomp.ssreflect.div.html#gcd1n">gcd1n</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/>
 <a href="mathcomp.algebra.intdiv.html#gcd1z">gcd1z</a> [lemma, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#Gcl">Gcl</a> [abbreviation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#gcore">gcore</a> [definition, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#gcore_max">gcore_max</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#gcore_normal">gcore_normal</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
@@ -707,7 +706,7 @@
 <a href="mathcomp.character.integral_char.html#GenericClassSums.F">GenericClassSums.F</a> [variable, in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
 <a href="mathcomp.character.integral_char.html#GenericClassSums.G">GenericClassSums.G</a> [variable, in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
 <a href="mathcomp.character.integral_char.html#GenericClassSums.gT">GenericClassSums.gT</a> [variable, in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
-<a href="mathcomp.character.integral_char.html#afc4c4affce3b8ef6e9f442c1d91639c">'K_ _ (ring_scope)</a> [notation, in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
+<a href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060">'K_ _ (ring_scope)</a> [notation, in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
 <a href="mathcomp.ssreflect.generic_quotient.html">generic_quotient</a> [library]<br/>
 <a href="mathcomp.fingroup.fingroup.html#genGid">genGid</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#genGidG">genGidG</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
@@ -807,15 +806,15 @@
 <a href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2">GFunctor.Definitions.F2</a> [variable, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
 <a href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.k">GFunctor.Definitions.k</a> [variable, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
 <a href="mathcomp.solvable.gfunctor.html#GFunctor.Exports">GFunctor.Exports</a> [module, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#617ba6355e0c6813ccd42cf7ac127f20">[ mgFun of _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9">[ mgFun by _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#ee155ab488843b0ecc37c27fc7341f64">[ pgFun of _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0">[ pgFun by _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#607d805a80d936daf34262a28a285db3">[ gFun of _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7">[ gFun by _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#0d3cf0514afe70d7a29245834117002f">[ igFun of _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#6a21e731147765f65bc5f2e922126efc">[ igFun by _ & ! _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
-<a href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923">[ igFun by _ & _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#703ce4e21f8af3122d8da8159ae55c98">[ mgFun of _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa">[ mgFun by _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#09ca9041b424fb3a198e2a775c1edfdd">[ pgFun of _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#f4a0ec7c18bd128b271d4428328fd43b">[ pgFun by _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#b978f29f27d17b625bd1a96535c57314">[ gFun of _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#cecbde1597e0d77a491e8c4f94033af4">[ gFun by _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#0a3c3d64903581df0193a363279f22cc">[ igFun of _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#8dd9a311237b4fd5bc515a2cbf48517e">[ igFun by _ & ! _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
+<a href="mathcomp.solvable.gfunctor.html#c0205c751a17b7793ccdaf02cc4999e3">[ igFun by _ & _ ] (form_scope)</a> [notation, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
 <a href="mathcomp.solvable.gfunctor.html#GFunctor.group_valued">GFunctor.group_valued</a> [definition, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
 <a href="mathcomp.solvable.gfunctor.html#GFunctor.hereditary">GFunctor.hereditary</a> [definition, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
 <a href="mathcomp.solvable.gfunctor.html#GFunctor.IsoMap">GFunctor.IsoMap</a> [constructor, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/>
@@ -948,9 +947,9 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports">GRing.Additive.Exports</a> [module, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports.Additive">GRing.Additive.Exports.Additive</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports.additive">GRing.Additive.Exports.additive</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#f4cde972a26515a86aeac58343f1e022">[ additive of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#e25de7b1e68b5f1ea5f04a4e9520c4da">[ additive of _ as _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#6566b94c06c342b0768c3d2d73badf6e">{ additive _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#1f39c3338430de1e4f0dd19d42cfade9">[ additive of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#b15d1bebaaff5b5ed693647b6d36f348">{ additive _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Additive.map">GRing.Additive.map</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Additive.Pack">GRing.Additive.Pack</a> [constructor, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.addKr">GRing.addKr</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1003,8 +1002,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Algebra.Exports.AlgType">GRing.Algebra.Exports.AlgType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Algebra.Exports.algType">GRing.Algebra.Exports.algType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Algebra.Exports.CommAlgType">GRing.Algebra.Exports.CommAlgType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#30cfd03a0f671acf70ae071bdb2b2330">[ algType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#30ca49fca582d0576271da5ba1a53c8c">[ algType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#205d21d03e723fd656efd69d615cdfd2">[ algType _ of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Algebra.lalgType">GRing.Algebra.lalgType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Algebra.lmodType">GRing.Algebra.lmodType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Algebra.mixin">GRing.Algebra.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1061,8 +1060,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.ClosedField.Exports">GRing.ClosedField.Exports</a> [module, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ClosedField.Exports.ClosedFieldType">GRing.ClosedField.Exports.ClosedFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ClosedField.Exports.closedFieldType">GRing.ClosedField.Exports.closedFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#048a114d22ff709784bf346d4799d085">[ closedFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#65cd3e8351f6b67d79f598a877d53892">[ closedFieldType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#4fcb7e9ad725fb7730e1c5fbb1867235">[ closedFieldType of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ClosedField.fieldType">GRing.ClosedField.fieldType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ClosedField.idomainType">GRing.ClosedField.idomainType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ClosedField.pack">GRing.ClosedField.pack</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1117,8 +1116,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.ComRingMixin">GRing.ComRing.Exports.ComRingMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.ComRingType">GRing.ComRing.Exports.ComRingType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.comRingType">GRing.ComRing.Exports.comRingType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f">[ comRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#c5d157e6390935889519f9a9d4d53955">[ comRingType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d">[ comRingType of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComRing.mixin">GRing.ComRing.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComRing.pack">GRing.ComRing.pack</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComRing.Pack">GRing.ComRing.Pack</a> [constructor, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1147,7 +1146,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Exports">GRing.ComUnitRing.Exports</a> [module, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Exports.ComUnitRingMixin">GRing.ComUnitRing.Exports.ComUnitRingMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Exports.comUnitRingType">GRing.ComUnitRing.Exports.comUnitRingType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec">[ comUnitRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc">[ comUnitRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.mixin">GRing.ComUnitRing.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Mixin">GRing.ComUnitRing.Mixin</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Mixin">GRing.ComUnitRing.Mixin</a> [section, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1191,8 +1190,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.DecidableField.Exports.DecFieldMixin">GRing.DecidableField.Exports.DecFieldMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.DecidableField.Exports.DecFieldType">GRing.DecidableField.Exports.DecFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.DecidableField.Exports.decFieldType">GRing.DecidableField.Exports.decFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#69397cdbaa48460ee270e9344cbfe301">[ decFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#571e046df0f3cfb95cda10363e01c19e">[ decFieldType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#e40d136c069cdf352d78bc69141aeefa">[ decFieldType of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.DecidableField.fieldType">GRing.DecidableField.fieldType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.DecidableField.idomainType">GRing.DecidableField.idomainType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.DecidableField.mixin">GRing.DecidableField.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1261,7 +1260,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.EvalTerm.Pick.pred_f">GRing.EvalTerm.Pick.pred_f</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.EvalTerm.Pick.then_f">GRing.EvalTerm.Pick.then_f</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.EvalTerm.R">GRing.EvalTerm.R</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#532298027342e33d4d5bcb7293144f7f">[ rec _ , _ ]</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#ad32e01476f8d2c74998482c543d7f39">[ rec _ , _ ]</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.eval_Pick">GRing.eval_Pick</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.eval_If">GRing.eval_If</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.eval_tsubst">GRing.eval_tsubst</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1335,10 +1334,11 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldType">GRing.Field.Exports.FieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType">GRing.Field.Exports.fieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldUnitMixin">GRing.Field.Exports.FieldUnitMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f">[ fieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#8c9c50e5199526a82960ff32ca0ae688">[ fieldType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2">[ fieldType of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.IdomainMixin">GRing.Field.IdomainMixin</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.idomainType">GRing.Field.idomainType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#GRing.Field.IdomainType">GRing.Field.IdomainType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.intro_unit">GRing.Field.intro_unit</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.inv_out">GRing.Field.inv_out</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.mixin">GRing.Field.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1346,7 +1346,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.Mixins">GRing.Field.Mixins</a> [section, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.Mixins.inv">GRing.Field.Mixins.inv</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.Mixins.inv0">GRing.Field.Mixins.inv0</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#GRing.Field.Mixins.mulVx">GRing.Field.Mixins.mulVx</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#GRing.Field.Mixins.mulVf">GRing.Field.Mixins.mulVf</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.Mixins.R">GRing.Field.Mixins.R</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.mixin_of">GRing.Field.mixin_of</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.pack">GRing.Field.pack</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1356,6 +1356,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.type">GRing.Field.type</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.UnitMixin">GRing.Field.UnitMixin</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.unitRingType">GRing.Field.unitRingType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#GRing.Field.UnitRingType">GRing.Field.UnitRingType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.xclass">GRing.Field.xclass</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Field.zmodType">GRing.Field.zmodType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.fmorphV">GRing.fmorphV</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1417,8 +1418,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports">GRing.IntegralDomain.Exports</a> [module, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.IdomainType">GRing.IntegralDomain.Exports.IdomainType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType">GRing.IntegralDomain.Exports.idomainType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780">[ idomainType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#29ac7480dfde2720a0c36d25103fa4a7">[ idomainType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de">[ idomainType of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.mixin">GRing.IntegralDomain.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.pack">GRing.IntegralDomain.pack</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Pack">GRing.IntegralDomain.Pack</a> [constructor, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1476,8 +1477,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.Exports">GRing.Lalgebra.Exports</a> [module, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.Exports.LalgType">GRing.Lalgebra.Exports.LalgType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.Exports.lalgType">GRing.Lalgebra.Exports.lalgType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#e01b377a4a68dd74ced1f2b445ae1568">[ lalgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#d808753be7e4a961b68bffadddfcdf30">[ lalgType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#c3932ab7d4b1953f142288e718bebbc4">[ lalgType _ of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.ext">GRing.Lalgebra.ext</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.lmodType">GRing.Lalgebra.lmodType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.lmod_ringType">GRing.Lalgebra.lmod_ringType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1489,6 +1490,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.type">GRing.Lalgebra.type</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.xclass">GRing.Lalgebra.xclass</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.zmodType">GRing.Lalgebra.zmodType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#GRing.lastr_eq0">GRing.lastr_eq0</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LiftedRing">GRing.LiftedRing</a> [section, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LiftedRing.R">GRing.LiftedRing.R</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LiftedRing.T">GRing.LiftedRing.T</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1578,15 +1580,15 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.scalable">GRing.Linear.Exports.scalable</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.scalable_for">GRing.Linear.Exports.scalable_for</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.scalar">GRing.Linear.Exports.scalar</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#6a5a02fb109bf09435e2c36ba981b2b6">[ linear of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#774108f4d8a6842d8de559e977fc7a05">[ linear of _ as _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#56dc3588c918939e4ac45c0cdf7e2bdc">_ *^ _ _ (linear_ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#636fc7175acc7bc0025288ebd6946502">_ *:^ _ _ (linear_ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#b9df725616bc22e5319be68be2737326">_ * _ (linear_ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#1b425587d932db8b7cd45125c59bfd60">_ *: _ (linear_ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#3caf1c46544edfa98868625c22bf2d5e">{ scalar _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#697e59dccfd7ad4519680ddb16ef82da">{ linear _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#592bf656f19e2760c7b7fecf8aa4932d">{ linear _ | _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#6190fe21ffbd3dab252b4f744e9e9c11">[ linear of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#09fcb2ff53297f611c9440c05c397a76">_ *^ _ _ (linear_ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#34bba9fc83736a2ae54eedc9403c7ffa">_ *:^ _ _ (linear_ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#751e095f871b75182d9f960cbc38311e">_ * _ (linear_ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#18d5a37ddb86b27d9a3e716fcbda4ee7">_ *: _ (linear_ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#46175849544ed868533ead6f2ac4a179">{ scalar _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#b9a9030f88e15d1a3aacd4e8ec9a2391">{ linear _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#aabc8eba9c2cbefac5d796739c9a54bd">{ linear _ | _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Linear.map">GRing.Linear.map</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Linear.MapFor">GRing.Linear.MapFor</a> [constructor, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Linear.mapUV">GRing.Linear.mapUV</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1614,7 +1616,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.LmoduleTheory.ClosedPredicates.S">GRing.LmoduleTheory.ClosedPredicates.S</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LmoduleTheory.R">GRing.LmoduleTheory.R</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LmoduleTheory.V">GRing.LmoduleTheory.V</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#7afd8be1b339ff7cc68808fc72d11109">*:%R</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#30f6d8f9ddb331fb2136ef9c13244e1c">*:%R</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.base">GRing.Lmodule.base</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.choiceType">GRing.Lmodule.choiceType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.class">GRing.Lmodule.class</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1632,8 +1634,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.Exports.LmodMixin">GRing.Lmodule.Exports.LmodMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.Exports.LmodType">GRing.Lmodule.Exports.LmodType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.Exports.lmodType">GRing.Lmodule.Exports.lmodType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#f5696ebf026860a6f9c8dd4d23269df7">[ lmodType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#7ae3f0c4bde1f78bffc254ec020999a6">[ lmodType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#f564c8972b813e490c7ba0cd5a233f85">[ lmodType _ of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.mixin">GRing.Lmodule.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.Mixin">GRing.Lmodule.Mixin</a> [constructor, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Lmodule.mixin_of">GRing.Lmodule.mixin_of</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1687,9 +1689,9 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.LRMorphism.Exports.LRMorphism">GRing.LRMorphism.Exports.LRMorphism</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LRMorphism.Exports.lrmorphism">GRing.LRMorphism.Exports.lrmorphism</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LRMorphism.Exports.lrmorphism_for">GRing.LRMorphism.Exports.lrmorphism_for</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#8900f6ae77a86586561e15965d5870c7">[ lrmorphism of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#2759afce9315ab3f51737bc14cc79ce9">{ lrmorphism _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#e29f9115b869cd4fe3153ebcc11c593c">{ lrmorphism _ | _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566">[ lrmorphism of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#c998d6ecd14e902f7fd2311ac585dfed">{ lrmorphism _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#be490f36b8d971894ee8495ffc283566">{ lrmorphism _ | _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LRMorphism.map">GRing.LRMorphism.map</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LRMorphism.mixin">GRing.LRMorphism.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.LRMorphism.pack">GRing.LRMorphism.pack</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -1994,7 +1996,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.RingTheory.FrobeniusAutomorphism">GRing.RingTheory.FrobeniusAutomorphism</a> [section, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.RingTheory.FrobeniusAutomorphism.charFp">GRing.RingTheory.FrobeniusAutomorphism.charFp</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.RingTheory.FrobeniusAutomorphism.p">GRing.RingTheory.FrobeniusAutomorphism.p</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#258e0db845a269f145e1328806c3365d">_ ^f</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#0a9ddc310d4a9a62484de48da8431046">_ ^f</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.RingTheory.R">GRing.RingTheory.R</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Ring.base">GRing.Ring.base</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Ring.choiceType">GRing.Ring.choiceType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2012,8 +2014,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.RingMixin">GRing.Ring.Exports.RingMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.RingType">GRing.Ring.Exports.RingType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType">GRing.Ring.Exports.ringType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce">[ ringType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#35ecfd7bffc5e04ef0f8a2c421680259">[ ringType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071">[ ringType of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Ring.mixin">GRing.Ring.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Ring.Mixin">GRing.Ring.Mixin</a> [constructor, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Ring.mixin_of">GRing.Ring.mixin_of</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2063,9 +2065,9 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.multiplicative">GRing.RMorphism.Exports.multiplicative</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.RMorphism">GRing.RMorphism.Exports.RMorphism</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.rmorphism">GRing.RMorphism.Exports.rmorphism</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#778d861598c34ba1d4bea8b9adaae863">[ rmorphism of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#665e1724a466fd5a4c6ba181bb2c140c">[ rmorphism of _ as _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9">{ rmorphism _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#f59994a9f1c6ff43f3de0a3cea89bb6b">[ rmorphism of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5">{ rmorphism _ } (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.RMorphism.map">GRing.RMorphism.map</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.RMorphism.mixin">GRing.RMorphism.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.RMorphism.mixin_of">GRing.RMorphism.mixin_of</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2265,15 +2267,15 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.SubType.cast_zmodType">GRing.SubType.cast_zmodType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.SubType.comRingMixin">GRing.SubType.comRingMixin</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.SubType.Exports">GRing.SubType.Exports</a> [module, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#a44e69ea3e41fe55edbcaf554dca2dfa">[ fieldMixin of _ by <: ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#b3ccc27c5dac0393365d2ae3ecbb2b01">[ idomainMixin of _ by <: ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#4068b60b6efac062962fcea41c5f1fa3">[ unitRingMixin of _ by <: ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#24cde06860b9c92e6c9c0397a62009c8">[ algMixin of _ by <: ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#644239693c924204bb2585490fe83da2">[ comRingMixin of _ by <: ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#6d8ba92320b5d921588d1709c8536d66">[ lalgMixin of _ by <: ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#32c2078c0586b055b54305843b7f7e67">[ lmodMixin of _ by <: ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#d95bbf22ba89f2c48e1ae4fe1338b7ee">[ ringMixin of _ by <: ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#12c08185c491bc566a7da7b64605c9a3">[ zmodMixin of _ by <: ] (form_scope)</a> [notation, 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> [notation, 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> [notation, 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> [notation, 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> [notation, 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> [notation, 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> [notation, 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> [notation, 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> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.SubType.fieldMixin">GRing.SubType.fieldMixin</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.SubType.idomainMixin">GRing.SubType.idomainMixin</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.SubType.lalgMixin">GRing.SubType.lalgMixin</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2375,6 +2377,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.addrCA">GRing.Theory.addrCA</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.addrI">GRing.Theory.addrI</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.addrK">GRing.Theory.addrK</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#GRing.Theory.addrKA">GRing.Theory.addrKA</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.addrK_char2">GRing.Theory.addrK_char2</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.addrN">GRing.Theory.addrN</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.addrNK">GRing.Theory.addrNK</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2759,6 +2762,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.subKr">GRing.Theory.subKr</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.subrI">GRing.Theory.subrI</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.subrK">GRing.Theory.subrK</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#GRing.Theory.subrKA">GRing.Theory.subrKA</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.subrr">GRing.Theory.subrr</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.subrXX">GRing.Theory.subrXX</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Theory.subrXX_comm">GRing.Theory.subrXX_comm</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2827,7 +2831,7 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitAlgebra.eqType">GRing.UnitAlgebra.eqType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitAlgebra.Exports">GRing.UnitAlgebra.Exports</a> [module, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitAlgebra.Exports.unitAlgType">GRing.UnitAlgebra.Exports.unitAlgType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#bdb1eed686184a9a4099efa772be7bc7">[ unitAlgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#53130370ad22aac4f3ee8434dbc4850d">[ unitAlgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitAlgebra.lalgType">GRing.UnitAlgebra.lalgType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitAlgebra.lalg_unitRingType">GRing.UnitAlgebra.lalg_unitRingType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitAlgebra.lmodType">GRing.UnitAlgebra.lmodType</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2874,8 +2878,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.UnitRingMixin">GRing.UnitRing.Exports.UnitRingMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.UnitRingType">GRing.UnitRing.Exports.UnitRingType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.unitRingType">GRing.UnitRing.Exports.unitRingType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f">[ unitRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#cb745c487a899dce62ab9ce5330f227e">[ unitRingType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e">[ unitRingType of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitRing.inv">GRing.UnitRing.inv</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitRing.mixin">GRing.UnitRing.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Mixin">GRing.UnitRing.Mixin</a> [constructor, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2940,8 +2944,8 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.ZmodMixin">GRing.Zmodule.Exports.ZmodMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.ZmodType">GRing.Zmodule.Exports.ZmodType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.zmodType">GRing.Zmodule.Exports.zmodType</a> [abbreviation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68">[ zmodType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#285f5ccd0012cc284cf906e2e04f16f7">[ zmodType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac">[ zmodType of _ ] (form_scope)</a> [notation, 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> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Zmodule.mixin">GRing.Zmodule.mixin</a> [projection, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Mixin">GRing.Zmodule.Mixin</a> [constructor, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.Zmodule.mixin_of">GRing.Zmodule.mixin_of</a> [record, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
@@ -2955,65 +2959,65 @@
 <a href="mathcomp.algebra.ssralg.html#GRing.zmod_closedD">GRing.zmod_closedD</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.zmod_closedN">GRing.zmod_closedN</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.algebra.ssralg.html#GRing.zmod_closed">GRing.zmod_closed</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#2b0f3ec783c950f59954eab0f90dbfa8">_ \o* _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#82b32d32eab6e1eab8147f667d41c846">_ \*o _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#9df698f0b10c644da28c4afd9af58cf4">_ \*: _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#8af655ace12546ccf393660f3321db1e">_ \- _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#f2f8c9cbf6197be0e03c235df75623a4">_ \+ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#1b9a40373c4c41de4d5793af234729fd">\0 (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#a9486b60fd4d51d8247008b3f8b21d21">_ %:A (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#5aa7bcc9ac922e77482767d325fdbb69">_ *: _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#51fab11b73193ca5e8e7a62cac129ebc">[ char _ ] (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#b5a6699e28c97bb33352772cfa3ea869">_ ^+ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#ed99e7035d9a1f8a2c1515be81ac2e5f">_ * _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#c191333b9c7c034282647fbffacc9d18">_ %:R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#c2f73d0f0853394bdf717fa89709fd91">- 1 (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#40d0d61ba5822fd71ac598322297deff">1 (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#cba7c6485dff34fa5d3cd17d8c695698">_ `_ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#be9a273af87c6a30d88bd8379c802cbe">_ *- _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#513eaa3129601ecbcc9e188a80d6155b">_ *+ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#4d4b9697032429ec46472e6332d1356a">_ - _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#338c5345074fd3586073fd29273c138a">_ + _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#6c3404a70e11a79a0fa82b3d398aa71f">+%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#eefae7eea8ed2b8fccf150cb653d7a7b">- _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#221881b99d58ceaaa33c4172192f697e">-%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#44ac5b09393b1be3619627a18b1a1ed4">0 (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#bc08eb662d28e6715d9720beafd75750">'forall 'X_ _ , _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#cde0c417a2306d50158e89540db8c60d">'exists 'X_ _ , _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#5df5d3023a888489ad7cff86e72ea2fd">_ != _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#bf1935aa3f28dfd45301897795b397a5">~ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#0686cd1bb1af98b02865ebbedcf70bd7">_ ==> _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#00b8327e04e2b6f2d979016edbc0c67a">_ \/ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#421c9c3c51833f1724975feaafb4b744">_ /\ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#1a6fbc7f80506595657605bb77bac252">_ == _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#076e0496ae7ecaf146a6c132bdca5782">_ ^+ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#1a2301a3d5e4af0ad61623e89901bddb">_ / _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#8527e8676e2efa838eb3d51e80e2d39f">_ ^-1 (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#bb8dcb8add43cd5b4672890afb1d1839">_ *+ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#0b9ef6879d691a4408b07cd59dbb28f0">_ * _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#18e2ce36b5b2614b64eb5d1e85d95826">_ - _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#6c3b3e259d3f407cc03b5863f5d872ec">- _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#7f909243ac0228583a25471d8084551b">_ + _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#f1a311970e214d42d363692226487c34">1 (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#f0c6ff46ab1279b1af160d4c151a75b2">0 (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#36988dee1d5e98e959473a8f531d647c">_ %:T (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#680a63315a46806afe986215b67ab961">_ %:R (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#bb8753f66ae3a3b4b3bd3423d5bd7db1">'X_ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#44fd865ce10e1d30970d09bdd85a0c8e">_ ^o (type_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#a92cdad26f40e318882f385be2783a4c">_ ^c (type_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#17bbfbf532cf26564c92faf790f04f34">_ ^- _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#1adb36345c2607a4dd991537de5ddba3">_ / _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#7f97e90bec2e67d9beef5851649e3fb1">_ ^-1</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#6498e6e308d8a143464cf2d2ba603d36">*%R</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#9d4bc68f8a37455428efb931e05d31ce">*:%R</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#0efa7b1cdb084a1541f915d91ff051e5">\prod_ ( _ <= _ < _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#3d9b33c1fff84830fd684d3347f0b504">\prod_ ( _ in _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#939d2f6b3eeb99c97ee97374f97463ee">\prod_ ( _ | _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#3f1a950be6bcb72c9434150471b42417">\prod_ ( _ <- _ | _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#c6a5df59bc3b78ffe928e04ac98d6fa4">\sum_ ( _ in _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#33f78485f60ea5a637d17f41367f37d2">\sum_ ( _ < _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#309e5ebdf789a3828a9b458462d3e1bc">\sum_ ( _ <= _ < _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
-<a href="mathcomp.algebra.ssralg.html#664ae738a3286983847c80e5ee4c8c6b">\sum_ ( _ <- _ | _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#fc74b441e09df14f29dadaaae6a85505">_ \o* _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#bc3112e15c615abd16fe817a85e6c0fd">_ \*o _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#4f2c8844bdca193370eeb7e4ed6c690a">_ \*: _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#8934e834fc8aae356ef1d8f2b3bd03ed">_ \- _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#e2061ffc5a4c809cf18bbafb8211e59f">_ \+ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#2fadffc111e97bfa2ac21311dff6237b">\0 (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#b328a5aed2733481ae9bfe9f2b7cc645">_ %:A (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#10f331d2d40399852634935b8aa18b88">_ *: _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#7cf08e2f41bbb95903802050d3919698">[ char _ ] (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#a1ff23c95130eb62e8ce3bc8a42b5e38">_ ^+ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#f99a2dc6d143aa8f1021ab57e4a19eee">_ * _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#512a31305e556a90e0ad0550ee623cbc">_ %:R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#f51fd4f778bf0ac24a682f5e5bb9e825">- 1 (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#64d179658494c6d58eedb3b196ceab5a">1 (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#ba78b96b099a9672a88803cbbfa90ebc">_ `_ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#0c0f4a48fca1c1f27e9d71f54b6b8bd3">_ *- _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#506f68330939db1f655609b68b37b467">_ *+ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#4a5fc7f0d0a33bc3822357a38c953c9e">_ - _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#730bbb3cf1092122fa1a208d3879e5e8">_ + _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#89db507031b6d4a3d916a0f1c8eeaac2">+%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#aa58dfcfb323e1f070c38e31f9efddbe">- _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#f6c07ffdcee3462925d63c623b06b027">-%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#a4731bf93645db2d12d8aa577c913a83">0 (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#662c07b5d0726d21c8edce4d5fbaa087">'forall 'X_ _ , _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#3a3c189a0c88aa572171a0bae2912beb">'exists 'X_ _ , _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#0097d74fdc44ca768502e9edebe7e195">_ != _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#8fd8345f0bd0f50ba5171cc7c1b45aca">~ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#33d69901017412abb2c3513a87e991c1">_ ==> _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#bef44b50d3f3917949ecad5e3e01309c">_ \/ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#ab32bd0aebe6dabd4efe45ce35759537">_ /\ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#e6bce7853a73484fa8c54c3b3d0fe8f6">_ == _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#d56cb9de8d42b54fdfaa24a15d81424e">_ ^+ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#1d3f5aaba0b5415b38ef086fecc784cc">_ / _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#ae816e3b24c797f519ce51141978e695">_ ^-1 (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#74b863100f00ebe6b6a91299397f9af3">_ *+ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#a9e0394c049f1992b539cb7717095281">_ * _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#cb78c0285370423798e088d285c922f5">_ - _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#e2d8b10a7f82d8520cd39f5ef78702a0">- _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#dbf4583bf7f5ea301319678efa885505">_ + _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#eb428fcfecf865b66549cce36cfaa418">1 (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#97dbe2955d24055fd83c970067919944">0 (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#a4e52005e26c4b25ab5e860f94c039f7">_ %:T (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#8f212249fc4cb1d481e8d42f00523dbd">_ %:R (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#2d5cc450d76596e00ba9d438af4e1dc5">'X_ _ (term_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#44117511dc5f0eff9d2bcbcfcdd33874">_ ^o (type_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#a5048fbb5749bbf342aa41d2111c50c8">_ ^c (type_scope)</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#1e3664ff5a0845564dcf20fcc71a269d">_ ^- _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#705c00ff5a03bf84d6828df21a7a7942">_ / _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#139f286ff80df5d41ea22851b1826860">_ ^-1</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#bae191a5c954d16cccd67244cf8a6ceb">*%R</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#38480d07e3193b4bc897687500c6bc9c">*:%R</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#483796999382d9671d4ef0e14aab5328">\prod_ ( _ <= _ < _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#ffaead03d6bc40b2e0dc2c448b2f18da">\prod_ ( _ in _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#ba1581e43a210b25c8f779050e03b92e">\prod_ ( _ | _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#5e0b538209a51fa2bd900767b9312dd8">\prod_ ( _ <- _ | _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#3f77cb0ecca797dabe8a89fee7b1337b">\sum_ ( _ in _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#2212b29e1a046120b3e8fdf5f4fbcd1f">\sum_ ( _ < _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#b6b1fbfe788a2b1990c0d8b2548df5eb">\sum_ ( _ <= _ < _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
+<a href="mathcomp.algebra.ssralg.html#dcb91d0b08ece8369cc6084787184d13">\sum_ ( _ <- _ | _ ) _</a> [notation, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#group">group</a> [definition, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#Group">Group</a> [constructor, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.fingroup.action.html#groupAction">groupAction</a> [record, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
@@ -3134,11 +3138,6 @@
 <a href="mathcomp.fingroup.gproduct.html#group0">group0</a> [lemma, in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#group1">group1</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#group1_contra">group1_contra</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#group1_finType">group1_finType</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#group1_eqType">group1_eqType</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#group1_class12">group1_class12</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#group1_class2">group1_class2</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#group1_class1">group1_class1</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.solvable.extraspecial.html#Grp_pX1p2">Grp_pX1p2</a> [lemma, in <a href="mathcomp.solvable.extraspecial.html">mathcomp.solvable.extraspecial</a>]<br/>
 <a href="mathcomp.solvable.extremal.html#Grp_quaternion">Grp_quaternion</a> [lemma, in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/>
 <a href="mathcomp.solvable.extremal.html#Grp_semidihedral">Grp_semidihedral</a> [lemma, in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/>
@@ -3160,12 +3159,12 @@
 <a href="mathcomp.ssreflect.ssrnat.html#gtn_min">gtn_min</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
 <a href="mathcomp.ssreflect.ssrnat.html#gtn_max">gtn_max</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
 <a href="mathcomp.ssreflect.ssrnat.html#gtn_eqF">gtn_eqF</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#gTr">gTr</a> [abbreviation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
 <a href="mathcomp.algebra.ssrint.html#gtr0_sgz">gtr0_sgz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
 <a href="mathcomp.solvable.extraspecial.html#gtype">gtype</a> [abbreviation, in <a href="mathcomp.solvable.extraspecial.html">mathcomp.solvable.extraspecial</a>]<br/>
 <a href="mathcomp.algebra.ssrint.html#gtz0_abs">gtz0_abs</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
 <a href="mathcomp.algebra.ssrint.html#gtz0_ge1">gtz0_ge1</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
 <a href="mathcomp.algebra.rat.html#gt_rat0">gt_rat0</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/>
+<a href="mathcomp.algebra.poly.html#gt_size_poly_neq0">gt_size_poly_neq0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
 <a href="mathcomp.character.classfun.html#gt0CG">gt0CG</a> [lemma, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
 <a href="mathcomp.character.classfun.html#gt0CiG">gt0CiG</a> [lemma, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
 <a href="mathcomp.fingroup.fingroup.html#gval">gval</a> [projection, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
@@ -3203,7 +3202,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>
@@ -3235,14 +3234,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>
@@ -3267,7 +3266,7 @@
 <td>Z</td>
 <td>_</td>
 <td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
 </tr>
 <tr>
 <td>Variable Index</td>
@@ -3299,7 +3298,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>
@@ -3331,7 +3330,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>
@@ -3363,7 +3362,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>
@@ -3395,7 +3394,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>
@@ -3427,7 +3426,7 @@
 <td>Z</td>
 <td>_</td>
 <td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
 </tr>
 <tr>
 <td>Inductive Index</td>
@@ -3459,14 +3458,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>
@@ -3491,7 +3490,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>
@@ -3523,7 +3522,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>
@@ -3555,7 +3554,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>
@@ -3587,14 +3586,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>
@@ -3619,7 +3618,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>
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_G.html
parent	415be3b908daadabf178a292c885db78e5b2c9a4 (diff)