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_lemma_E.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_lemma_E.html')
| -rw-r--r-- | docs/htmldoc/index_lemma_E.html | 100 |
1 files changed, 51 insertions, 49 deletions
diff --git a/docs/htmldoc/index_lemma_E.html b/docs/htmldoc/index_lemma_E.html index 0e90174..a86d944 100644 --- a/docs/htmldoc/index_lemma_E.html +++ b/docs/htmldoc/index_lemma_E.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="lemma_E"></a><h2>E (lemma)</h2> @@ -471,7 +471,6 @@ <a href="mathcomp.ssreflect.div.html#edivnP">edivnP</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> <a href="mathcomp.ssreflect.div.html#edivn_def">edivn_def</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> <a href="mathcomp.ssreflect.div.html#edivn_eq">edivn_eq</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#edivn2P">edivn2P</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.div.html#egcdnP">egcdnP</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> <a href="mathcomp.algebra.intdiv.html#egcdzP">egcdzP</a> [in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/> <a href="mathcomp.ssreflect.div.html#egcd0n">egcd0n</a> [in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> @@ -480,7 +479,6 @@ <a href="mathcomp.algebra.mxpoly.html#eigenvalue_root_min">eigenvalue_root_min</a> [in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxpoly.html#eigenvalue_root_char">eigenvalue_root_char</a> [in <a href="mathcomp.algebra.mxpoly.html">mathcomp.algebra.mxpoly</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eigenvalue_map">eigenvalue_map</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#elogn2P">elogn2P</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.solvable.cyclic.html#eltmE">eltmE</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> <a href="mathcomp.solvable.cyclic.html#eltmM">eltmM</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> <a href="mathcomp.solvable.cyclic.html#eltm_id">eltm_id</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> @@ -578,13 +576,16 @@ <a href="mathcomp.character.mxrepresentation.html#eqg_mx_irr">eqg_mx_irr</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#eqg_mx_faithful">eqg_mx_faithful</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#eqg_repr_proof">eqg_repr_proof</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.algebra.interval.html#eqitvP">eqitvP</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> <a href="mathcomp.algebra.vector.html#eqlfunP">eqlfunP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#eqlfun_inP">eqlfun_inP</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#eqMixin">eqMixin</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#eqmodE">eqmodE</a> [in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#eqmodP">eqmodP</a> [in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmxMfree">eqmxMfree</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmxMfull">eqmxMfull</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmxMr">eqmxMr</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> +<a href="mathcomp.algebra.mxalgebra.html#eqmxMunitP">eqmxMunitP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmxP">eqmxP</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#eqmx_semisimple">eqmx_semisimple</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#eqmx_iso">eqmx_iso</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -697,10 +698,13 @@ <a href="mathcomp.ssreflect.generic_quotient.html#eq_quot_countMixin">eq_quot_countMixin</a> [in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#eq_op_trans">eq_op_trans</a> [in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#eq_lock">eq_lock</a> [in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> +<a href="mathcomp.algebra.interval.html#eq_itv_boundP">eq_itv_boundP</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> +<a href="mathcomp.ssreflect.tuple.html#eq_mktuple">eq_mktuple</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#eq_from_tnth">eq_from_tnth</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> <a href="mathcomp.algebra.matrix.html#eq_block_mx">eq_block_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#eq_col_mx">eq_col_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.algebra.matrix.html#eq_row_mx">eq_row_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#eq_mx">eq_mx</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.fingroup.automorphism.html#eq_Aut">eq_Aut</a> [in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/> <a href="mathcomp.character.character.html#eq_subZnat_irr">eq_subZnat_irr</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> <a href="mathcomp.character.character.html#eq_addZ_irr">eq_addZ_irr</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> @@ -710,11 +714,15 @@ <a href="mathcomp.character.character.html#eq_irr_mem_classP">eq_irr_mem_classP</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> <a href="mathcomp.character.character.html#eq_sum_nth_irr">eq_sum_nth_irr</a> [in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> <a href="mathcomp.solvable.extremal.html#eq_Mod8_D8">eq_Mod8_D8</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#eq_in_allpairs">eq_in_allpairs</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#eq_in_allpairs_dep">eq_in_allpairs_dep</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#eq_allpairs">eq_allpairs</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_from_flatten_shape">eq_from_flatten_shape</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_mkseq">eq_mkseq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_pmap">eq_pmap</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_in_map">eq_in_map</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_map">eq_map</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#eq_uniq">eq_uniq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_all_r">eq_all_r</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_has_r">eq_has_r</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_in_has">eq_in_has</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -774,11 +782,11 @@ <a href="mathcomp.ssreflect.ssrnat.html#eq_ex_minn">eq_ex_minn</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#eq_leq">eq_leq</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.algebra.poly.html#eq_map_poly">eq_map_poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#eq_poly">eq_poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#eq_prim_root_expr">eq_prim_root_expr</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_bigmax">eq_bigmax</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_bigmax_cond">eq_bigmax_cond</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_big_idem">eq_big_idem</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.bigop.html#eq_big_perm">eq_big_perm</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_big_idx">eq_big_idx</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_big_idx_seq">eq_big_idx_seq</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_big_nat">eq_big_nat</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> @@ -787,6 +795,8 @@ <a href="mathcomp.ssreflect.bigop.html#eq_bigr">eq_bigr</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_bigl">eq_bigl</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_big_op">eq_big_op</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#eq_ffun">eq_ffun</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#eq_dffun">eq_dffun</a> [in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#eq_Tagged">eq_Tagged</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#eq_tag">eq_tag</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#eq_frel">eq_frel</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> @@ -828,19 +838,12 @@ <a href="mathcomp.ssreflect.finset.html#eq_in_imset">eq_in_imset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#eq_imset">eq_imset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#eq_preimset">eq_preimset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> +<a href="mathcomp.ssreflect.finset.html#eq_finset">eq_finset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.prime.html#Euclid_dvdX">Euclid_dvdX</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#Euclid_dvd1">Euclid_dvd1</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#Euclid_dvdM">Euclid_dvdM</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.solvable.cyclic.html#Euler_exp_totient">Euler_exp_totient</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#eval_mxmodule">eval_mxmodule</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_poly1">eval_poly1</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_poly_mulM">eval_poly_mulM</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_natmulpT">eval_natmulpT</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_opppT">eval_opppT</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_mulpT">eval_mulpT</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_sumpT">eval_sumpT</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_amulXnT">eval_amulXnT</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_lift">eval_lift</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.ssreflect.prime.html#even_prime">even_prime</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#exchange_big_nat">exchange_big_nat</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#exchange_big_dep_nat">exchange_big_dep_nat</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> @@ -852,6 +855,7 @@ <a href="mathcomp.solvable.jordanholder.html#exists_acomps">exists_acomps</a> [in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> <a href="mathcomp.solvable.jordanholder.html#exists_comps">exists_comps</a> [in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#exists_eq_inP">exists_eq_inP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#exists_inPP">exists_inPP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#exists_inP">exists_inP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#exists_eqP">exists_eqP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.algebra.matrix.html#expand_det_col">expand_det_col</a> [in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> @@ -999,6 +1003,7 @@ <a href="mathcomp.solvable.extremal.html#Extremal.Grp">Extremal.Grp</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> <a href="mathcomp.solvable.extremal.html#Extremal.gtype_key">Extremal.gtype_key</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> <a href="mathcomp.solvable.extremal.html#extremal2_structure">extremal2_structure</a> [in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#extremumP">extremumP</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.solvable.hall.html#ext_coprime_quotient_cent">ext_coprime_quotient_cent</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> <a href="mathcomp.solvable.hall.html#ext_coprime_Hall_subset">ext_coprime_Hall_subset</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> <a href="mathcomp.solvable.hall.html#ext_norm_conj_cent">ext_norm_conj_cent</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> @@ -1008,9 +1013,6 @@ <a href="mathcomp.ssreflect.ssrnat.html#ex_maxnP">ex_maxnP</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#ex_maxn_subproof">ex_maxn_subproof</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#ex_minnP">ex_minnP</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.field.closed_field.html#ex_elim_qf">ex_elim_qf</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#ex_elim_seq_qf">ex_elim_seq_qf</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#ex_elim_seqP">ex_elim_seqP</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#ex_mingroup">ex_mingroup</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#ex_maxgroup">ex_maxgroup</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.ssreflect.finset.html#ex_maxset">ex_maxset</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> @@ -1046,7 +1048,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> @@ -1078,14 +1080,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> @@ -1110,7 +1112,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -1142,7 +1144,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> @@ -1174,7 +1176,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> @@ -1206,7 +1208,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> @@ -1238,7 +1240,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> @@ -1270,7 +1272,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -1302,14 +1304,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> @@ -1334,7 +1336,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> @@ -1366,7 +1368,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> @@ -1398,7 +1400,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> @@ -1430,14 +1432,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> @@ -1462,7 +1464,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> |