diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_global_P.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_P.html')
| -rw-r--r-- | docs/htmldoc/index_global_P.html | 217 |
1 files changed, 139 insertions, 78 deletions
diff --git a/docs/htmldoc/index_global_P.html b/docs/htmldoc/index_global_P.html index 7dd5cb8..1233911 100644 --- a/docs/htmldoc/index_global_P.html +++ b/docs/htmldoc/index_global_P.html @@ -4,7 +4,7 @@ <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.ssreflect.tuple</title> +<title>mathcomp.test_suite.hierarchy_test</title> </head> <body> @@ -47,7 +47,7 @@ <td><a href="index_global_Z.html">Z</a></td> <td>_</td> <td><a href="index_global_*.html">other</a></td> -<td>(23233 entries)</td> +<td>(23836 entries)</td> </tr> <tr> <td>Notation Index</td> @@ -79,14 +79,14 @@ <td><a href="index_notation_Z.html">Z</a></td> <td>_</td> <td><a href="index_notation_*.html">other</a></td> -<td>(1373 entries)</td> +<td>(1409 entries)</td> </tr> <tr> <td>Module Index</td> <td><a href="index_module_A.html">A</a></td> <td><a href="index_module_B.html">B</a></td> <td><a href="index_module_C.html">C</a></td> -<td>D</td> +<td><a href="index_module_D.html">D</a></td> <td><a href="index_module_E.html">E</a></td> <td><a href="index_module_F.html">F</a></td> <td><a href="index_module_G.html">G</a></td> @@ -111,7 +111,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -143,7 +143,7 @@ <td><a href="index_variable_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3475 entries)</td> +<td>(3574 entries)</td> </tr> <tr> <td>Library Index</td> @@ -175,7 +175,7 @@ <td><a href="index_library_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(89 entries)</td> +<td>(90 entries)</td> </tr> <tr> <td>Lemma Index</td> @@ -207,7 +207,7 @@ <td><a href="index_lemma_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(11853 entries)</td> +<td>(12096 entries)</td> </tr> <tr> <td>Constructor Index</td> @@ -239,7 +239,7 @@ <td><a href="index_constructor_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(359 entries)</td> +<td>(368 entries)</td> </tr> <tr> <td>Axiom Index</td> @@ -271,7 +271,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -303,14 +303,14 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(103 entries)</td> +<td>(107 entries)</td> </tr> <tr> <td>Projection Index</td> <td><a href="index_projection_A.html">A</a></td> <td><a href="index_projection_B.html">B</a></td> <td><a href="index_projection_C.html">C</a></td> -<td>D</td> +<td><a href="index_projection_D.html">D</a></td> <td><a href="index_projection_E.html">E</a></td> <td><a href="index_projection_F.html">F</a></td> <td><a href="index_projection_G.html">G</a></td> @@ -335,7 +335,7 @@ <td><a href="index_projection_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(266 entries)</td> +<td>(273 entries)</td> </tr> <tr> <td>Section Index</td> @@ -367,7 +367,7 @@ <td><a href="index_section_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(1118 entries)</td> +<td>(1140 entries)</td> </tr> <tr> <td>Abbreviation Index</td> @@ -399,7 +399,7 @@ <td><a href="index_abbreviation_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(691 entries)</td> +<td>(728 entries)</td> </tr> <tr> <td>Definition Index</td> @@ -431,14 +431,14 @@ <td><a href="index_definition_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3461 entries)</td> +<td>(3596 entries)</td> </tr> <tr> <td>Record Index</td> <td><a href="index_record_A.html">A</a></td> <td>B</td> <td><a href="index_record_C.html">C</a></td> -<td>D</td> +<td><a href="index_record_D.html">D</a></td> <td><a href="index_record_E.html">E</a></td> <td><a href="index_record_F.html">F</a></td> <td><a href="index_record_G.html">G</a></td> @@ -463,7 +463,7 @@ <td><a href="index_record_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(185 entries)</td> +<td>(189 entries)</td> </tr> </table> <hr/><a name="global_P"></a><h2>P </h2> @@ -1031,11 +1031,11 @@ <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.FieldDivision.FieldMap">Pdiv.Field.FieldDivision.FieldMap</a> [section, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.FieldDivision.FieldMap.f">Pdiv.Field.FieldDivision.FieldMap.f</a> [variable, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.FieldDivision.FieldMap.rR">Pdiv.Field.FieldDivision.FieldMap.rR</a> [variable, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> -<a href="mathcomp.algebra.polydiv.html#34b65849dab7adb22098517124e67650">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> +<a href="mathcomp.algebra.polydiv.html#ffd296f893410e849a35ec5356a13636">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.FieldDivision.FieldRingMap">Pdiv.Field.FieldDivision.FieldRingMap</a> [section, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.FieldDivision.FieldRingMap.f">Pdiv.Field.FieldDivision.FieldRingMap.f</a> [variable, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.FieldDivision.FieldRingMap.rR">Pdiv.Field.FieldDivision.FieldRingMap.rR</a> [variable, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> -<a href="mathcomp.algebra.polydiv.html#67d6f029332878db8c6f4efc5c9b26ee">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> +<a href="mathcomp.algebra.polydiv.html#7ccad1b5013efc6ffe407f7b77347c15">_ ^f (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.gcdp_map">Pdiv.Field.gcdp_map</a> [lemma, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.gdcop_map">Pdiv.Field.gdcop_map</a> [lemma, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.Field.gdcop_rec_map">Pdiv.Field.gdcop_rec_map</a> [lemma, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> @@ -1069,10 +1069,10 @@ <a href="mathcomp.algebra.polydiv.html#Pdiv.IdomainDefs.IDomainPseudoDivisionDefs.R">Pdiv.IdomainDefs.IDomainPseudoDivisionDefs.R</a> [variable, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.IdomainDefs.modp">Pdiv.IdomainDefs.modp</a> [definition, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.IdomainDefs.scalp">Pdiv.IdomainDefs.scalp</a> [definition, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> -<a href="mathcomp.algebra.polydiv.html#9c1ccd33b816bf809c7479082caaf63e">_ %= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> -<a href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad">_ %| _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> -<a href="mathcomp.algebra.polydiv.html#538b21ac9fb9938cd88200e5780e8f9d">_ %% _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> -<a href="mathcomp.algebra.polydiv.html#6a276cc55c6f28b3ec69a3618ce07a9c">_ %/ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> +<a href="mathcomp.algebra.polydiv.html#952776a2e27e0a80427a97e8cd81c9aa">_ %= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> +<a href="mathcomp.algebra.polydiv.html#64fc6df2b95b79b2107dd5d7f2014b97">_ %| _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> +<a href="mathcomp.algebra.polydiv.html#d8832071e7663562cc14f17c6edf99dc">_ %% _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> +<a href="mathcomp.algebra.polydiv.html#72a0c853cc9a32bb5fdc8a920a96e7c6">_ %/ _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.IdomainMonic">Pdiv.IdomainMonic</a> [module, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.IdomainMonic.divpE">Pdiv.IdomainMonic.divpE</a> [lemma, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> <a href="mathcomp.algebra.polydiv.html#Pdiv.IdomainMonic.divpp">Pdiv.IdomainMonic.divpp</a> [lemma, in <a href="mathcomp.algebra.polydiv.html">mathcomp.algebra.polydiv</a>]<br/> @@ -1233,6 +1233,7 @@ <a href="mathcomp.fingroup.perm.html#PermDef.perm">PermDef.perm</a> [definition, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.fingroup.perm.html#PermDef.permE">PermDef.permE</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.fingroup.perm.html#permE">permE</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permEl">permEl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.fingroup.automorphism.html#PermIn">PermIn</a> [section, in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/> <a href="mathcomp.fingroup.automorphism.html#PermIn.A">PermIn.A</a> [variable, in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/> <a href="mathcomp.fingroup.automorphism.html#PermIn.f">PermIn.f</a> [variable, in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/> @@ -1244,10 +1245,24 @@ <a href="mathcomp.fingroup.perm.html#permKV">permKV</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.fingroup.perm.html#permM">permM</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.fingroup.perm.html#permP">permP</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permP">permP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permPl">permPl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permPr">permPr</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perms">perms</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#PermSeq">PermSeq</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#PermSeq.T">PermSeq.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perms_rec">perms_rec</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.fingroup.perm.html#PermutationParity">PermutationParity</a> [section, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.fingroup.perm.html#PermutationParity.T">PermutationParity.T</a> [variable, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permutations">permutations</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#Permutations">Permutations</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permutationsE">permutationsE</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permutationsErot">permutationsErot</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permutations_all_uniq">permutations_all_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#permutations_uniq">permutations_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#Permutations.cons_permsE">Permutations.cons_permsE</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#Permutations.permsP">Permutations.permsP</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#Permutations.T">Permutations.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.fingroup.perm.html#permX">permX</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.ssreflect.path.html#perm_sortP">perm_sortP</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#perm_sort">perm_sort</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> @@ -1286,45 +1301,73 @@ <a href="mathcomp.fingroup.automorphism.html#perm_in_on">perm_in_on</a> [lemma, in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/> <a href="mathcomp.fingroup.automorphism.html#perm_in">perm_in</a> [definition, in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/> <a href="mathcomp.fingroup.automorphism.html#perm_in_inj">perm_in_inj</a> [lemma, in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_undup_count">perm_undup_count</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_iotaP">perm_eq_iotaP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_undup_count">perm_undup_count</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_iotaP">perm_eq_iotaP</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_consP">perm_eq_consP</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_nilP">perm_eq_nilP</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_small">perm_eq_small</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_all">perm_eq_all</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_flatten">perm_eq_flatten</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_rev">perm_eq_rev</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_uniq">perm_eq_uniq</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_mem">perm_eq_mem</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_size">perm_eq_size</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_trans">perm_eq_trans</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_sym">perm_eq_sym</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eq_refl">perm_eq_refl</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eqlE">perm_eqlE</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eqrP">perm_eqrP</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eqlP">perm_eqlP</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_eqP">perm_eqP</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_permutations">perm_permutations</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_count_undup">perm_count_undup</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_tseq">perm_tseq</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_tally_seq">perm_tally_seq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_tally">perm_tally</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_flatten">perm_flatten</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_sumn">perm_sumn</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_iotaP">perm_iotaP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_pmap">perm_pmap</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_map_inj">perm_map_inj</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_map">perm_map</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_to_subseq">perm_to_subseq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_to_rem">perm_to_rem</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_eqr">perm_eqr</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_eql">perm_eql</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_uniq">perm_eq_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_undup">perm_undup</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_uniq">perm_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_small">perm_eq_small</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_size">perm_eq_size</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_all">perm_eq_all</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_mem">perm_eq_mem</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_small_eq">perm_small_eq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_all">perm_all</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_has">perm_has</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_consP">perm_consP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_nilP">perm_nilP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_mem">perm_mem</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_size">perm_size</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_filterC">perm_filterC</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_filter">perm_filter</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_rev">perm_eq_rev</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_rev">perm_rev</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_rotr">perm_rotr</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_rot">perm_rot</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_rcons">perm_rcons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_catCA">perm_catCA</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_catAC">perm_catAC</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_cat">perm_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_catr">perm_catr</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_cat2r">perm_cat2r</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_cons">perm_cons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_catl">perm_catl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_cat2l">perm_cat2l</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_catC">perm_catC</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eqrP">perm_eqrP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eqlP">perm_eqlP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eqlE">perm_eqlE</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_eqr">perm_eqr</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_eql">perm_eql</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_trans">perm_eq_trans</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_sym">perm_eq_sym</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eq_refl">perm_eq_refl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#perm_eqP">perm_eqP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_trans">perm_trans</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_sym">perm_sym</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#perm_refl">perm_refl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#perm_eq">perm_eq</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.solvable.abelian.html#perm_eq_abelian_type">perm_eq_abelian_type</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> <a href="mathcomp.fingroup.action.html#perm_faithful">perm_faithful</a> [lemma, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#perm_act1P">perm_act1P</a> [lemma, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#perm_mact">perm_mact</a> [lemma, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#perm_big">perm_big</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.fingroup.perm.html#perm1">perm1</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#PervasiveMonoids">PervasiveMonoids</a> [section, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.algebra.ssrint.html#pexpIrz">pexpIrz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> @@ -1471,8 +1514,7 @@ <a href="mathcomp.ssreflect.prime.html#pi_max_pdiv">pi_max_pdiv</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#pi_pdiv">pi_pdiv</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#pi_of">pi_of</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#pi_wrapped_arg">pi_wrapped_arg</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#pi_unwrapped_arg">pi_unwrapped_arg</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#pi_arg">pi_arg</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.algebra.ring_quotient.html#pi_invr">pi_invr</a> [lemma, in <a href="mathcomp.algebra.ring_quotient.html">mathcomp.algebra.ring_quotient</a>]<br/> <a href="mathcomp.algebra.ring_quotient.html#pi_unitr">pi_unitr</a> [lemma, in <a href="mathcomp.algebra.ring_quotient.html">mathcomp.algebra.ring_quotient</a>]<br/> <a href="mathcomp.algebra.ring_quotient.html#pi_is_multiplicative">pi_is_multiplicative</a> [lemma, in <a href="mathcomp.algebra.ring_quotient.html">mathcomp.algebra.ring_quotient</a>]<br/> @@ -1497,9 +1539,6 @@ <a href="mathcomp.ssreflect.prime.html#pi'_p'nat">pi'_p'nat</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#Pi.E">Pi.E</a> [definition, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#Pi.f">Pi.f</a> [definition, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#PlainTheory">PlainTheory</a> [section, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#PlainTheory.aT">PlainTheory.aT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> -<a href="mathcomp.ssreflect.finfun.html#PlainTheory.rT">PlainTheory.rT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#plusE">plusE</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.seq.html#pmap">pmap</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#Pmap">Pmap</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1510,6 +1549,7 @@ <a href="mathcomp.ssreflect.seq.html#pmapS_filter">pmapS_filter</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#pmap_sub_uniq">pmap_sub_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#pmap_uniq">pmap_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#pmap_cat">pmap_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#pmap_filter">pmap_filter</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#Pmap.aT">Pmap.aT</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#Pmap.f">Pmap.f</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1573,7 +1613,7 @@ <a href="mathcomp.algebra.poly.html#polyCK">polyCK</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#PolyCompose">PolyCompose</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#PolyCompose.R">PolyCompose.R</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#3963cf6cfb5e8b54483fc37af1a6db2d">_ \Po _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#b0797d7dde7f681ae2ccab57f6c6a648">_ \Po _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#polyC_inv">polyC_inv</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#polyC_exp">polyC_exp</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#polyC_multiplicative">polyC_multiplicative</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -1588,7 +1628,6 @@ <a href="mathcomp.algebra.poly.html#polyC0">polyC0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#polyC1">polyC1</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.polydiv.html">polydiv</a> [library]<br/> -<a href="mathcomp.field.closed_field.html#polyF">polyF</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.algebra.poly.html#PolyK">PolyK</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#polynomial">polynomial</a> [record, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#Polynomial">Polynomial</a> [constructor, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -1608,18 +1647,24 @@ <a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverAdd.kS">PolynomialTheory.PolyOverAdd.kS</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverAdd.S">PolynomialTheory.PolyOverAdd.S</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverRing">PolynomialTheory.PolyOverRing</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverRing.kS">PolynomialTheory.PolyOverRing.kS</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverRing.ringS">PolynomialTheory.PolyOverRing.ringS</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverRing.S">PolynomialTheory.PolyOverRing.S</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverSemiring">PolynomialTheory.PolyOverSemiring</a> [section, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverSemiring.kS">PolynomialTheory.PolyOverSemiring.kS</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverSemiring.ringS">PolynomialTheory.PolyOverSemiring.ringS</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#PolynomialTheory.PolyOverSemiring.S">PolynomialTheory.PolyOverSemiring.S</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#PolynomialTheory.R">PolynomialTheory.R</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#a942f71ef6e79d81ec1823e85631f18b">_ ^`N ( _ ) (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#d70b9939cc44180cb082f293ad21429e">_ ^` ( _ ) (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#2bd58b7fc104e5befe2ca1fecac7c623">_ .-primitive_root (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#7f47f838360ae58c7843275633f83d07">_ .-unity_root (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#baba25a9b511327d163a4abdecb45e2a">_ .[ _ ] (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#9caef92b6a6aef95cfbc4574952f8622">_ ^`</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#4a33fe2dad4a62417624cbe36418a1fe">_ %:P</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#a1cd5f9ec97ed6af469b2ab6da5bc5f9">'X</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#5342abeecce868539daa879464131e00">'X^ _</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> -<a href="mathcomp.algebra.poly.html#b1bd1c5077c681a8a37f97ae835f4bf6">\poly_ ( _ < _ ) _</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#31951e7a9fd9bb5a774892066ed196b8">_ ^`N ( _ ) (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#1d9676bfa4392b4098c6e293b2d018ad">_ ^` ( _ ) (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#945c56de5ff21a9d3435445d11cfa3f2">_ .-primitive_root (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#cf34ca2293616a3eea81a8b32110ecbc">_ .-unity_root (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#03fafeca1d8bb8af3cc89a1830d3996b">_ .[ _ ] (ring_scope)</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#cfa0aa09962cfc701c4777d893c479b4">_ ^`</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#728a2917ff59e46e3f0e4d98ed9ea172">_ %:P</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#78f0b7e9c087664de9d653df6828ab64">'X</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#72573bab7b99d99443b6173a7515ef0d">'X^ _</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#27fd9446e6d344308e4e6554f93d6b3b">\poly_ ( _ < _ ) _</a> [notation, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#polynomial_choiceMixin">polynomial_choiceMixin</a> [definition, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#polynomial_eqMixin">polynomial_eqMixin</a> [definition, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#Polynomial.R">Polynomial.R</a> [variable, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -1679,7 +1724,6 @@ <a href="mathcomp.algebra.ssrint.html#PolyZintRing">PolyZintRing</a> [section, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.ssrint.html#PolyZintRing.R">PolyZintRing.R</a> [variable, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.field.separable.html#poly_square_freeP">poly_square_freeP</a> [lemma, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> -<a href="mathcomp.field.countalg.html#poly_countMixin">poly_countMixin</a> [definition, in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#poly_rV_is_linear">poly_rV_is_linear</a> [lemma, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#poly_rV_K">poly_rV_K</a> [lemma, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#poly_rV">poly_rV</a> [definition, in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> @@ -1709,6 +1753,7 @@ <a href="mathcomp.algebra.poly.html#poly_key">poly_key</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#poly_expanded_def">poly_expanded_def</a> [definition, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#poly_nil">poly_nil</a> [definition, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#poly_countMixin">poly_countMixin</a> [definition, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#poly_of">poly_of</a> [definition, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#poly_inj">poly_inj</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#poly0Vpos">poly0Vpos</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -1780,6 +1825,7 @@ <a href="mathcomp.ssreflect.binomial.html#predn_exp">predn_exp</a> [lemma, in <a href="mathcomp.ssreflect.binomial.html">mathcomp.ssreflect.binomial</a>]<br/> <a href="mathcomp.algebra.ssrint.html#predn_int">predn_int</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.ssreflect.finset.html#predOfType">predOfType</a> [abbreviation, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> +<a href="mathcomp.ssreflect.ssrbool.html#PredType">PredType</a> [definition, in <a href="mathcomp.ssreflect.ssrbool.html">mathcomp.ssreflect.ssrbool</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#predT_subset">predT_subset</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#predU1">predU1</a> [definition, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#predU1l">predU1l</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> @@ -1894,7 +1940,23 @@ <a href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing.charRp">PrimeChar.PrimeCharRing.charRp</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing.natrFp">PrimeChar.PrimeCharRing.natrFp</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> <a href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing.R0">PrimeChar.PrimeCharRing.R0</a> [variable, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> -<a href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f">_ *p: _</a> [notation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> +<a href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65">_ *p: _</a> [notation, in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux">PrimeDecompAux</a> [module, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.add_totient_factor">PrimeDecompAux.add_totient_factor</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.add_divisors">PrimeDecompAux.add_divisors</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.cons_pfactor">PrimeDecompAux.cons_pfactor</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.edivn2">PrimeDecompAux.edivn2</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.edivn2P">PrimeDecompAux.edivn2P</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.elogn2">PrimeDecompAux.elogn2</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.elogn2P">PrimeDecompAux.elogn2P</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.Elogn2Spec">PrimeDecompAux.Elogn2Spec</a> [constructor, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.elogn2_spec">PrimeDecompAux.elogn2_spec</a> [inductive, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.ifnz">PrimeDecompAux.ifnz</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.ifnzP">PrimeDecompAux.ifnzP</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.IfnzPos">PrimeDecompAux.IfnzPos</a> [constructor, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.IfnzZero">PrimeDecompAux.IfnzZero</a> [constructor, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#PrimeDecompAux.ifnz_spec">PrimeDecompAux.ifnz_spec</a> [inductive, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#7be21c16e780ad44531793b3b1a9d2d1">_ ^? _ :: _ (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.algebra.zmodp.html#PrimeField">PrimeField</a> [section, in <a href="mathcomp.algebra.zmodp.html">mathcomp.algebra.zmodp</a>]<br/> <a href="mathcomp.algebra.zmodp.html#PrimeField.F_prime.p_pr">PrimeField.F_prime.p_pr</a> [variable, in <a href="mathcomp.algebra.zmodp.html">mathcomp.algebra.zmodp</a>]<br/> <a href="mathcomp.algebra.zmodp.html#PrimeField.F_prime">PrimeField.F_prime</a> [section, in <a href="mathcomp.algebra.zmodp.html">mathcomp.algebra.zmodp</a>]<br/> @@ -1923,7 +1985,7 @@ <a href="mathcomp.ssreflect.prime.html#prime_nt_dvdP">prime_nt_dvdP</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#prime_decomp_correct">prime_decomp_correct</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#prime_decomp">prime_decomp</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#07e1474be9be12fc282844ac903c103e">[ rec _ , _ , _ , _ , _ , _ ]</a> [notation, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> +<a href="mathcomp.ssreflect.prime.html#074ed9914305c17e256e36efda3fbe58">[ rec _ , _ , _ , _ , _ , _ ]</a> [notation, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#prime_decomp_rec">prime_decomp_rec</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#prime_decomp">prime_decomp</a> [section, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.algebra.ring_quotient.html#prime_idealrM">prime_idealrM</a> [lemma, in <a href="mathcomp.algebra.ring_quotient.html">mathcomp.algebra.ring_quotient</a>]<br/> @@ -2060,7 +2122,6 @@ <a href="mathcomp.character.classfun.html#prod_cfunE">prod_cfunE</a> [lemma, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#prod_nat_const_nat">prod_nat_const_nat</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#prod_nat_const">prod_nat_const</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#prod_eqMixin">prod_eqMixin</a> [definition, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#prod_t_correct">prod_t_correct</a> [lemma, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#prod_tuple">prod_tuple</a> [definition, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.field.falgebra.html#prod0v">prod0v</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> @@ -2268,7 +2329,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> @@ -2300,14 +2361,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> @@ -2332,7 +2393,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -2364,7 +2425,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> @@ -2396,7 +2457,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> @@ -2428,7 +2489,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> @@ -2460,7 +2521,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> @@ -2492,7 +2553,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -2524,14 +2585,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> @@ -2556,7 +2617,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> @@ -2588,7 +2649,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> @@ -2620,7 +2681,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> @@ -2652,14 +2713,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> @@ -2684,7 +2745,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> |