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_S.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_S.html')
| -rw-r--r-- | docs/htmldoc/index_global_S.html | 117 |
1 files changed, 68 insertions, 49 deletions
diff --git a/docs/htmldoc/index_global_S.html b/docs/htmldoc/index_global_S.html index 5b32caa..41ea302 100644 --- a/docs/htmldoc/index_global_S.html +++ b/docs/htmldoc/index_global_S.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_S"></a><h2>S </h2> @@ -798,9 +798,11 @@ <a href="mathcomp.ssreflect.seq.html#Sequences.SubPred.s12">Sequences.SubPred.s12</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#Sequences.T">Sequences.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#Sequences.x0">Sequences.x0</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#bd3a6d577cd53c0f76a9a712a1be8f7b">_ ++ _ (seq_scope)</a> [notation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#cfcff6535a1677da2547b032de3120ce">_ ++ _ (seq_scope)</a> [notation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.field.falgebra.html#seqv_sub_adjoin">seqv_sub_adjoin</a> [lemma, in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#seq_tnthP">seq_tnthP</a> [lemma, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#seq_eqclass">seq_eqclass</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#seq_ind2">seq_ind2</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.choice.html#seq_countMixin">seq_countMixin</a> [definition, in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> <a href="mathcomp.ssreflect.choice.html#seq_choiceMixin">seq_choiceMixin</a> [lemma, in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> <a href="mathcomp.ssreflect.choice.html#seq_of_optK">seq_of_optK</a> [lemma, in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> @@ -819,7 +821,6 @@ <a href="mathcomp.solvable.burnside_app.html#seq_iso_L">seq_iso_L</a> [definition, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.algebra.vector.html#seq1_basis">seq1_basis</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#seq1_free">seq1_free</a> [lemma, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#seq2_ind">seq2_ind</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.solvable.nilpotent.html#SeriesDefs">SeriesDefs</a> [section, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> <a href="mathcomp.solvable.nilpotent.html#SeriesDefs.A">SeriesDefs.A</a> [variable, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> <a href="mathcomp.solvable.nilpotent.html#SeriesDefs.gT">SeriesDefs.gT</a> [variable, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> @@ -1084,10 +1085,10 @@ <a href="mathcomp.solvable.jordanholder.html#simple_compsP">simple_compsP</a> [lemma, in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> <a href="mathcomp.solvable.gseries.html#simple_maxnormal">simple_maxnormal</a> [lemma, in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> <a href="mathcomp.solvable.maximal.html#simple_sol_prime">simple_sol_prime</a> [lemma, in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> +<a href="mathcomp.ssreflect.ssrbool.html#SimplRel">SimplRel</a> [definition, in <a href="mathcomp.ssreflect.ssrbool.html">mathcomp.ssreflect.ssrbool</a>]<br/> +<a href="mathcomp.ssreflect.ssrbool.html#simpl_rel">simpl_rel</a> [definition, in <a href="mathcomp.ssreflect.ssrbool.html">mathcomp.ssreflect.ssrbool</a>]<br/> +<a href="mathcomp.ssreflect.ssrbool.html#simpl_pred_sortE">simpl_pred_sortE</a> [lemma, in <a href="mathcomp.ssreflect.ssrbool.html">mathcomp.ssreflect.ssrbool</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size">size</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.field.closed_field.html#sizeT">sizeT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#sizeTP">sizeTP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#sizeT_qf">sizeT_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.algebra.polyXY.html#sizeY">sizeY</a> [definition, in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.algebra.polyXY.html#sizeYE">sizeYE</a> [lemma, in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.algebra.polyXY.html#sizeY_mulX">sizeY_mulX</a> [lemma, in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> @@ -1109,7 +1110,10 @@ <a href="mathcomp.algebra.polyXY.html#size_poly_XaY">size_poly_XaY</a> [lemma, in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.field.cyclotomic.html#size_Cyclotomic">size_Cyclotomic</a> [lemma, in <a href="mathcomp.field.cyclotomic.html">mathcomp.field.cyclotomic</a>]<br/> <a href="mathcomp.field.cyclotomic.html#size_cyclotomic">size_cyclotomic</a> [lemma, in <a href="mathcomp.field.cyclotomic.html">mathcomp.field.cyclotomic</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#size_permutations">size_permutations</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#size_tally_seq">size_tally_seq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size_allpairs">size_allpairs</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#size_allpairs_dep">size_allpairs_dep</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size_reshape">size_reshape</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size_flatten">size_flatten</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size_zip">size_zip</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1150,6 +1154,10 @@ <a href="mathcomp.algebra.poly.html#size_comp_poly2">size_comp_poly2</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_comp_poly">size_comp_poly</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_exp">size_exp</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_prod_eq1">size_prod_eq1</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_prod_seq_eq1">size_prod_seq_eq1</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_mul_eq1">size_mul_eq1</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_prod_seq">size_prod_seq</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_prod">size_prod</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_Cmul">size_Cmul</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_scale">size_scale</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -1181,6 +1189,7 @@ <a href="mathcomp.algebra.poly.html#size_addl">size_addl</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_add">size_add</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_opp">size_opp</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_polyC_leq1">size_polyC_leq1</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_poly1P">size_poly1P</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_poly_gt0">size_poly_gt0</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_poly_leq0P">size_poly_leq0P</a> [lemma, in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -1257,12 +1266,15 @@ <a href="mathcomp.solvable.nilpotent.html#sol_der1_proper">sol_der1_proper</a> [lemma, in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> <a href="mathcomp.solvable.sylow.html#SomeHall">SomeHall</a> [section, in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> <a href="mathcomp.solvable.sylow.html#SomeHall.gT">SomeHall.gT</a> [variable, in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> +<a href="mathcomp.ssreflect.ssrfun.html#Some_inj">Some_inj</a> [lemma, in <a href="mathcomp.ssreflect.ssrfun.html">mathcomp.ssreflect.ssrfun</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#sop">sop</a> [definition, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#sop_morph">sop_morph</a> [lemma, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#sop_spec">sop_spec</a> [lemma, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#sop_inj">sop_inj</a> [lemma, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.ssreflect.path.html#sort">sort</a> [definition, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#sorted">sorted</a> [definition, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> +<a href="mathcomp.ssreflect.path.html#sorted_le_nth">sorted_le_nth</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> +<a href="mathcomp.ssreflect.path.html#sorted_lt_nth">sorted_lt_nth</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#sorted_uniq">sorted_uniq</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#sorted_filter">sorted_filter</a> [lemma, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.prime.html#sorted_divisors_ltn">sorted_divisors_ltn</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> @@ -1347,8 +1359,8 @@ <a href="mathcomp.field.galois.html#SplittingField.Exports">SplittingField.Exports</a> [module, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> <a href="mathcomp.field.galois.html#SplittingField.Exports.SplittingFieldType">SplittingField.Exports.SplittingFieldType</a> [abbreviation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> <a href="mathcomp.field.galois.html#SplittingField.Exports.splittingFieldType">SplittingField.Exports.splittingFieldType</a> [abbreviation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.field.galois.html#99357846948d73ae425c8713e468bc5c">[ splittingFieldType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> -<a href="mathcomp.field.galois.html#201f8b6ebe31f6a88a3d073a45335fc2">[ splittingFieldType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> +<a href="mathcomp.field.galois.html#d8a72e9d06179f0980f622a9988083f5">[ splittingFieldType _ of _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> +<a href="mathcomp.field.galois.html#205eef6999e87a23b5f8f5c2e8fec9d8">[ splittingFieldType _ of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> <a href="mathcomp.field.galois.html#SplittingField.FalgType">SplittingField.FalgType</a> [definition, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> <a href="mathcomp.field.galois.html#SplittingField.fieldExtType">SplittingField.fieldExtType</a> [definition, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> <a href="mathcomp.field.galois.html#SplittingField.fieldType">SplittingField.fieldType</a> [definition, in <a href="mathcomp.field.galois.html">mathcomp.field.galois</a>]<br/> @@ -1453,6 +1465,7 @@ <a href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.rT">StrongJordanHolder.rT</a> [variable, in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> <a href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.to">StrongJordanHolder.to</a> [variable, in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> <a href="mathcomp.field.separable.html#strong_Primitive_Element_Theorem">strong_Primitive_Element_Theorem</a> [lemma, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#Sub">Sub</a> [abbreviation, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#Sub">Sub</a> [projection, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.fingroup.action.html#subact">subact</a> [definition, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#SubAction">SubAction</a> [section, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> @@ -1540,7 +1553,7 @@ <a href="mathcomp.field.fieldext.html#SubFieldExtension.z">SubFieldExtension.z</a> [variable, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#SubFieldExtension.z0">SubFieldExtension.z0</a> [variable, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#SubFieldExtension.z0Ciota">SubFieldExtension.z0Ciota</a> [variable, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> -<a href="mathcomp.field.fieldext.html#32025d8baa64cf6d146609ad9813fb0e">_ ^iota (ring_scope)</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> +<a href="mathcomp.field.fieldext.html#b90c6ceb09b006f6d3aeda21af2787b9">_ ^iota (ring_scope)</a> [notation, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#SubFieldExtType">SubFieldExtType</a> [definition, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.field.fieldext.html#subfield_closed">subfield_closed</a> [lemma, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.fingroup.fingroup.html#subFinGroupMixin">subFinGroupMixin</a> [definition, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/> @@ -1683,6 +1696,9 @@ <a href="mathcomp.ssreflect.eqtype.html#SubP">SubP</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.algebra.rat.html#subq">subq</a> [definition, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> <a href="mathcomp.algebra.rat.html#subq_ge0">subq_ge0</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> +<a href="mathcomp.algebra.interval.html#subr_lersif0">subr_lersif0</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> +<a href="mathcomp.algebra.interval.html#subr_lersif0r">subr_lersif0r</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> +<a href="mathcomp.algebra.interval.html#subr_lersifr0">subr_lersifr0</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq">subseq</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#Subseq">Subseq</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseqP">subseqP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1693,8 +1709,8 @@ <a href="mathcomp.ssreflect.seq.html#subseq_uniq">subseq_uniq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq_rcons">subseq_rcons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq_cons">subseq_cons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_refl">subseq_refl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq_trans">subseq_trans</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#subseq_refl">subseq_refl</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#Subseq.T">Subseq.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq0">subseq0</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#subseries_repr">subseries_repr</a> [definition, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> @@ -1761,8 +1777,10 @@ <a href="mathcomp.ssreflect.eqtype.html#SubType">SubType</a> [constructor, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#SubType">SubType</a> [section, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#SubType.P">SubType.P</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> -<a href="mathcomp.ssreflect.eqtype.html#SubType.sT">SubType.sT</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#SubType.T">SubType.T</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#SubType.Theory">SubType.Theory</a> [section, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#SubType.Theory.insub_eq_aux">SubType.Theory.insub_eq_aux</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> +<a href="mathcomp.ssreflect.eqtype.html#SubType.Theory.sT">SubType.Theory.sT</a> [variable, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.ssreflect.finset.html#subUset">subUset</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#subUsetP">subUsetP</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.algebra.vector.html#subV">subV</a> [abbreviation, in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> @@ -1949,13 +1967,14 @@ <a href="mathcomp.algebra.mxalgebra.html#summx_sub">summx_sub</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.ssrint.html#sumMz">sumMz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn">sumn</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#sumnE">sumnE</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_flatten">sumn_flatten</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_rev">sumn_rev</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#sumn_rot">sumn_rot</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_rcons">sumn_rcons</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_count">sumn_count</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_cat">sumn_cat</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_nseq">sumn_nseq</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.field.closed_field.html#sumpT">sumpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#sumsmxMr">sumsmxMr</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#sumsmxMr_gen">sumsmxMr_gen</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#sumsmxS">sumsmxS</a> [lemma, in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> @@ -2000,7 +2019,7 @@ <a href="mathcomp.ssreflect.eqtype.html#sum_eq">sum_eq</a> [definition, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.solvable.cyclic.html#sum_totient_dvd">sum_totient_dvd</a> [lemma, in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> <a href="mathcomp.solvable.cyclic.html#sum_ncycle_totient">sum_ncycle_totient</a> [lemma, in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#sum_nat_dep_const">sum_nat_dep_const</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> +<a href="mathcomp.ssreflect.finset.html#sum_nat_cond_const">sum_nat_cond_const</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#sum1dep_card">sum1dep_card</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#sum1_size">sum1_size</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#sum1_count">sum1_count</a> [lemma, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> @@ -2074,8 +2093,8 @@ <a href="mathcomp.solvable.alt.html#SymAltDef">SymAltDef</a> [section, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> <a href="mathcomp.solvable.alt.html#SymAltDef.n">SymAltDef.n</a> [variable, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> <a href="mathcomp.solvable.alt.html#SymAltDef.T">SymAltDef.T</a> [variable, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> -<a href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748">'Alt_T</a> [notation, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> -<a href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003">'Sym_T</a> [notation, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> +<a href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8">'Alt_T</a> [notation, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> +<a href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d">'Sym_T</a> [notation, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> <a href="mathcomp.solvable.extremal.html#symplectic_type_group_structure">symplectic_type_group_structure</a> [lemma, in <a href="mathcomp.solvable.extremal.html">mathcomp.solvable.extremal</a>]<br/> <a href="mathcomp.solvable.alt.html#Sym_trans">Sym_trans</a> [lemma, in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#s0">s0</a> [definition, in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> @@ -2153,7 +2172,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> @@ -2185,14 +2204,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> @@ -2217,7 +2236,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -2249,7 +2268,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> @@ -2281,7 +2300,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> @@ -2313,7 +2332,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> @@ -2345,7 +2364,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> @@ -2377,7 +2396,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -2409,14 +2428,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> @@ -2441,7 +2460,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> @@ -2473,7 +2492,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> @@ -2505,7 +2524,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> @@ -2537,14 +2556,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> @@ -2569,7 +2588,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> |