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_E.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_E.html')
| -rw-r--r-- | docs/htmldoc/index_global_E.html | 152 |
1 files changed, 82 insertions, 70 deletions
diff --git a/docs/htmldoc/index_global_E.html b/docs/htmldoc/index_global_E.html index b3054e3..bf7c6c8 100644 --- a/docs/htmldoc/index_global_E.html +++ b/docs/htmldoc/index_global_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="global_E"></a><h2>E </h2> @@ -478,8 +478,6 @@ <a href="mathcomp.ssreflect.div.html#edivn_eq">edivn_eq</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> <a href="mathcomp.ssreflect.div.html#edivn_spec">edivn_spec</a> [inductive, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> <a href="mathcomp.ssreflect.div.html#edivn_rec">edivn_rec</a> [definition, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#edivn2">edivn2</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#edivn2P">edivn2P</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.div.html#egcdn">egcdn</a> [definition, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> <a href="mathcomp.ssreflect.div.html#egcdnP">egcdnP</a> [lemma, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> <a href="mathcomp.ssreflect.div.html#EgcdnSpec">EgcdnSpec</a> [constructor, in <a href="mathcomp.ssreflect.div.html">mathcomp.ssreflect.div</a>]<br/> @@ -537,10 +535,6 @@ <a href="mathcomp.ssreflect.bigop.html#Elim3.R1">Elim3.R1</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Elim3.R2">Elim3.R2</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#Elim3.R3">Elim3.R3</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#elogn2">elogn2</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#elogn2P">elogn2P</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#Elogn2Spec">Elogn2Spec</a> [constructor, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#elogn2_spec">elogn2_spec</a> [inductive, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.solvable.cyclic.html#eltm">eltm</a> [definition, in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> <a href="mathcomp.solvable.cyclic.html#Eltm">Eltm</a> [section, in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> <a href="mathcomp.solvable.cyclic.html#eltmE">eltmE</a> [lemma, in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> @@ -625,6 +619,11 @@ <a href="mathcomp.character.mxrepresentation.html#envelop_mx1">envelop_mx1</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#envelop_mx_id">envelop_mx_id</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqAllPairs">EqAllPairs</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#EqAllPairsDep">EqAllPairsDep</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#EqAllPairsDep.R">EqAllPairsDep.R</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#EqAllPairsDep.S">EqAllPairsDep.S</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#EqAllPairsDep.T">EqAllPairsDep.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#EqAllPairs.R">EqAllPairs.R</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqAllPairs.S">EqAllPairs.S</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqAllPairs.T">EqAllPairs.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.field.algnum.html#eqAmod">eqAmod</a> [definition, in <a href="mathcomp.field.algnum.html">mathcomp.field.algnum</a>]<br/> @@ -719,6 +718,8 @@ <a href="mathcomp.fingroup.quotient.html#EqIso.G">EqIso.G</a> [variable, in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> <a href="mathcomp.fingroup.quotient.html#EqIso.gT">EqIso.gT</a> [variable, in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> <a href="mathcomp.fingroup.quotient.html#EqIso.H">EqIso.H</a> [variable, in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/> +<a href="mathcomp.algebra.interval.html#eqitv">eqitv</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> +<a href="mathcomp.algebra.interval.html#eqitvP">eqitvP</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> <a href="mathcomp.algebra.vector.html#eqlfunP">eqlfunP</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#eqlfun_inP">eqlfun_inP</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqMap">EqMap</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -732,12 +733,14 @@ <a href="mathcomp.ssreflect.seq.html#EqMask">EqMask</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqMask.n0">EqMask.n0</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqMask.T">EqMask.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#eqMixin">eqMixin</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#eqmodE">eqmodE</a> [lemma, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#eqmodP">eqmodP</a> [lemma, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmx">eqmx</a> [definition, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmxMfree">eqmxMfree</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmxMfull">eqmxMfull</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmxMr">eqmxMr</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> +<a href="mathcomp.algebra.mxalgebra.html#eqmxMunitP">eqmxMunitP</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#eqmxP">eqmxP</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#eqmx_semisimple">eqmx_semisimple</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#eqmx_iso">eqmx_iso</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -830,7 +833,6 @@ <a href="mathcomp.ssreflect.seq.html#eqseqE">eqseqE</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eqseqP">eqseqP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eqseq_rot">eqseq_rot</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#eqseq_class">eqseq_class</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eqseq_rcons">eqseq_rcons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eqseq_cat">eqseq_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eqseq_cons">eqseq_cons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -838,11 +840,16 @@ <a href="mathcomp.ssreflect.seq.html#EqSeq.EqIn.a1">EqSeq.EqIn.a1</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqSeq.EqIn.a2">EqSeq.EqIn.a2</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqSeq.Filters">EqSeq.Filters</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#EqSeq.Filters.A">EqSeq.Filters.A</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqSeq.Filters.a">EqSeq.Filters.a</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#EqSeq.Filters.aP">EqSeq.Filters.aP</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#EqSeq.Filters.s">EqSeq.Filters.s</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqSeq.inE">EqSeq.inE</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqSeq.n0">EqSeq.n0</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqSeq.T">EqSeq.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#EqSeq.x0">EqSeq.x0</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#ab51245ad31bdb97452f83c8b446e9f3">'all_ _</a> [notation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#c7a8000a6cd687fa747a1b027fdad1c9">'has_ _</a> [notation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#eqSS">eqSS</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.finset.html#eqsVneq">eqsVneq</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finfun.html#EqTheory">EqTheory</a> [section, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> @@ -870,13 +877,12 @@ <a href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqMixin">Equality.Exports.EqMixin</a> [abbreviation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType">Equality.Exports.EqType</a> [abbreviation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType">Equality.Exports.eqType</a> [abbreviation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2">[ eqType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#ea28a4d33dfb78a62dc4071e70f3d5db">[ eqType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#78287ce0666bcaa587a668e46d5a01f3">[ eqMixin of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c">[ eqType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#81ec7b251f2007d39c38861f2d0a8253">[ eqType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#537cd9d3521b1a9c172f81d0628e3d40">[ eqMixin of _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Equality.Mixin">Equality.Mixin</a> [constructor, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Equality.mixin_of">Equality.mixin_of</a> [record, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Equality.op">Equality.op</a> [projection, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#Equality.pack">Equality.pack</a> [definition, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Equality.Pack">Equality.Pack</a> [constructor, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Equality.sort">Equality.sort</a> [projection, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Equality.type">Equality.type</a> [record, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> @@ -986,10 +992,14 @@ <a href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class_of">eq_quot_class_of</a> [record, in <a href="mathcomp.ssreflect.generic_quotient.html">mathcomp.ssreflect.generic_quotient</a>]<br/> <a href="mathcomp.ssreflect.generic_quotient.html#eq_quot_mixin_of">eq_quot_mixin_of</a> [definition, 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> [lemma, 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> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> +<a href="mathcomp.algebra.interval.html#eq_itv_bound">eq_itv_bound</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> +<a href="mathcomp.ssreflect.tuple.html#eq_mktuple">eq_mktuple</a> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> +<a href="mathcomp.algebra.matrix.html#eq_mx">eq_mx</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.fingroup.automorphism.html#eq_Aut">eq_Aut</a> [lemma, 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> [lemma, 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> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/> @@ -999,11 +1009,15 @@ <a href="mathcomp.character.character.html#eq_irr_mem_classP">eq_irr_mem_classP</a> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#eq_allpairs">eq_allpairs</a> [lemma, 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> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_mkseq">eq_mkseq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_pmap">eq_pmap</a> [lemma, 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> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#eq_map">eq_map</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#eq_uniq">eq_uniq</a> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1063,11 +1077,12 @@ <a href="mathcomp.ssreflect.ssrnat.html#eq_ex_minn">eq_ex_minn</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#eq_leq">eq_leq</a> [lemma, 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> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#eq_poly">eq_poly</a> [lemma, 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> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#eq_big_perm">eq_big_perm</a> [abbreviation, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_bigmax">eq_bigmax</a> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> @@ -1076,6 +1091,8 @@ <a href="mathcomp.ssreflect.bigop.html#eq_bigr">eq_bigr</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#eq_bigl">eq_bigl</a> [lemma, 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> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#eq_ffun">eq_ffun</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> +<a href="mathcomp.ssreflect.finfun.html#eq_dffun">eq_dffun</a> [lemma, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#eq_Tagged">eq_Tagged</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#eq_tag">eq_tag</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#eq_comparable">eq_comparable</a> [definition, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> @@ -1119,6 +1136,7 @@ <a href="mathcomp.ssreflect.finset.html#eq_in_imset">eq_in_imset</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#eq_imset">eq_imset</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#eq_preimset">eq_preimset</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> +<a href="mathcomp.ssreflect.finset.html#eq_finset">eq_finset</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#Eq0NotPos">Eq0NotPos</a> [constructor, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.character.mxabelem.html#ErV">ErV</a> [abbreviation, in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/> <a href="mathcomp.ssreflect.prime.html#Euclid_dvdX">Euclid_dvdX</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> @@ -1128,16 +1146,6 @@ <a href="mathcomp.character.mxrepresentation.html#eval">eval</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.algebra.polyXY.html#eval">eval</a> [abbreviation, in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#eval_mxmodule">eval_mxmodule</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_bigmul">eval_bigmul</a> [abbreviation, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_poly1">eval_poly1</a> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, 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> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#eval_poly">eval_poly</a> [definition, 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> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#ev_ax">ev_ax</a> [abbreviation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#exchange_big_nat">exchange_big_nat</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> @@ -1150,6 +1158,7 @@ <a href="mathcomp.solvable.jordanholder.html#exists_acomps">exists_acomps</a> [lemma, in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> <a href="mathcomp.solvable.jordanholder.html#exists_comps">exists_comps</a> [lemma, 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> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#exists_inPP">exists_inPP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#exists_inP">exists_inP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#exists_eqP">exists_eqP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#ExMaxn">ExMaxn</a> [section, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> @@ -1527,15 +1536,23 @@ <a href="mathcomp.solvable.extremal.html#Extremal.gtype_key">Extremal.gtype_key</a> [lemma, in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> <a href="mathcomp.solvable.extremal.html#extremal2">extremal2</a> [definition, in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> <a href="mathcomp.solvable.extremal.html#extremal2_structure">extremal2_structure</a> [lemma, in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.ArgMinMax">Extrema.ArgMinMax</a> [section, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.ArgMinMax.F">Extrema.ArgMinMax.F</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.ArgMinMax.I">Extrema.ArgMinMax.I</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.ArgMinMax.i0">Extrema.ArgMinMax.i0</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.ArgMinMax.P">Extrema.ArgMinMax.P</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.ArgMinMax.Pi0">Extrema.ArgMinMax.Pi0</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#Extrema.arg_pred">Extrema.arg_pred</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#Extrema.exFP">Extrema.exFP</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#Extrema.F">Extrema.F</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#Extrema.FP">Extrema.FP</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#Extrema.FP_F">Extrema.FP_F</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#Extrema.I">Extrema.I</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#Extrema.i0">Extrema.i0</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#Extrema.P">Extrema.P</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> -<a href="mathcomp.ssreflect.fintype.html#Extrema.Pi0">Extrema.Pi0</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.Extremum">Extrema.Extremum</a> [section, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.Extremum.ord_total">Extrema.Extremum.ord_total</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.Extremum.ord_trans">Extrema.Extremum.ord_trans</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.Extremum.ord_refl">Extrema.Extremum.ord_refl</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#Extrema.Extremum.Pi0">Extrema.Extremum.Pi0</a> [variable, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#be936861724bff9e36682d789ae9b182">[ arg[ _ ]_( _ < _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#331f7185e81731ef2b1eb9cef1aed0ab">[ arg[ _ ]_( _ < _ in _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#d2709c05b8893fbfce6113b58d692e11">[ arg[ _ ]_( _ < _ | _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#extremum">extremum</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> +<a href="mathcomp.ssreflect.fintype.html#extremumP">extremumP</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#ExtremumSpec">ExtremumSpec</a> [constructor, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#extremum_spec">extremum_spec</a> [inductive, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.fingroup.gproduct.html#ExtSdprodm">ExtSdprodm</a> [section, in <a href="mathcomp.fingroup.gproduct.html">mathcomp.fingroup.gproduct</a>]<br/> @@ -1563,11 +1580,6 @@ <a href="mathcomp.ssreflect.ssrnat.html#ex_minnP">ex_minnP</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#ex_minn_spec">ex_minn_spec</a> [inductive, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#ex_minn">ex_minn</a> [definition, 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> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#ex_elim">ex_elim</a> [definition, 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> [lemma, 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> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#ex_elim_seq">ex_elim_seq</a> [definition, 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> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#ex_maxgroup">ex_maxgroup</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.ssreflect.finset.html#ex_maxset">ex_maxset</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> @@ -1610,7 +1622,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> @@ -1642,14 +1654,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> @@ -1674,7 +1686,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -1706,7 +1718,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> @@ -1738,7 +1750,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> @@ -1770,7 +1782,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> @@ -1802,7 +1814,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> @@ -1834,7 +1846,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -1866,14 +1878,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> @@ -1898,7 +1910,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> @@ -1930,7 +1942,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> @@ -1962,7 +1974,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> @@ -1994,14 +2006,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> @@ -2026,7 +2038,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> |