diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_global_F.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_F.html')
| -rw-r--r-- | docs/htmldoc/index_global_F.html | 563 |
1 files changed, 333 insertions, 230 deletions
diff --git a/docs/htmldoc/index_global_F.html b/docs/htmldoc/index_global_F.html index 7dfdd53..b27db9e 100644 --- a/docs/htmldoc/index_global_F.html +++ b/docs/htmldoc/index_global_F.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_F"></a><h2>F </h2> @@ -526,12 +526,12 @@ <a href="mathcomp.field.falgebra.html#FalgebraTheory">FalgebraTheory</a> [section, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#FalgebraTheory.aT">FalgebraTheory.aT</a> [variable, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#FalgebraTheory.K">FalgebraTheory.K</a> [variable, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#22fc78a071967cb498292883560bf256">{ aspace _ } (type_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#7902c4a8ff2316fb35d6d0c2ed7d11ae">'Z ( _ ) (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#cbd9ee36d93894e7e70e23c2d488b443">'C ( _ ) (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#31433815c4b94767dc54e5ea54a78836">'C [ _ ] (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#21d8f2654a27422064fa906a038e93e4">_ ^+ _ (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#e27d7b49f0f266dd87f31a2700ab99c7">_ * _ (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> +<a href="mathcomp.field.falgebra.html#0ac367aab6864c536e98a34f9ffcfa34">{ aspace _ } (type_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> +<a href="mathcomp.field.falgebra.html#80354b4ac5a7ae24a2bb90308585eedc">'Z ( _ ) (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> +<a href="mathcomp.field.falgebra.html#2e0b34a8e05ee287d92de114cd9577b4">'C ( _ ) (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> +<a href="mathcomp.field.falgebra.html#a3603406613c9df0ee9e7d6a7f7e1386">'C [ _ ] (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> +<a href="mathcomp.field.falgebra.html#1d427e6c23d5e01e29ecf0123d1e1b59">_ ^+ _ (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> +<a href="mathcomp.field.falgebra.html#5215eefac650e5069ffc61e3cc9dc055">_ * _ (vspace_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#Falgebra_FieldMixin">Falgebra_FieldMixin</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#Falgebra.algType">Falgebra.algType</a> [definition, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#Falgebra.BaseMixin">Falgebra.BaseMixin</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> @@ -555,8 +555,8 @@ <a href="mathcomp.field.falgebra.html#Falgebra.Exports">Falgebra.Exports</a> [module, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#Falgebra.Exports.FalgType">Falgebra.Exports.FalgType</a> [abbreviation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#Falgebra.Exports.FalgUnitRingType">Falgebra.Exports.FalgUnitRingType</a> [abbreviation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#bcfd974a09004a8a31fe2123e2a5e1bb">[ FalgType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.falgebra.html#3c0387428f19a365dfa0c989db9030d7">[ FalgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> +<a href="mathcomp.field.falgebra.html#c59cbf7ead4fff233447196845a75eb7">[ FalgType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> +<a href="mathcomp.field.falgebra.html#8fcc6f073a7a36fa680d6889440e6651">[ FalgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#Falgebra.lalgType">Falgebra.lalgType</a> [definition, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#Falgebra.lmodType">Falgebra.lmodType</a> [definition, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#Falgebra.mixin">Falgebra.mixin</a> [projection, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> @@ -627,7 +627,6 @@ <a href="mathcomp.ssreflect.path.html#fcycle">fcycle</a> [abbreviation, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.fingroup.automorphism.html#fE">fE</a> [abbreviation, in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/> <a href="mathcomp.field.finfield.html#Fermat's_little_theorem">Fermat's_little_theorem</a> [lemma, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> -<a href="mathcomp.field.closed_field.html#fF">fF</a> [abbreviation, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.fingroup.morphism.html#ff">ff</a> [abbreviation, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/> <a href="mathcomp.ssreflect.binomial.html#ffactE">ffactE</a> [lemma, in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/> <a href="mathcomp.ssreflect.binomial.html#ffactnn">ffactnn</a> [lemma, in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/> @@ -642,7 +641,6 @@ <a href="mathcomp.ssreflect.binomial.html#ffact_gt0">ffact_gt0</a> [lemma, in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/> <a href="mathcomp.ssreflect.binomial.html#ffact_rec">ffact_rec</a> [definition, in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/> <a href="mathcomp.ssreflect.binomial.html#ffact0n">ffact0n</a> [lemma, in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#ffT">ffT</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.character.character.html#fful_lin_char_inj">fful_lin_char_inj</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#ffunE">ffunE</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#ffunK">ffunK</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> @@ -681,10 +679,13 @@ <a href="mathcomp.ssreflect.finfun.html#ffun_on">ffun_on</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#ffun_onP">ffun_onP</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#ffun_on_mem">ffun_on_mem</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#ffun0">ffun0</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.algebra.ssralg.html#ffun1_nonzero">ffun1_nonzero</a> [lemma, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.fingroup.action.html#fGisom">fGisom</a> [abbreviation, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#fgraph">fgraph</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#fgraphK">fgraphK</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#fgraph_codom">fgraph_codom</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#fgraph_ffun0">fgraph_ffun0</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.fingroup.quotient.html#fH">fH</a> [abbreviation, in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> <a href="mathcomp.fingroup.action.html#fHisom">fHisom</a> [abbreviation, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.quotient.html#fH_G">fH_G</a> [abbreviation, in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> @@ -700,7 +701,7 @@ <a href="mathcomp.character.classfun.html#FieldAutomorphism.R">FieldAutomorphism.R</a> [variable, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> <a href="mathcomp.character.classfun.html#FieldAutomorphism.rT">FieldAutomorphism.rT</a> [variable, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> <a href="mathcomp.character.classfun.html#FieldAutomorphism.u">FieldAutomorphism.u</a> [variable, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.character.classfun.html#e936761e50df896498d658058c61dde2">_ ^u</a> [notation, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> +<a href="mathcomp.character.classfun.html#951fc6d5628818da9c9fe35428eee358">_ ^u</a> [notation, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> <a href="mathcomp.field.fieldext.html#FieldExt">FieldExt</a> [module, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html">fieldext</a> [library]<br/> <a href="mathcomp.field.fieldext.html#FieldExtTheory">FieldExtTheory</a> [section, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> @@ -739,9 +740,9 @@ <a href="mathcomp.field.fieldext.html#FieldExt.eqType">FieldExt.eqType</a> [definition, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#FieldExt.Exports">FieldExt.Exports</a> [module, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType">FieldExt.Exports.fieldExtType</a> [abbreviation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#5f5a3c95feae5e889ef0ed2ea21bd611">[ fieldExtType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#03c33b945f661e93f536291e742438c3">[ fieldExtType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d">{ subfield _ } (type_scope)</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> +<a href="mathcomp.field.fieldext.html#78069a19fdca27731326a2758b55293c">[ fieldExtType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> +<a href="mathcomp.field.fieldext.html#702fe37861ef3c9032a715a749ac1ea7">[ fieldExtType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> +<a href="mathcomp.field.fieldext.html#810f00798e9fd6a59691271bacabea40">{ subfield _ } (type_scope)</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#FieldExt.FalgType">FieldExt.FalgType</a> [definition, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#FieldExt.Falg_fieldType">FieldExt.Falg_fieldType</a> [definition, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#FieldExt.Falg_idomainType">FieldExt.Falg_idomainType</a> [definition, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> @@ -808,7 +809,7 @@ <a href="mathcomp.field.fieldext.html#FieldOver.F">FieldOver.F</a> [variable, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#FieldOver.F0">FieldOver.F0</a> [variable, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#FieldOver.L">FieldOver.L</a> [variable, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#43aa599248ac296c93d07d0ece5108b7">_ *F: _</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> +<a href="mathcomp.field.fieldext.html#6f2c77fbfb346ccf3ded84f9624cdaa7">_ *F: _</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr">FieldRepr</a> [section, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Abelian">FieldRepr.Abelian</a> [section, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.AbelianQuotient">FieldRepr.AbelianQuotient</a> [section, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -848,7 +849,7 @@ <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Clifford.sH">FieldRepr.Clifford.sH</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Clifford.sHG">FieldRepr.Clifford.sHG</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Clifford.valWact">FieldRepr.Clifford.valWact</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#e18a3934ddda7b4da23627d05a96af2d">'Cl (action_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#c32b9d64dc405a3e24ead9493c235eac">'Cl (action_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Conjugate">FieldRepr.Conjugate</a> [section, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Conjugate.B">FieldRepr.Conjugate.B</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Conjugate.G">FieldRepr.Conjugate.G</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -960,10 +961,10 @@ <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Regular.sG">FieldRepr.Regular.sG</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Regular.splitG">FieldRepr.Regular.splitG</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Regular.sums_R">FieldRepr.Regular.sums_R</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#f525fb0dd2275735c0a65da3608bcb12">'e_ _ (group_ring_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#7b6a6a8c01938a6edd22860d7e925339">'R_ _ (group_ring_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#c674f1775e550ca38ba6626787fbdfd2">'n_ _ (group_ring_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#8178faf6fa436d2b11560085cf16b0f2">1 (irrType_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#054dde6e8475b5f978f6fc72d9b3020d">'e_ _ (group_ring_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#fed1998123fd4374722b35d4bd45df37">'R_ _ (group_ring_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#c76c6c26fb72cd04c64ab5deab6af994">'n_ _ (group_ring_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#8ba1b427d1cc10c412270edbc6cff6dd">1 (irrType_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Similarity">FieldRepr.Similarity</a> [section, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Similarity.G">FieldRepr.Similarity.G</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Similarity.gT">FieldRepr.Similarity.gT</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -981,7 +982,7 @@ <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Submodule.rG">FieldRepr.Submodule.rG</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Submodule.U">FieldRepr.Submodule.U</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#FieldRepr.Submodule.Umod">FieldRepr.Submodule.Umod</a> [variable, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.character.mxrepresentation.html#3cd258bd0038ef00bb5c09c7e22c6159">[ 1 _ ] (irrType_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.character.mxrepresentation.html#40a56b9af2338a1ea7b3f19d7505f6f6">[ 1 _ ] (irrType_scope)</a> [notation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.algebra.poly.html#FieldRoots">FieldRoots</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#FieldRoots.F">FieldRoots.F</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#FieldRoots.UnityRoots">FieldRoots.UnityRoots</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -1016,6 +1017,7 @@ <a href="mathcomp.ssreflect.seq.html#filter_pred0">filter_pred0</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#filter_rcons">filter_rcons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#filter_cat">filter_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#filter_nseq">filter_nseq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#filter_id">filter_id</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#filter_all">filter_all</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.character.classfun.html#filter_pairwise_orthogonal">filter_pairwise_orthogonal</a> [lemma, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> @@ -1031,6 +1033,9 @@ <a href="mathcomp.ssreflect.fintype.html#FinCancel.T">FinCancel.T</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.field.finfield.html#finCharP">finCharP</a> [lemma, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.ssreflect.seq.html#find">find</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinDepTheory">FinDepTheory</a> [section, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinDepTheory.aT">FinDepTheory.aT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinDepTheory.rT">FinDepTheory.rT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.fingraph.html#findex">findex</a> [definition, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> <a href="mathcomp.ssreflect.fingraph.html#findex_iter">findex_iter</a> [lemma, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> <a href="mathcomp.ssreflect.fingraph.html#findex_max">findex_max</a> [lemma, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> @@ -1043,7 +1048,7 @@ <a href="mathcomp.field.finfield.html#FinDomain.domR">FinDomain.domR</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#FinDomain.lregR">FinDomain.lregR</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#FinDomain.R">FinDomain.R</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> -<a href="mathcomp.field.finfield.html#f360384641878cb2be7294bed4659e99">_ %| _</a> [notation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> +<a href="mathcomp.field.finfield.html#24ae9732afc48da1e1f059fb289af11b">_ %| _</a> [notation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.ssreflect.seq.html#find_map">find_map</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#find_nseq">find_nseq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#find_cat">find_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1053,7 +1058,7 @@ <a href="mathcomp.field.finfield.html">finfield</a> [library]<br/> <a href="mathcomp.field.finfield.html#FinFieldExists">FinFieldExists</a> [section, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#FinFieldExists.map_poly_extField">FinFieldExists.map_poly_extField</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> -<a href="mathcomp.field.finfield.html#445fdb3ebc0ff682c0cd1af9d3a32b17">_ ^%:A (ring_scope)</a> [notation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> +<a href="mathcomp.field.finfield.html#387983a03fdf688b74a29beb3a4344bb">_ ^%:A (ring_scope)</a> [notation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#FinFieldExtType">FinFieldExtType</a> [abbreviation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.character.mxabelem.html#FinFieldRepr">FinFieldRepr</a> [section, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> <a href="mathcomp.character.mxabelem.html#FinFieldRepr.F">FinFieldRepr.F</a> [variable, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> @@ -1066,28 +1071,39 @@ <a href="mathcomp.character.mxabelem.html#FinFieldRepr.ScaleAction">FinFieldRepr.ScaleAction</a> [section, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> <a href="mathcomp.character.mxabelem.html#FinFieldRepr.ScaleAction.m">FinFieldRepr.ScaleAction.m</a> [variable, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> <a href="mathcomp.character.mxabelem.html#FinFieldRepr.ScaleAction.n">FinFieldRepr.ScaleAction.n</a> [variable, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> -<a href="mathcomp.character.mxabelem.html#4fffb19fcc003d579f537986e6d81a64">'Zm (action_scope)</a> [notation, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> +<a href="mathcomp.character.mxabelem.html#4e8ce2ff912cfeb67343e97564bc5001">'Zm (action_scope)</a> [notation, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> <a href="mathcomp.field.finfield.html#finField_galois_generator">finField_galois_generator</a> [lemma, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#finField_galois">finField_galois</a> [lemma, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#finField_is_abelem">finField_is_abelem</a> [lemma, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#finField_genPoly">finField_genPoly</a> [lemma, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#finField_unit">finField_unit</a> [definition, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#FinField.F">FinField.F</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#Finfun">Finfun</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#finfun">finfun</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#Finfun">Finfun</a> [constructor, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html">finfun</a> [library]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunComRing">FinFunComRing</a> [section, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunComRing.a">FinFunComRing.a</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunComRing.aT">FinFunComRing.aT</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunComRing.R">FinFunComRing.R</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunDef">FinfunDef</a> [module, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunDefSig">FinfunDefSig</a> [module, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunDefSig.finfun">FinfunDefSig.finfun</a> [axiom, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunDefSig.finfunE">FinfunDefSig.finfunE</a> [axiom, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunDef.finfun">FinfunDef.finfun</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunDef.finfunE">FinfunDef.finfunE</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunK">FinfunK</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunLmod">FinFunLmod</a> [section, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunLmod.aT">FinFunLmod.aT</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunLmod.R">FinFunLmod.R</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunLmod.rT">FinFunLmod.rT</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunOf">FinfunOf</a> [constructor, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunRing">FinFunRing</a> [section, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunRing.a">FinFunRing.a</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunRing.aT">FinFunRing.aT</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunRing.R">FinFunRing.R</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinFunTheory">FinFunTheory</a> [section, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinFunTheory.aT">FinFunTheory.aT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinFunTheory.rT">FinFunTheory.rT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunZmod">FinFunZmod</a> [section, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunZmod.aT">FinFunZmod.aT</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunZmod.rT">FinFunZmod.rT</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> @@ -1096,13 +1112,12 @@ <a href="mathcomp.algebra.ssralg.html#FinFunZmod.Sum.I">FinFunZmod.Sum.I</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunZmod.Sum.P">FinFunZmod.Sum.P</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> <a href="mathcomp.algebra.ssralg.html#FinFunZmod.Sum.r">FinFunZmod.Sum.r</a> [variable, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_finMixin">finfun_finMixin</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_countMixin">finfun_countMixin</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_choiceMixin">finfun_choiceMixin</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_eqMixin">finfun_eqMixin</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#finfun_def">finfun_def</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_of">finfun_of</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_type">finfun_type</a> [inductive, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#finfun_of">finfun_of</a> [inductive, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#finfun_rec">finfun_rec</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#finfun_cons">finfun_cons</a> [constructor, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#finfun_nil">finfun_nil</a> [constructor, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#finfun_on">finfun_on</a> [inductive, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finset.html#finfun_of_set">finfun_of_set</a> [definition, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.fingraph.html">fingraph</a> [library]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup">FinGroup</a> [module, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> @@ -1123,8 +1138,8 @@ <a href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.baseFinGroupType">FinGroup.Exports.baseFinGroupType</a> [abbreviation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.FinGroupType">FinGroup.Exports.FinGroupType</a> [abbreviation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType">FinGroup.Exports.finGroupType</a> [abbreviation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09">[ finGroupType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#bdbf19c07c4322c6fcf6df6c95066969">[ baseFinGroupType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> +<a href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a">[ finGroupType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> +<a href="mathcomp.fingroup.fingroup.html#ac5c214a3d709d8519333b0f98027cc9">[ baseFinGroupType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.finClass">FinGroup.finClass</a> [definition, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.InheritedClasses">FinGroup.InheritedClasses</a> [section, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.InheritedClasses.bT">FinGroup.InheritedClasses.bT</a> [variable, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> @@ -1140,9 +1155,9 @@ <a href="mathcomp.fingroup.fingroup.html#FinGroup.Mixin.mul1">FinGroup.Mixin.mul1</a> [variable, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.Mixin.one">FinGroup.Mixin.one</a> [variable, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.Mixin.T">FinGroup.Mixin.T</a> [variable, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#6982596e2b81c072ea7627dbd9786546">_ ^-1</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#006ee57122782cbbf25dc03841983bb0">_ * _</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.fingroup.fingroup.html#d998d540958964b9098d14237b8825c5">1</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> +<a href="mathcomp.fingroup.fingroup.html#956536dc58c202e68942118494784d7d">_ ^-1</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> +<a href="mathcomp.fingroup.fingroup.html#102ef8aeb14816079aff70619dedce2e">_ * _</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> +<a href="mathcomp.fingroup.fingroup.html#1944280a1d5c9fe870f1187d525b73f2">1</a> [notation, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.mk_invMg">FinGroup.mk_invMg</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.mk_invgK">FinGroup.mk_invgK</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.mul">FinGroup.mul</a> [projection, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> @@ -1209,13 +1224,13 @@ <a href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.f2sub">FiniteModule.OneFinMod.f2sub</a> [variable, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> <a href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.gT">FiniteModule.OneFinMod.gT</a> [variable, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> <a href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.sub2f">FiniteModule.OneFinMod.sub2f</a> [variable, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> -<a href="mathcomp.solvable.finmodule.html#7c98bb3aae09ec8defcde60e1fe9fd1a">'M (action_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> -<a href="mathcomp.solvable.finmodule.html#fc9edd19efe07e751389113a56e73526">'M (groupAction_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> -<a href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946">_ ^@ _ (ring_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> +<a href="mathcomp.solvable.finmodule.html#75180d85ac3b996e23d5f700ff669508">'M (action_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> +<a href="mathcomp.solvable.finmodule.html#60648ddfb848055c00656b4851a7ea06">'M (groupAction_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> +<a href="mathcomp.solvable.finmodule.html#a8d159da9722ccf39a3be9874c41f224">_ ^@ _ (ring_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> <a href="mathcomp.solvable.finmodule.html#FiniteModule.valA">FiniteModule.valA</a> [abbreviation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> -<a href="mathcomp.solvable.finmodule.html#5f85997305decc6e43bdcd4369b88e63">'M (action_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> -<a href="mathcomp.solvable.finmodule.html#1665aa361c9febc77836f6e34002c85d">'M (groupAction_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> -<a href="mathcomp.solvable.finmodule.html#5265ec8bf0e3eb99e5b993065d871eb7">_ ^@ _ (ring_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> +<a href="mathcomp.solvable.finmodule.html#e64e8beaaa33e98dbf15c1c648c8e8fa">'M (action_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> +<a href="mathcomp.solvable.finmodule.html#523346788a5254daf6c0408c3a5dc259">'M (groupAction_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> +<a href="mathcomp.solvable.finmodule.html#2b9e94cf53d24eee473cd33f39783e94">_ ^@ _ (ring_scope)</a> [notation, in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant">FiniteQuant</a> [module, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.all">FiniteQuant.all</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.all_in">FiniteQuant.all_in</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> @@ -1223,39 +1238,39 @@ <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.Definitions.T">FiniteQuant.Definitions.T</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.ex">FiniteQuant.ex</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.Exports">FiniteQuant.Exports</a> [module, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#820c0d91f14d8bd214791c55fe4916da">, exists _ : _ in _ _ (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#16c0991f94f0d812137457fc1c1383fe">, exists _ in _ _ (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#a933bbd16e3a45a4b889ac2f8732ec0e">[ exists _ : _ in _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#5404fd9d76c24a375fce91eeeb1972da">[ exists _ in _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#158832d8c1ec7121db752c45c87cc3aa">[ exists ( _ : _ | _ ) _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#2622a9930e3eed1321ab6ed4605c7142">[ exists ( _ | _ ) _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#a843dcbb9dc2e69b147054d3e1465e78">[ exists _ : _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2">[ exists _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#a1fa7fa2f38c8bf7a4380b3099a7f5cc">, forall _ : _ in _ _ (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#569613cf8a3bdd9ea86bbbe48a5b61c3">, forall _ in _ _ (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#35b77e34a049e8a812164aa2debaf974">[ forall _ : _ in _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#0a2353937835d965c09d6cd592199019">[ forall _ in _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30">[ forall ( _ : _ | _ ) _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#71aa9b4d33ee64c2b31b6cd545727657">[ forall ( _ | _ ) _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#924e46d1120f21a5b355c376b609abe3">[ forall _ : _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e">[ forall _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#7b05ad85727c891b29b0672026ea07f9">, exists ( _ : _ | _ ) _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#5fcc6a9a5ab8cf28a008d132794985d5">, exists ( _ | _ ) _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#9a69525d4d7bd01771d4d07ab174d2f1">, exists _ : _ _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#ef3225e810fcf2e8c51fa9af98d6cdaf">, exists _ _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#33851fdc2b3107574ff195c5b3a5f91c">, forall ( _ : _ | _ ) _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#71e191c4608118a84659c62df77deabc">, forall ( _ | _ ) _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#179e9cebf3b372c78d9f6a5df5a9c45d">, forall _ : _ _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#e66d8de38c2dd41a650467838c8fd364">, forall _ _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785">, _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#0145806588c5e908657ca7bbbf7abd16">, exists _ : _ in _ _ (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#919732e2a395b004050c56ad6129fab5">, exists _ in _ _ (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#251e8192c305cd7601bbed67fd6d6249">[ exists _ : _ in _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#f302e204901821a508e6d6d00228c0ed">[ exists _ in _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#14d06eec1f5f7dfac346d730fae6723c">[ exists ( _ : _ | _ ) _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#e9122b3568d6f47f958b76a6e55e4e40">[ exists ( _ | _ ) _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482">[ exists _ : _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25">[ exists _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#c6e0bc4114dd714e7262ed511d975a84">, forall _ : _ in _ _ (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#7406769ad390d6c18d532b497e931ef0">, forall _ in _ _ (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#e786d38fb1c78583c78486483761dfff">[ forall _ : _ in _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#9b40a7420e06ba2a775d87b43bd1c69f">[ forall _ in _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#b14c43cd248537980c3a1a815ab087df">[ forall ( _ : _ | _ ) _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#90a753c4c9a43b6ba4178e7bc1e47801">[ forall ( _ | _ ) _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#fb0199913c9911d56fa87965a9a828a3">[ forall _ : _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#ce8c9a990e3e773a56ef37417d3761c6">[ forall _ _ ] (bool_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#3b2dca918c748246f164f2487e80f224">, exists ( _ : _ | _ ) _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#e38196bd288251be5369c1e4ce7316f7">, exists ( _ | _ ) _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#5675e9c5cf174e09b1b7005056e9bd89">, exists _ : _ _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#879ea41111b984d072ab3bba11feda79">, exists _ _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#e43a13e3d639c464aa3578ee61719a3b">, forall ( _ : _ | _ ) _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#59ce155014a925cca079058b40bab72e">, forall ( _ | _ ) _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#e1924a831ebc4eede7a49ea158a3d66c">, forall _ : _ _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#491573e303f379eb171e60e73aff62ae">, forall _ _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98">, _ (fin_quant_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.ex_in">FiniteQuant.ex_in</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.Quantified">FiniteQuant.Quantified</a> [constructor, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.quantified">FiniteQuant.quantified</a> [inductive, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#FiniteQuant.quant0b">FiniteQuant.quant0b</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#87b50e2524afd24ce3fa86e25e250984">_ ^~</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#ed8677a60b02e6f4a3e034ddedab0754">_ ^*</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#6aaa6b7c692b4350a2b0b8947c625448">[ _ : _ | _ ]</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#8851f797d0e413ad24e2bf680ba67c0f">[ _ | _ ]</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#56df6c3db37fd477fd0b9e866d6c43d1">_ ^~</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#ea5146b504820609501c18972cdc0754">_ ^*</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#a144991985dddee1fffe479e66e76aa4">[ _ : _ | _ ]</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#fee710af89d70df72664de2598d9dce0">[ _ | _ ]</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.field.separable.html#finite_PET">finite_PET</a> [lemma, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.axiom">Finite.axiom</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.base">Finite.base</a> [projection, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> @@ -1287,8 +1302,8 @@ <a href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType">Finite.Exports.FinType</a> [abbreviation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType">Finite.Exports.finType</a> [abbreviation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.Exports.UniqFinMixin">Finite.Exports.UniqFinMixin</a> [abbreviation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e">[ finType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e">[ finType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f">[ finType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#274683adfd1c9a24b44d4dd6ea30913a">[ finType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.mixin">Finite.mixin</a> [projection, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.Mixin">Finite.Mixin</a> [constructor, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.Mixins">Finite.Mixins</a> [section, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> @@ -1307,7 +1322,9 @@ <a href="mathcomp.ssreflect.fintype.html#Finite.UniqMixin">Finite.UniqMixin</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.uniq_enumP">Finite.uniq_enumP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.xclass">Finite.xclass</a> [abbreviation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#finMixin">finMixin</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.solvable.finmodule.html">finmodule</a> [library]<br/> +<a href="mathcomp.ssreflect.finfun.html#finPi">finPi</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.field.finfield.html#FinRing">FinRing</a> [section, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing">FinRing</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.character.mxabelem.html#FinRingRepr">FinRingRepr</a> [section, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> @@ -1322,6 +1339,16 @@ <a href="mathcomp.algebra.finalg.html#FinRing.AdditiveGroup.U">FinRing.AdditiveGroup.U</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra">FinRing.Algebra</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.algType">FinRing.Algebra.algType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_finLalgType">FinRing.Algebra.alg_finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_finLmodType">FinRing.Algebra.alg_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_finRingType">FinRing.Algebra.alg_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_countRingType">FinRing.Algebra.alg_countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_finZmodType">FinRing.Algebra.alg_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_countZmodType">FinRing.Algebra.alg_countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_finGroupType">FinRing.Algebra.alg_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_baseFinGroupType">FinRing.Algebra.alg_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_finType">FinRing.Algebra.alg_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.alg_countType">FinRing.Algebra.alg_countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.base">FinRing.Algebra.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.baseFinGroupType">FinRing.Algebra.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.base2">FinRing.Algebra.base2</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1334,24 +1361,19 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.ClassDef.R">FinRing.Algebra.ClassDef.R</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.ClassDef.xT">FinRing.Algebra.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.class_of">FinRing.Algebra.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.countRingType">FinRing.Algebra.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.countType">FinRing.Algebra.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.countZmodType">FinRing.Algebra.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.eqType">FinRing.Algebra.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.Exports">FinRing.Algebra.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.Exports.finAlgType">FinRing.Algebra.Exports.finAlgType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#1f3938acab41e5853e751c34c441bf83">[ finAlgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#e1046e375fa30252214f407945285be1">[ finAlgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.finGroupType">FinRing.Algebra.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.finLalgType">FinRing.Algebra.finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.finLmodType">FinRing.Algebra.finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.finRingType">FinRing.Algebra.finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.finType">FinRing.Algebra.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.finZmodType">FinRing.Algebra.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.join_finGroupType">FinRing.Algebra.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.join_baseFinGroupType">FinRing.Algebra.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.join_finLalgType">FinRing.Algebra.join_finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.join_finLmodType">FinRing.Algebra.join_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.join_finRingType">FinRing.Algebra.join_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.join_finZmodType">FinRing.Algebra.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Algebra.join_finType">FinRing.Algebra.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.lalgType">FinRing.Algebra.lalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.lmodType">FinRing.Algebra.lmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.mixin">FinRing.Algebra.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1366,7 +1388,6 @@ <a href="mathcomp.algebra.finalg.html#FinRing.ComRing">FinRing.ComRing</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.base">FinRing.ComRing.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.baseFinGroupType">FinRing.ComRing.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.base2">FinRing.ComRing.base2</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.choiceType">FinRing.ComRing.choiceType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.class">FinRing.ComRing.class</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.Class">FinRing.ComRing.Class</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1375,20 +1396,28 @@ <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.ClassDef.xT">FinRing.ComRing.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.class_of">FinRing.ComRing.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.comRingType">FinRing.ComRing.comRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.comRing_finRingType">FinRing.ComRing.comRing_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.comRing_finZmodType">FinRing.ComRing.comRing_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.comRing_finGroupType">FinRing.ComRing.comRing_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.comRing_baseFinGroupType">FinRing.ComRing.comRing_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.comRing_finType">FinRing.ComRing.comRing_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countComRingType">FinRing.ComRing.countComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countComRing_finRingType">FinRing.ComRing.countComRing_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countComRing_finZmodType">FinRing.ComRing.countComRing_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countComRing_finGroupType">FinRing.ComRing.countComRing_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countComRing_baseFinGroupType">FinRing.ComRing.countComRing_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countComRing_finType">FinRing.ComRing.countComRing_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countRingType">FinRing.ComRing.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countType">FinRing.ComRing.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.countZmodType">FinRing.ComRing.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.eqType">FinRing.ComRing.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.Exports">FinRing.ComRing.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.Exports.finComRingType">FinRing.ComRing.Exports.finComRingType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#381777e14bce98b548cb274563c7fc56">[ finComRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099">[ finComRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.finGroupType">FinRing.ComRing.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.finRingType">FinRing.ComRing.finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.finType">FinRing.ComRing.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.finZmodType">FinRing.ComRing.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.join_finGroupType">FinRing.ComRing.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.join_baseFinGroupType">FinRing.ComRing.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.join_finRingType">FinRing.ComRing.join_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.join_finZmodType">FinRing.ComRing.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComRing.join_finType">FinRing.ComRing.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.mixin">FinRing.ComRing.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.pack">FinRing.ComRing.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.Pack">FinRing.ComRing.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1400,10 +1429,7 @@ <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing">FinRing.ComUnitRing</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.base">FinRing.ComUnitRing.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.baseFinGroupType">FinRing.ComUnitRing.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.base2">FinRing.ComUnitRing.base2</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.base3">FinRing.ComUnitRing.base3</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.choiceType">FinRing.ComUnitRing.choiceType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.cjoin_finUnitRingType">FinRing.ComUnitRing.cjoin_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.class">FinRing.ComUnitRing.class</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.Class">FinRing.ComUnitRing.Class</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.ClassDef">FinRing.ComUnitRing.ClassDef</a> [section, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1411,34 +1437,49 @@ <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.ClassDef.xT">FinRing.ComUnitRing.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.class_of">FinRing.ComUnitRing.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comRingType">FinRing.ComUnitRing.comRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comRing_finUnitRingType">FinRing.ComUnitRing.comRing_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comUnitRingType">FinRing.ComUnitRing.comUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comUnitRing_finUnitRingType">FinRing.ComUnitRing.comUnitRing_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comUnitRing_finComRingType">FinRing.ComUnitRing.comUnitRing_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comUnitRing_finRingType">FinRing.ComUnitRing.comUnitRing_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comUnitRing_finZmodType">FinRing.ComUnitRing.comUnitRing_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comUnitRing_finGroupType">FinRing.ComUnitRing.comUnitRing_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comUnitRing_baseFinGroupType">FinRing.ComUnitRing.comUnitRing_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.comUnitRing_finType">FinRing.ComUnitRing.comUnitRing_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComRingType">FinRing.ComUnitRing.countComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComRing_finUnitRingType">FinRing.ComUnitRing.countComRing_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComUnitRingType">FinRing.ComUnitRing.countComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComUnitRing_finUnitRingType">FinRing.ComUnitRing.countComUnitRing_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComUnitRing_finComRingType">FinRing.ComUnitRing.countComUnitRing_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComUnitRing_finRingType">FinRing.ComUnitRing.countComUnitRing_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComUnitRing_finZmodType">FinRing.ComUnitRing.countComUnitRing_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComUnitRing_finGroupType">FinRing.ComUnitRing.countComUnitRing_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComUnitRing_baseFinGroupType">FinRing.ComUnitRing.countComUnitRing_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countComUnitRing_finType">FinRing.ComUnitRing.countComUnitRing_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countRingType">FinRing.ComUnitRing.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countType">FinRing.ComUnitRing.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countUnitRingType">FinRing.ComUnitRing.countUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countUnitRing_finComRingType">FinRing.ComUnitRing.countUnitRing_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.countZmodType">FinRing.ComUnitRing.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.eqType">FinRing.ComUnitRing.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.Exports">FinRing.ComUnitRing.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.Exports.finComUnitRingType">FinRing.ComUnitRing.Exports.finComUnitRingType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#f0aa4fcf143660f4378ecfead8f3fdda">[ finComUnitRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.fcjoin_finUnitRingType">FinRing.ComUnitRing.fcjoin_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a">[ finComUnitRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.finComRingType">FinRing.ComUnitRing.finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.finComRing_finUnitRingType">FinRing.ComUnitRing.finComRing_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.finGroupType">FinRing.ComUnitRing.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.finRingType">FinRing.ComUnitRing.finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.finType">FinRing.ComUnitRing.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.finUnitRingType">FinRing.ComUnitRing.finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.finZmodType">FinRing.ComUnitRing.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.join_finGroupType">FinRing.ComUnitRing.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.join_baseFinGroupType">FinRing.ComUnitRing.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.join_finUnitRingType">FinRing.ComUnitRing.join_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.join_finComRingType">FinRing.ComUnitRing.join_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.join_finRingType">FinRing.ComUnitRing.join_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.join_finZmodType">FinRing.ComUnitRing.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.join_finType">FinRing.ComUnitRing.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.mixin">FinRing.ComUnitRing.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.pack">FinRing.ComUnitRing.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.Pack">FinRing.ComUnitRing.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.ringType">FinRing.ComUnitRing.ringType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.sort">FinRing.ComUnitRing.sort</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.type">FinRing.ComUnitRing.type</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.ujoin_finComRingType">FinRing.ComUnitRing.ujoin_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.unitRingType">FinRing.ComUnitRing.unitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.unitRing_finComRingType">FinRing.ComUnitRing.unitRing_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.xclass">FinRing.ComUnitRing.xclass</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.zmodType">FinRing.ComUnitRing.zmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.DecField">FinRing.DecField</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1465,7 +1506,6 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Field">FinRing.Field</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.base">FinRing.Field.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.baseFinGroupType">FinRing.Field.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.base2">FinRing.Field.base2</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.choiceType">FinRing.Field.choiceType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.class">FinRing.Field.class</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.Class">FinRing.Field.Class</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1475,12 +1515,37 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Field.class_of">FinRing.Field.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.comRingType">FinRing.Field.comRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.comUnitRingType">FinRing.Field.comUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countComRingType">FinRing.Field.countComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countComUnitRingType">FinRing.Field.countComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countFieldType">FinRing.Field.countFieldType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_finIdomainType">FinRing.Field.countField_finIdomainType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_finComUnitRingType">FinRing.Field.countField_finComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_finComRingType">FinRing.Field.countField_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_finUnitRingType">FinRing.Field.countField_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_finRingType">FinRing.Field.countField_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_finZmodType">FinRing.Field.countField_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_finGroupType">FinRing.Field.countField_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_baseFinGroupType">FinRing.Field.countField_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countField_finType">FinRing.Field.countField_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countIdomainType">FinRing.Field.countIdomainType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countRingType">FinRing.Field.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.countType">FinRing.Field.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countUnitRingType">FinRing.Field.countUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.countZmodType">FinRing.Field.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.eqType">FinRing.Field.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.Exports">FinRing.Field.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType">FinRing.Field.Exports.finFieldType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7">[ finFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47">[ finFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.fieldType">FinRing.Field.fieldType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_finIdomainType">FinRing.Field.field_finIdomainType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_finComUnitRingType">FinRing.Field.field_finComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_finComRingType">FinRing.Field.field_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_finUnitRingType">FinRing.Field.field_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_finRingType">FinRing.Field.field_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_finZmodType">FinRing.Field.field_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_finGroupType">FinRing.Field.field_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_baseFinGroupType">FinRing.Field.field_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Field.field_finType">FinRing.Field.field_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.finComRingType">FinRing.Field.finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.finComUnitRingType">FinRing.Field.finComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.finGroupType">FinRing.Field.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1490,15 +1555,6 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Field.finUnitRingType">FinRing.Field.finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.finZmodType">FinRing.Field.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.idomainType">FinRing.Field.idomainType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_finGroupType">FinRing.Field.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_baseFinGroupType">FinRing.Field.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_finIdomainType">FinRing.Field.join_finIdomainType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_finComUnitRingType">FinRing.Field.join_finComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_finComRingType">FinRing.Field.join_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_finUnitRingType">FinRing.Field.join_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_finRingType">FinRing.Field.join_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_finZmodType">FinRing.Field.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Field.join_finType">FinRing.Field.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.mixin">FinRing.Field.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.pack">FinRing.Field.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.Pack">FinRing.Field.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1525,7 +1581,6 @@ <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain">FinRing.IntegralDomain</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.base">FinRing.IntegralDomain.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.baseFinGroupType">FinRing.IntegralDomain.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.base2">FinRing.IntegralDomain.base2</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.choiceType">FinRing.IntegralDomain.choiceType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.class">FinRing.IntegralDomain.class</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.Class">FinRing.IntegralDomain.Class</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1535,11 +1590,25 @@ <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.class_of">FinRing.IntegralDomain.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.comRingType">FinRing.IntegralDomain.comRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.comUnitRingType">FinRing.IntegralDomain.comUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countComRingType">FinRing.IntegralDomain.countComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countComUnitRingType">FinRing.IntegralDomain.countComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomainType">FinRing.IntegralDomain.countIdomainType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomain_finComUnitRingType">FinRing.IntegralDomain.countIdomain_finComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomain_finComRingType">FinRing.IntegralDomain.countIdomain_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomain_finUnitRingType">FinRing.IntegralDomain.countIdomain_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomain_finRingType">FinRing.IntegralDomain.countIdomain_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomain_finZmodType">FinRing.IntegralDomain.countIdomain_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomain_finGroupType">FinRing.IntegralDomain.countIdomain_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomain_baseFinGroupType">FinRing.IntegralDomain.countIdomain_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countIdomain_finType">FinRing.IntegralDomain.countIdomain_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countRingType">FinRing.IntegralDomain.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countType">FinRing.IntegralDomain.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countUnitRingType">FinRing.IntegralDomain.countUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.countZmodType">FinRing.IntegralDomain.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.eqType">FinRing.IntegralDomain.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.Exports">FinRing.IntegralDomain.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.Exports.finIdomainType">FinRing.IntegralDomain.Exports.finIdomainType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#6c49b73b4d6aa1a932fafe7684bba39c">[ finIdomainType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c">[ finIdomainType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.finComRingType">FinRing.IntegralDomain.finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.finComUnitRingType">FinRing.IntegralDomain.finComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.finGroupType">FinRing.IntegralDomain.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1548,14 +1617,14 @@ <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.finUnitRingType">FinRing.IntegralDomain.finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.finZmodType">FinRing.IntegralDomain.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomainType">FinRing.IntegralDomain.idomainType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.join_finGroupType">FinRing.IntegralDomain.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.join_baseFinGroupType">FinRing.IntegralDomain.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.join_finComUnitRingType">FinRing.IntegralDomain.join_finComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.join_finComRingType">FinRing.IntegralDomain.join_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.join_finUnitRingType">FinRing.IntegralDomain.join_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.join_finRingType">FinRing.IntegralDomain.join_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.join_finZmodType">FinRing.IntegralDomain.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.join_finType">FinRing.IntegralDomain.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomain_finComUnitRingType">FinRing.IntegralDomain.idomain_finComUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomain_finComRingType">FinRing.IntegralDomain.idomain_finComRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomain_finUnitRingType">FinRing.IntegralDomain.idomain_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomain_finRingType">FinRing.IntegralDomain.idomain_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomain_finZmodType">FinRing.IntegralDomain.idomain_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomain_finGroupType">FinRing.IntegralDomain.idomain_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomain_baseFinGroupType">FinRing.IntegralDomain.idomain_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.idomain_finType">FinRing.IntegralDomain.idomain_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.mixin">FinRing.IntegralDomain.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.pack">FinRing.IntegralDomain.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.Pack">FinRing.IntegralDomain.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1579,31 +1648,38 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.ClassDef.R">FinRing.Lalgebra.ClassDef.R</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.ClassDef.xT">FinRing.Lalgebra.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.class_of">FinRing.Lalgebra.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.countRingType">FinRing.Lalgebra.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.countType">FinRing.Lalgebra.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.countZmodType">FinRing.Lalgebra.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.eqType">FinRing.Lalgebra.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.Exports">FinRing.Lalgebra.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.Exports.finLalgType">FinRing.Lalgebra.Exports.finLalgType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#f791552e58608a16cb248da4e7f34691">[ finLalgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#006f6a476eaf49ff2271764c2e9c0634">[ finLalgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.finGroupType">FinRing.Lalgebra.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.finLmodType">FinRing.Lalgebra.finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.finLmod_finRingType">FinRing.Lalgebra.finLmod_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.finLmod_countRingType">FinRing.Lalgebra.finLmod_countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.finLmod_ringType">FinRing.Lalgebra.finLmod_ringType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.finRingType">FinRing.Lalgebra.finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.finType">FinRing.Lalgebra.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.finZmodType">FinRing.Lalgebra.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.fljoin_finRingType">FinRing.Lalgebra.fljoin_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.join_finGroupType">FinRing.Lalgebra.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.join_baseFinGroupType">FinRing.Lalgebra.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.join_finRingType">FinRing.Lalgebra.join_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.join_finLmodType">FinRing.Lalgebra.join_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.join_finZmodType">FinRing.Lalgebra.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.join_finType">FinRing.Lalgebra.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalgType">FinRing.Lalgebra.lalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.ljoin_finRingType">FinRing.Lalgebra.ljoin_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_finRingType">FinRing.Lalgebra.lalg_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_countRingType">FinRing.Lalgebra.lalg_countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_finLmodType">FinRing.Lalgebra.lalg_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_finZmodType">FinRing.Lalgebra.lalg_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_countZmodType">FinRing.Lalgebra.lalg_countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_finGroupType">FinRing.Lalgebra.lalg_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_baseFinGroupType">FinRing.Lalgebra.lalg_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_finType">FinRing.Lalgebra.lalg_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lalg_countType">FinRing.Lalgebra.lalg_countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lmodType">FinRing.Lalgebra.lmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lmod_finRingType">FinRing.Lalgebra.lmod_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.lmod_countRingType">FinRing.Lalgebra.lmod_countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.mixin">FinRing.Lalgebra.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.pack">FinRing.Lalgebra.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.Pack">FinRing.Lalgebra.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.ringType">FinRing.Lalgebra.ringType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.rjoin_finLmodType">FinRing.Lalgebra.rjoin_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.sort">FinRing.Lalgebra.sort</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.type">FinRing.Lalgebra.type</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.xclass">FinRing.Lalgebra.xclass</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1611,7 +1687,6 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule">FinRing.Lmodule</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.base">FinRing.Lmodule.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.baseFinGroupType">FinRing.Lmodule.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.base2">FinRing.Lmodule.base2</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.choiceType">FinRing.Lmodule.choiceType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.class">FinRing.Lmodule.class</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.Class">FinRing.Lmodule.Class</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1622,18 +1697,21 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.ClassDef.xT">FinRing.Lmodule.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.class_of">FinRing.Lmodule.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.countType">FinRing.Lmodule.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.countZmodType">FinRing.Lmodule.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.eqType">FinRing.Lmodule.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.Exports">FinRing.Lmodule.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.Exports.finLmodType">FinRing.Lmodule.Exports.finLmodType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#73928e07fdf596d7d0d44cccaf9a9cb3">[ finLmodType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#89ed2b9c4fe0e2b73b78eb3dc17a4b6f">[ finLmodType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.finGroupType">FinRing.Lmodule.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.finType">FinRing.Lmodule.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.finZmodType">FinRing.Lmodule.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.join_finGroupType">FinRing.Lmodule.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.join_baseFinGroupType">FinRing.Lmodule.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.join_finZmodType">FinRing.Lmodule.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.join_finType">FinRing.Lmodule.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.lmodType">FinRing.Lmodule.lmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.lmod_finZmodType">FinRing.Lmodule.lmod_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.lmod_countZmodType">FinRing.Lmodule.lmod_countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.lmod_finGroupType">FinRing.Lmodule.lmod_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.lmod_baseFinGroupType">FinRing.Lmodule.lmod_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.lmod_finType">FinRing.Lmodule.lmod_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.lmod_countType">FinRing.Lmodule.lmod_countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.mixin">FinRing.Lmodule.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.pack">FinRing.Lmodule.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.Pack">FinRing.Lmodule.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1646,7 +1724,6 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Ring">FinRing.Ring</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.base">FinRing.Ring.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.baseFinGroupType">FinRing.Ring.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Ring.base2">FinRing.Ring.base2</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.choiceType">FinRing.Ring.choiceType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.class">FinRing.Ring.class</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.Class">FinRing.Ring.Class</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1654,11 +1731,17 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Ring.ClassDef.cT">FinRing.Ring.ClassDef.cT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.ClassDef.xT">FinRing.Ring.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.class_of">FinRing.Ring.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.countRingType">FinRing.Ring.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.countRing_finZmodType">FinRing.Ring.countRing_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.countRing_finGroupType">FinRing.Ring.countRing_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.countRing_baseFinGroupType">FinRing.Ring.countRing_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.countRing_finType">FinRing.Ring.countRing_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.countType">FinRing.Ring.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.countZmodType">FinRing.Ring.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.eqType">FinRing.Ring.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.Exports">FinRing.Ring.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.Exports.finRingType">FinRing.Ring.Exports.finRingType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c">[ finRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11">[ finRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.finGroupType">FinRing.Ring.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.finType">FinRing.Ring.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.finZmodType">FinRing.Ring.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1666,16 +1749,16 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Ring.inv">FinRing.Ring.inv</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.invr_out">FinRing.Ring.invr_out</a> [lemma, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.is_inv">FinRing.Ring.is_inv</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Ring.join_finGroupType">FinRing.Ring.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Ring.join_baseFinGroupType">FinRing.Ring.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Ring.join_finZmodType">FinRing.Ring.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Ring.join_finType">FinRing.Ring.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.mixin">FinRing.Ring.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.mulrV">FinRing.Ring.mulrV</a> [lemma, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.mulVr">FinRing.Ring.mulVr</a> [lemma, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.pack">FinRing.Ring.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.Pack">FinRing.Ring.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.ringType">FinRing.Ring.ringType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.ring_finZmodType">FinRing.Ring.ring_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.ring_finGroupType">FinRing.Ring.ring_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.ring_baseFinGroupType">FinRing.Ring.ring_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Ring.ring_finType">FinRing.Ring.ring_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.sort">FinRing.Ring.sort</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.type">FinRing.Ring.type</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.unit">FinRing.Ring.unit</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1700,7 +1783,6 @@ <a href="mathcomp.algebra.finalg.html#FinRing.unit">FinRing.unit</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Unit">FinRing.Unit</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra">FinRing.UnitAlgebra</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.ajoin_finUnitRingType">FinRing.UnitAlgebra.ajoin_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.algType">FinRing.UnitAlgebra.algType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.base">FinRing.UnitAlgebra.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.baseFinGroupType">FinRing.UnitAlgebra.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1715,12 +1797,20 @@ <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.ClassDef.R">FinRing.UnitAlgebra.ClassDef.R</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.ClassDef.xT">FinRing.UnitAlgebra.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.class_of">FinRing.UnitAlgebra.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countRingType">FinRing.UnitAlgebra.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countType">FinRing.UnitAlgebra.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countUnitRingType">FinRing.UnitAlgebra.countUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countUnitRing_finAlgType">FinRing.UnitAlgebra.countUnitRing_finAlgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countUnitRing_algType">FinRing.UnitAlgebra.countUnitRing_algType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countUnitRing_finLalgType">FinRing.UnitAlgebra.countUnitRing_finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countUnitRing_lalgType">FinRing.UnitAlgebra.countUnitRing_lalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countUnitRing_finLmodType">FinRing.UnitAlgebra.countUnitRing_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countUnitRing_lmodType">FinRing.UnitAlgebra.countUnitRing_lmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.countZmodType">FinRing.UnitAlgebra.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.eqType">FinRing.UnitAlgebra.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.Exports">FinRing.UnitAlgebra.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.Exports.finUnitAlgType">FinRing.UnitAlgebra.Exports.finUnitAlgType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#9af0def31728327fea663946c68b8952">[ finUnitAlgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.fajoin_finUnitRingType">FinRing.UnitAlgebra.fajoin_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#2aaa42abe766947d0080d3fd1521c4bc">[ finUnitAlgType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finAlgType">FinRing.UnitAlgebra.finAlgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finGroupType">FinRing.UnitAlgebra.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finLalgType">FinRing.UnitAlgebra.finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1728,39 +1818,44 @@ <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finRingType">FinRing.UnitAlgebra.finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finType">FinRing.UnitAlgebra.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finUnitRingType">FinRing.UnitAlgebra.finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finUnitRing_finAlgType">FinRing.UnitAlgebra.finUnitRing_finAlgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finUnitRing_algType">FinRing.UnitAlgebra.finUnitRing_algType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finUnitRing_finLalgType">FinRing.UnitAlgebra.finUnitRing_finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finUnitRing_lalgType">FinRing.UnitAlgebra.finUnitRing_lalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finUnitRing_finLmodType">FinRing.UnitAlgebra.finUnitRing_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finUnitRing_lmodType">FinRing.UnitAlgebra.finUnitRing_lmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finZmodType">FinRing.UnitAlgebra.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.fljoin_finUnitRingType">FinRing.UnitAlgebra.fljoin_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.fnjoin_finUnitRingType">FinRing.UnitAlgebra.fnjoin_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_finGroupType">FinRing.UnitAlgebra.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_baseFinGroupType">FinRing.UnitAlgebra.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_finAlgType">FinRing.UnitAlgebra.join_finAlgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_finLalgType">FinRing.UnitAlgebra.join_finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_finLmodType">FinRing.UnitAlgebra.join_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_finUnitRingType">FinRing.UnitAlgebra.join_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_finRingType">FinRing.UnitAlgebra.join_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_finZmodType">FinRing.UnitAlgebra.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.join_finType">FinRing.UnitAlgebra.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.lalgType">FinRing.UnitAlgebra.lalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.ljoin_finUnitRingType">FinRing.UnitAlgebra.ljoin_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.lmodType">FinRing.UnitAlgebra.lmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.mixin">FinRing.UnitAlgebra.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.njoin_finUnitRingType">FinRing.UnitAlgebra.njoin_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.pack">FinRing.UnitAlgebra.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.Pack">FinRing.UnitAlgebra.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.ringType">FinRing.UnitAlgebra.ringType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.sort">FinRing.UnitAlgebra.sort</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.type">FinRing.UnitAlgebra.type</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.ujoin_finAlgType">FinRing.UnitAlgebra.ujoin_finAlgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.ujoin_finLalgType">FinRing.UnitAlgebra.ujoin_finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.ujoin_finLmodType">FinRing.UnitAlgebra.ujoin_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlgType">FinRing.UnitAlgebra.unitAlgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_finAlgType">FinRing.UnitAlgebra.unitAlg_finAlgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_finLalgType">FinRing.UnitAlgebra.unitAlg_finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_finLmodType">FinRing.UnitAlgebra.unitAlg_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_finUnitRingType">FinRing.UnitAlgebra.unitAlg_finUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_countUnitRingType">FinRing.UnitAlgebra.unitAlg_countUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_finRingType">FinRing.UnitAlgebra.unitAlg_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_countRingType">FinRing.UnitAlgebra.unitAlg_countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_finZmodType">FinRing.UnitAlgebra.unitAlg_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_countZmodType">FinRing.UnitAlgebra.unitAlg_countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_finGroupType">FinRing.UnitAlgebra.unitAlg_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_baseFinGroupType">FinRing.UnitAlgebra.unitAlg_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_finType">FinRing.UnitAlgebra.unitAlg_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitAlg_countType">FinRing.UnitAlgebra.unitAlg_countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitRingType">FinRing.UnitAlgebra.unitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitRing_finAlgType">FinRing.UnitAlgebra.unitRing_finAlgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitRing_finLalgType">FinRing.UnitAlgebra.unitRing_finLalgType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.unitRing_finLmodType">FinRing.UnitAlgebra.unitRing_finLmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.xclass">FinRing.UnitAlgebra.xclass</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.zmodType">FinRing.UnitAlgebra.zmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing">FinRing.UnitRing</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.base">FinRing.UnitRing.base</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.baseFinGroupType">FinRing.UnitRing.baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.base2">FinRing.UnitRing.base2</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.choiceType">FinRing.UnitRing.choiceType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.class">FinRing.UnitRing.class</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Class">FinRing.UnitRing.Class</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1768,20 +1863,23 @@ <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.ClassDef.cT">FinRing.UnitRing.ClassDef.cT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.ClassDef.xT">FinRing.UnitRing.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.class_of">FinRing.UnitRing.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countRingType">FinRing.UnitRing.countRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countType">FinRing.UnitRing.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countUnitRingType">FinRing.UnitRing.countUnitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countUnitRing_finRingType">FinRing.UnitRing.countUnitRing_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countUnitRing_finZmodType">FinRing.UnitRing.countUnitRing_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countUnitRing_finGroupType">FinRing.UnitRing.countUnitRing_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countUnitRing_baseFinGroupType">FinRing.UnitRing.countUnitRing_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countUnitRing_finType">FinRing.UnitRing.countUnitRing_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.countZmodType">FinRing.UnitRing.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.eqType">FinRing.UnitRing.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Exports">FinRing.UnitRing.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Exports.finUnitRingType">FinRing.UnitRing.Exports.finUnitRingType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#7f21453830587186138043335ab91dd1">[ finUnitRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f">[ finUnitRingType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.finGroupType">FinRing.UnitRing.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.finRingType">FinRing.UnitRing.finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.finType">FinRing.UnitRing.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.finZmodType">FinRing.UnitRing.finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.join_finGroupType">FinRing.UnitRing.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.join_baseFinGroupType">FinRing.UnitRing.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.join_finRingType">FinRing.UnitRing.join_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.join_finZmodType">FinRing.UnitRing.join_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.join_finType">FinRing.UnitRing.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.mixin">FinRing.UnitRing.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.pack">FinRing.UnitRing.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Pack">FinRing.UnitRing.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1789,6 +1887,11 @@ <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.sort">FinRing.UnitRing.sort</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.type">FinRing.UnitRing.type</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.unitRingType">FinRing.UnitRing.unitRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.unitRing_finRingType">FinRing.UnitRing.unitRing_finRingType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.unitRing_finZmodType">FinRing.UnitRing.unitRing_finZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.unitRing_finGroupType">FinRing.UnitRing.unitRing_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.unitRing_baseFinGroupType">FinRing.UnitRing.unitRing_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.unitRing_finType">FinRing.UnitRing.unitRing_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.xclass">FinRing.UnitRing.xclass</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.zmodType">FinRing.UnitRing.zmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitsGroup">FinRing.UnitsGroup</a> [section, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1830,17 +1933,18 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.ClassDef.xT">FinRing.Zmodule.ClassDef.xT</a> [variable, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.class_of">FinRing.Zmodule.class_of</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.countType">FinRing.Zmodule.countType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.countZmodType">FinRing.Zmodule.countZmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.countZmod_finGroupType">FinRing.Zmodule.countZmod_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.countZmod_baseFinGroupType">FinRing.Zmodule.countZmod_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.countZmod_finType">FinRing.Zmodule.countZmod_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.eqType">FinRing.Zmodule.eqType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.Exports">FinRing.Zmodule.Exports</a> [module, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.Exports.finZmodType">FinRing.Zmodule.Exports.finZmodType</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4">[ finGroupType of _ for +%R ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd">[ baseFinGroupType of _ for +%R ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5">[ finZmodType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c">[ finGroupType of _ for +%R ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511">[ baseFinGroupType of _ for +%R ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944">[ finZmodType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.finGroupType">FinRing.Zmodule.finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.finType">FinRing.Zmodule.finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.join_finGroupType">FinRing.Zmodule.join_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.join_baseFinGroupType">FinRing.Zmodule.join_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> -<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.join_finType">FinRing.Zmodule.join_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.mixin">FinRing.Zmodule.mixin</a> [projection, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.pack">FinRing.Zmodule.pack</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.Pack">FinRing.Zmodule.Pack</a> [constructor, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1848,6 +1952,9 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.type">FinRing.Zmodule.type</a> [record, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.xclass">FinRing.Zmodule.xclass</a> [abbreviation, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.zmodType">FinRing.Zmodule.zmodType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.zmod_finGroupType">FinRing.Zmodule.zmod_finGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.zmod_baseFinGroupType">FinRing.Zmodule.zmod_baseFinGroupType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> +<a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.zmod_finType">FinRing.Zmodule.zmod_finType</a> [definition, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.zmodVgE">FinRing.zmodVgE</a> [lemma, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.zmodXgE">FinRing.zmodXgE</a> [lemma, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.zmod_abelian">FinRing.zmod_abelian</a> [lemma, in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -1866,9 +1973,6 @@ <a href="mathcomp.field.finfield.html#FinSplittingField.FinGalois.galL">FinSplittingField.FinGalois.galL</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#FinSplittingField.FinGalois.L">FinSplittingField.FinGalois.L</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#FinSplittingField.order">FinSplittingField.order</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FinTheory">FinTheory</a> [section, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FinTheory.aT">FinTheory.aT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FinTheory.rT">FinTheory.rT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#FinTuple">FinTuple</a> [module, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#FinTupleSig">FinTupleSig</a> [module, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#FinTupleSig.enum">FinTupleSig.enum</a> [axiom, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> @@ -2001,13 +2105,16 @@ <a href="mathcomp.algebra.poly.html#fmorph_unity_root">fmorph_unity_root</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#fmorph_root">fmorph_root</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.ssreflect.seq.html#foldl">foldl</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#foldlE">foldlE</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.seq.html#FoldLeft">FoldLeft</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#FoldLeft.f">FoldLeft.f</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#FoldLeft.R">FoldLeft.R</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#FoldLeft.T">FoldLeft.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#foldl_cat">foldl_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#foldl_rev">foldl_rev</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#foldl_idx">foldl_idx</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.seq.html#foldr">foldr</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#foldrE">foldrE</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.seq.html#FoldRight">FoldRight</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#FoldRightComp">FoldRightComp</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#FoldRightComp.f">FoldRightComp.f</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -2025,6 +2132,7 @@ <a href="mathcomp.ssreflect.tuple.html#forallb_tnth">forallb_tnth</a> [lemma, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#forallP">forallP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#forallPP">forallPP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#forall_inPP">forall_inPP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#forall_inP">forall_inP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#fp">fp</a> [abbreviation, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#fp">fp</a> [abbreviation, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> @@ -2044,11 +2152,11 @@ <a href="mathcomp.algebra.fraction.html#frac">frac</a> [projection, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracDomain">FracDomain</a> [section, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracDomain.R">FracDomain.R</a> [variable, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> -<a href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89">{ ratio _ }</a> [notation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> +<a href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc">{ ratio _ }</a> [notation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField">FracField</a> [module, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracFieldTheory">FracFieldTheory</a> [section, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracFieldTheory.R">FracFieldTheory.R</a> [variable, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> -<a href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac">_ %:F</a> [notation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> +<a href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d">_ %:F</a> [notation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField.add">FracField.add</a> [definition, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField.addA">FracField.addA</a> [lemma, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField.addC">FracField.addC</a> [lemma, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> @@ -2070,8 +2178,8 @@ <a href="mathcomp.algebra.fraction.html#FracField.frac">FracField.frac</a> [abbreviation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField.FracField">FracField.FracField</a> [section, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField.FracField.R">FracField.FracField.R</a> [variable, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> -<a href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77">_ %:F</a> [notation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> -<a href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f">{ fraction _ }</a> [notation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> +<a href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6">_ %:F</a> [notation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> +<a href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce">{ fraction _ }</a> [notation, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField.frac_comRingMixin">FracField.frac_comRingMixin</a> [definition, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField.frac_zmodMixin">FracField.frac_zmodMixin</a> [definition, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> <a href="mathcomp.algebra.fraction.html#FracField.inv">FracField.inv</a> [definition, in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/> @@ -2205,6 +2313,8 @@ <a href="mathcomp.ssreflect.finfun.html#fT">fT</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#fT">fT</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#fT">fT</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#fT">fT</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#fT">fT</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.algebra.vector.html#fullv">fullv</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.solvable.gfunctor.html#FunctorGroup">FunctorGroup</a> [section, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> <a href="mathcomp.solvable.gfunctor.html#FunctorGroup.F">FunctorGroup.F</a> [variable, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> @@ -2218,16 +2328,6 @@ <a href="mathcomp.solvable.gfunctor.html#FunctorTheory.F">FunctorTheory.F</a> [variable, in <a href="mathcomp.solvable.gfunctor.html">mathcomp.solvable.gfunctor</a>]<br/> <a href="mathcomp.field.algebraics_fundamentals.html#Fundamental_Theorem_of_Algebraics">Fundamental_Theorem_of_Algebraics</a> [lemma, in <a href="mathcomp.field.algebraics_fundamentals.html">mathcomp.field.algebraics_fundamentals</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#FunDelta">FunDelta</a> [constructor, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfun">FunFinfun</a> [module, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfunSig">FunFinfunSig</a> [module, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfunSig.finfun">FunFinfunSig.finfun</a> [axiom, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfunSig.finfunE">FunFinfunSig.finfunE</a> [axiom, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfunSig.fun_of_finE">FunFinfunSig.fun_of_finE</a> [axiom, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfunSig.fun_of_fin">FunFinfunSig.fun_of_fin</a> [axiom, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfun.finfun">FunFinfun.finfun</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfun.finfunE">FunFinfun.finfunE</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfun.fun_of_finE">FunFinfun.fun_of_finE</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfun.fun_of_fin">FunFinfun.fun_of_fin</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.finset.html#FunImage">FunImage</a> [section, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#FunImageComp">FunImageComp</a> [section, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#FunImageComp.T">FunImageComp.T</a> [variable, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> @@ -2240,6 +2340,9 @@ <a href="mathcomp.ssreflect.finset.html#FunImage.ImsetTheory.ImsetProp.f">FunImage.ImsetTheory.ImsetProp.f</a> [variable, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#FunImage.ImsetTheory.ImsetProp.f2">FunImage.ImsetTheory.ImsetProp.f2</a> [variable, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#FunImage.ImsetTheory.rT">FunImage.ImsetTheory.rT</a> [variable, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FunPlainTheory">FunPlainTheory</a> [section, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FunPlainTheory.aT">FunPlainTheory.aT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FunPlainTheory.rT">FunPlainTheory.rT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.algebra.vector.html#FunVectType">FunVectType</a> [section, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#FunVectType.I">FunVectType.I</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#FunVectType.R">FunVectType.R</a> [variable, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> @@ -2255,8 +2358,8 @@ <a href="mathcomp.algebra.vector.html#fun_of_lfun_def">fun_of_lfun_def</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.matrix.html#fun_of_matrix">fun_of_matrix</a> [definition, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.character.classfun.html#fun_of_cfun">fun_of_cfun</a> [definition, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#fun_of_fin">fun_of_fin</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#fun_of_fin_def">fun_of_fin_def</a> [abbreviation, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#fun_of_fin">fun_of_fin</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#fun_of_fin_rec">fun_of_fin_rec</a> [definition, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#fun_delta">fun_delta</a> [inductive, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.fingraph.html#fun_adjunction">fun_adjunction</a> [abbreviation, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> <a href="mathcomp.ssreflect.finset.html#Fun2Set1">Fun2Set1</a> [section, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> @@ -2337,7 +2440,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> @@ -2369,14 +2472,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> @@ -2401,7 +2504,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -2433,7 +2536,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> @@ -2465,7 +2568,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> @@ -2497,7 +2600,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> @@ -2529,7 +2632,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> @@ -2561,7 +2664,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -2593,14 +2696,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> @@ -2625,7 +2728,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> @@ -2657,7 +2760,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> @@ -2689,7 +2792,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> @@ -2721,14 +2824,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> @@ -2753,7 +2856,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> |