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_A.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_A.html')
| -rw-r--r-- | docs/htmldoc/index_global_A.html | 130 |
1 files changed, 75 insertions, 55 deletions
diff --git a/docs/htmldoc/index_global_A.html b/docs/htmldoc/index_global_A.html index c576f97..543ecdb 100644 --- a/docs/htmldoc/index_global_A.html +++ b/docs/htmldoc/index_global_A.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_A"></a><h2>A </h2> @@ -548,6 +548,7 @@ <a href="mathcomp.solvable.abelian.html#abelian_type_abelem">abelian_type_abelem</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> <a href="mathcomp.solvable.abelian.html#abelian_type_homocyclic">abelian_type_homocyclic</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> <a href="mathcomp.solvable.abelian.html#abelian_rank1_cyclic">abelian_rank1_cyclic</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> +<a href="mathcomp.solvable.abelian.html#abelian_type_pgroup">abelian_type_pgroup</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> <a href="mathcomp.solvable.abelian.html#abelian_structure">abelian_structure</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> <a href="mathcomp.solvable.abelian.html#abelian_type_sorted">abelian_type_sorted</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> <a href="mathcomp.solvable.abelian.html#abelian_type_gt1">abelian_type_gt1</a> [lemma, in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/> @@ -564,11 +565,6 @@ <a href="mathcomp.solvable.nilpotent.html#abelian_nil">abelian_nil</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#abelian_gen">abelian_gen</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#abelian1">abelian1</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> -<a href="mathcomp.field.closed_field.html#abstrX">abstrX</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#abstrXP">abstrXP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#abstrX_bigmul">abstrX_bigmul</a> [abbreviation, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#abstrX_mulM">abstrX_mulM</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#abstrX1">abstrX1</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.algebra.ssrint.html#Absz">Absz</a> [section, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.ssrint.html#absz">absz</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.ssrint.html#abszE">abszE</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> @@ -609,7 +605,7 @@ <a href="mathcomp.fingroup.action.html#ActBy.R">ActBy.R</a> [variable, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#ActBy.rT">ActBy.rT</a> [variable, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#ActBy.to">ActBy.to</a> [variable, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> -<a href="mathcomp.fingroup.action.html#5bf4be35f60d187d626f827a16d8a344"><[nRA]> (action_scope)</a> [notation, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> +<a href="mathcomp.fingroup.action.html#6cb933d23b4e1104f17518736b51639e"><[nRA]> (action_scope)</a> [notation, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#actCJ">actCJ</a> [lemma, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#actCJV">actCJV</a> [lemma, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#action">action</a> [record, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> @@ -713,9 +709,12 @@ <a href="mathcomp.algebra.mxalgebra.html#addmx_sub">addmx_sub</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#addn">addn</a> [definition, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#addnA">addnA</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#addnABC">addnABC</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#addnAC">addnAC</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#addnACA">addnACA</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#addnBA">addnBA</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#addnBAC">addnBAC</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#addnBCA">addnBCA</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#addnC">addnC</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#addnCA">addnCA</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#addnE">addnE</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> @@ -797,8 +796,6 @@ <a href="mathcomp.algebra.vector.html#addv_idPl">addv_idPl</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#addv0">addv0</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.ssralg.html#add_pair">add_pair</a> [definition, in <a href="mathcomp.algebra.ssralg.html">mathcomp.algebra.ssralg</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#add_totient_factor">add_totient_factor</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> -<a href="mathcomp.ssreflect.prime.html#add_divisors">add_divisors</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#add_sub_fact_mod">add_sub_fact_mod</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.algebra.vector.html#add_lfunE">add_lfunE</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#add_lfun">add_lfun</a> [definition, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> @@ -1007,10 +1004,10 @@ <a href="mathcomp.field.algC.html#Algebraics.Exports.nCdivE">Algebraics.Exports.nCdivE</a> [lemma, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Exports.truncC">Algebraics.Exports.truncC</a> [definition, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Exports.zCdivE">Algebraics.Exports.zCdivE</a> [lemma, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> -<a href="mathcomp.field.algC.html#7f475a8fd3a16c1e4c806088f6e9e378">_ != _ %[mod _ ] (C_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> -<a href="mathcomp.field.algC.html#ad6c1a2e0c593edef8f546c6caff1370">_ == _ %[mod _ ] (C_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> -<a href="mathcomp.field.algC.html#9a2f23320469c9d2a314bb86625d5b32">_ %| _ (C_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> -<a href="mathcomp.field.algC.html#a934248f68ba79f0e05555e2d6d19837">_ %| _ (C_expanded_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> +<a href="mathcomp.field.algC.html#aa7ae38652f54e25821cb36f6decd206">_ != _ %[mod _ ] (C_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> +<a href="mathcomp.field.algC.html#074a766e3f389a9f57f000217fe90e0f">_ == _ %[mod _ ] (C_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> +<a href="mathcomp.field.algC.html#a8acd6561c48edf701c07f3c736659e7">_ %| _ (C_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> +<a href="mathcomp.field.algC.html#b94462522df85d8cb1d6596b03c49ad4">_ %| _ (C_expanded_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Implementation">Algebraics.Implementation</a> [module, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Implementation.add">Algebraics.Implementation.add</a> [definition, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Implementation.addA">Algebraics.Implementation.addA</a> [lemma, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> @@ -1086,7 +1083,7 @@ <a href="mathcomp.field.algC.html#Algebraics.Internals.QtoCm">Algebraics.Internals.QtoCm</a> [abbreviation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Internals.ZtoC">Algebraics.Internals.ZtoC</a> [abbreviation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Internals.ZtoQ">Algebraics.Internals.ZtoQ</a> [abbreviation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> -<a href="mathcomp.field.algC.html#b8bcd15d62c4408371f497f2c85500e1">_ ^* (ring_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> +<a href="mathcomp.field.algC.html#7741402f392eb0ebcaf84d97b9f2940d">_ ^* (ring_scope)</a> [notation, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Specification">Algebraics.Specification</a> [module, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Specification.algebraic">Algebraics.Specification.algebraic</a> [axiom, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#Algebraics.Specification.choiceMixin">Algebraics.Specification.choiceMixin</a> [axiom, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> @@ -1130,20 +1127,40 @@ <a href="mathcomp.field.algebraics_fundamentals.html#alg_integral">alg_integral</a> [lemma, in <a href="mathcomp.field.algebraics_fundamentals.html">mathcomp.field.algebraics_fundamentals</a>]<br/> <a href="mathcomp.ssreflect.seq.html#all">all</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.all.all.html">all</a> [library]<br/> +<a href="mathcomp.ssreflect.seq.html#AllIff">AllIff</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllIffConj">AllIffConj</a> [constructor, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#allP">allP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#allpairs">allpairs</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#AllPairs">AllPairs</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsDep">AllPairsDep</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsDep.R">AllPairsDep.R</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsDep.S">AllPairsDep.S</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsDep.S'">AllPairsDep.S'</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsDep.T">AllPairsDep.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsDep.T'">AllPairsDep.T'</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsNonDep">AllPairsNonDep</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsNonDep.f">AllPairsNonDep.f</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsNonDep.R">AllPairsNonDep.R</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsNonDep.S">AllPairsNonDep.S</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#AllPairsNonDep.T">AllPairsNonDep.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#allpairsP">allpairsP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#allpairsPdep">allpairsPdep</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#allpairs_tupleP">allpairs_tupleP</a> [lemma, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> <a href="mathcomp.ssreflect.seq.html#allpairs_uniq">allpairs_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#allpairs_f">allpairs_f</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#allpairs_uniq_dep">allpairs_uniq_dep</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#allpairs_catr">allpairs_catr</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#allpairs_f_dep">allpairs_f_dep</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#allpairs_mapr">allpairs_mapr</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#allpairs_mapl">allpairs_mapl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#allpairs_cat">allpairs_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#AllPairs.f">AllPairs.f</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#AllPairs.R">AllPairs.R</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#AllPairs.S">AllPairs.S</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#AllPairs.T">AllPairs.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#allpairs_dep">allpairs_dep</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#allPn">allPn</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#allPP">allPP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#all_tnthP">all_tnthP</a> [lemma, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#all_iffP">all_iffP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#all_iffLR">all_iffLR</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#all_iff">all_iff</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#all_iff_and">all_iff_and</a> [inductive, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#all_map">all_map</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#all_nthP">all_nthP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#all_pred1_nseq">all_pred1_nseq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1169,6 +1186,8 @@ <a href="mathcomp.field.all_field.html">all_field</a> [library]<br/> <a href="mathcomp.algebra.all_algebra.html">all_algebra</a> [library]<br/> <a href="mathcomp.ssreflect.all_ssreflect.html">all_ssreflect</a> [library]<br/> +<a href="mathcomp.ssreflect.seq.html#all2">all2</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#all2E">all2E</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.solvable.alt.html#Alt">Alt</a> [definition, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> <a href="mathcomp.solvable.alt.html">alt</a> [library]<br/> <a href="mathcomp.solvable.alt.html#Alt_trans">Alt_trans</a> [lemma, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> @@ -1189,11 +1208,12 @@ <a href="mathcomp.field.falgebra.html#amulr">amulr</a> [definition, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#amulr_is_lrmorphism">amulr_is_lrmorphism</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.field.falgebra.html#amulr_inj">amulr_inj</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> -<a href="mathcomp.field.closed_field.html#amulXnT">amulXnT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#And">And</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#annihilator_mxP">annihilator_mxP</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#annihilator_mx">annihilator_mx</a> [definition, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#anti_leq">anti_leq</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#anti_mono">anti_mono</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#anti_mono_in">anti_mono_in</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.fingroup.perm.html#aperm">aperm</a> [definition, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.fingroup.perm.html#apermE">apermE</a> [lemma, in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/> <a href="mathcomp.solvable.alt.html#aperm_faithful">aperm_faithful</a> [lemma, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> @@ -1359,7 +1379,7 @@ <a href="mathcomp.character.vcharacter.html#AutVchar.G">AutVchar.G</a> [variable, in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> <a href="mathcomp.character.vcharacter.html#AutVchar.gT">AutVchar.gT</a> [variable, in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> <a href="mathcomp.character.vcharacter.html#AutVchar.u">AutVchar.u</a> [variable, in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> -<a href="mathcomp.character.vcharacter.html#be5305d56f36ee4c1e372520d7a4ee16">_ ^u</a> [notation, in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> +<a href="mathcomp.character.vcharacter.html#1dcc5e3b162744dbc296c5f466424c6d">_ ^u</a> [notation, in <a href="mathcomp.character.vcharacter.html">mathcomp.character.vcharacter</a>]<br/> <a href="mathcomp.field.algC.html#aut_Crat">aut_Crat</a> [lemma, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#aut_Cint">aut_Cint</a> [lemma, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> <a href="mathcomp.field.algC.html#aut_Cnat">aut_Cnat</a> [lemma, in <a href="mathcomp.field.algC.html">mathcomp.field.algC</a>]<br/> @@ -1430,7 +1450,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> @@ -1462,14 +1482,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> @@ -1494,7 +1514,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -1526,7 +1546,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> @@ -1558,7 +1578,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> @@ -1590,7 +1610,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> @@ -1622,7 +1642,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> @@ -1654,7 +1674,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -1686,14 +1706,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> @@ -1718,7 +1738,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> @@ -1750,7 +1770,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> @@ -1782,7 +1802,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> @@ -1814,14 +1834,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> @@ -1846,7 +1866,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> |