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_definition_F.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_definition_F.html')
| -rw-r--r-- | docs/htmldoc/index_definition_F.html | 353 |
1 files changed, 221 insertions, 132 deletions
diff --git a/docs/htmldoc/index_definition_F.html b/docs/htmldoc/index_definition_F.html index 179caa4..3c940c8 100644 --- a/docs/htmldoc/index_definition_F.html +++ b/docs/htmldoc/index_definition_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="definition_F"></a><h2>F (definition)</h2> @@ -570,11 +570,9 @@ <a href="mathcomp.field.finfield.html#FinDomainFieldType">FinDomainFieldType</a> [in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#FinDomainSplittingFieldType">FinDomainSplittingFieldType</a> [in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#finField_unit">finField_unit</a> [in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_finMixin">finfun_finMixin</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_countMixin">finfun_countMixin</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_choiceMixin">finfun_choiceMixin</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_eqMixin">finfun_eqMixin</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#finfun_of">finfun_of</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#Finfun">Finfun</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#FinfunDef.finfun">FinfunDef.finfun</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#finfun_rec">finfun_rec</a> [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> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.arg_finType">FinGroup.arg_finType</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#FinGroup.arg_countType">FinGroup.arg_countType</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> @@ -618,12 +616,25 @@ <a href="mathcomp.ssreflect.fintype.html#Finite.eqType">Finite.eqType</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.pack">Finite.pack</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Finite.UniqMixin">Finite.UniqMixin</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#finMixin">finMixin</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.algType">FinRing.Algebra.algType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.choiceType">FinRing.Algebra.choiceType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.class">FinRing.Algebra.class</a> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -631,65 +642,77 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.finRingType">FinRing.Algebra.finRingType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.pack">FinRing.Algebra.pack</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.ringType">FinRing.Algebra.ringType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Algebra.zmodType">FinRing.Algebra.zmodType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.ringType">FinRing.ComRing.ringType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.ComRing.zmodType">FinRing.ComRing.zmodType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.DecField.baseFinGroupType">FinRing.DecField.baseFinGroupType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.DecField.finComRingType">FinRing.DecField.finComRingType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -703,14 +726,38 @@ <a href="mathcomp.algebra.finalg.html#FinRing.DecField.type">FinRing.DecField.type</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.DecidableFieldMixin">FinRing.DecidableFieldMixin</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -720,15 +767,6 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Field.finUnitRingType">FinRing.Field.finUnitRingType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.ringType">FinRing.Field.ringType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Field.unitRingType">FinRing.Field.unitRingType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -736,12 +774,25 @@ <a href="mathcomp.algebra.finalg.html#FinRing.gen_pack">FinRing.gen_pack</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.groupMixin">FinRing.groupMixin</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -751,14 +802,14 @@ <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.finUnitRingType">FinRing.IntegralDomain.finUnitRingType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.ringType">FinRing.IntegralDomain.ringType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.unitRingType">FinRing.IntegralDomain.unitRingType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -768,60 +819,74 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.base3">FinRing.Lalgebra.base3</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.choiceType">FinRing.Lalgebra.choiceType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.class">FinRing.Lalgebra.class</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lalgebra.zmodType">FinRing.Lalgebra.zmodType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Lmodule.zmodType">FinRing.Lmodule.zmodType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.inv">FinRing.Ring.inv</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.UnitMixin">FinRing.Ring.UnitMixin</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Ring.zmodType">FinRing.Ring.zmodType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -837,16 +902,23 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Theory.zmod_abelian">FinRing.Theory.zmod_abelian</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Theory.zmod_mulgC">FinRing.Theory.zmod_mulgC</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Theory.zmod1gE">FinRing.Theory.zmod1gE</a> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.base2">FinRing.UnitAlgebra.base2</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.base3">FinRing.UnitAlgebra.base3</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.choiceType">FinRing.UnitAlgebra.choiceType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.class">FinRing.UnitAlgebra.class</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -854,48 +926,61 @@ <a href="mathcomp.algebra.finalg.html#FinRing.UnitAlgebra.finRingType">FinRing.UnitAlgebra.finRingType</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.UnitRing.ringType">FinRing.UnitRing.ringType</a> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.unit_act">FinRing.unit_act</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.unit_GroupMixin">FinRing.unit_GroupMixin</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> @@ -911,14 +996,18 @@ <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.choiceType">FinRing.Zmodule.choiceType</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.algebra.finalg.html#FinRing.Zmodule.class">FinRing.Zmodule.class</a> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [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> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#FinTuple.enum">FinTuple.enum</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> <a href="mathcomp.ssreflect.fingraph.html#finv">finv</a> [in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#fin_pred_sort">fin_pred_sort</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> @@ -957,13 +1046,13 @@ <a href="mathcomp.solvable.frobenius.html#Frobenius_group">Frobenius_group</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> <a href="mathcomp.solvable.frobenius.html#Frobenius_group_with_complement">Frobenius_group_with_complement</a> [in <a href="mathcomp.solvable.frobenius.html">mathcomp.solvable.frobenius</a>]<br/> <a href="mathcomp.algebra.vector.html#fullv">fullv</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#FunFinfun.finfun">FunFinfun.finfun</a> [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> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.path.html#fun_base">fun_base</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.algebra.vector.html#fun_of_lfun">fun_of_lfun</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#fun_of_lfun_def">fun_of_lfun_def</a> [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> [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> [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> [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> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#fwith">fwith</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#F0">F0</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#F1">F1</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> @@ -1002,7 +1091,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> @@ -1034,14 +1123,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> @@ -1066,7 +1155,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -1098,7 +1187,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> @@ -1130,7 +1219,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> @@ -1162,7 +1251,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> @@ -1194,7 +1283,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> @@ -1226,7 +1315,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -1258,14 +1347,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> @@ -1290,7 +1379,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> @@ -1322,7 +1411,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> @@ -1354,7 +1443,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> @@ -1386,14 +1475,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> @@ -1418,7 +1507,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> |