From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/index_global_S.html | 117 +++++++++++++++++++++++----------------
1 file changed, 68 insertions(+), 49 deletions(-)
(limited to 'docs/htmldoc/index_global_S.html')
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 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
| Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,7 +463,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
S
@@ -798,9 +798,11 @@
Sequences.SubPred.s12 [variable, in mathcomp.ssreflect.seq]
Sequences.T [variable, in mathcomp.ssreflect.seq]
Sequences.x0 [variable, in mathcomp.ssreflect.seq]
-_ ++ _ (seq_scope) [notation, in mathcomp.ssreflect.seq]
+_ ++ _ (seq_scope) [notation, in mathcomp.ssreflect.seq]
seqv_sub_adjoin [lemma, in mathcomp.field.falgebra]
seq_tnthP [lemma, in mathcomp.ssreflect.tuple]
+seq_eqclass [definition, in mathcomp.ssreflect.seq]
+seq_ind2 [lemma, in mathcomp.ssreflect.seq]
seq_countMixin [definition, in mathcomp.ssreflect.choice]
seq_choiceMixin [lemma, in mathcomp.ssreflect.choice]
seq_of_optK [lemma, in mathcomp.ssreflect.choice]
@@ -819,7 +821,6 @@
seq_iso_L [definition, in mathcomp.solvable.burnside_app]
seq1_basis [lemma, in mathcomp.algebra.vector]
seq1_free [lemma, in mathcomp.algebra.vector]
-seq2_ind [lemma, in mathcomp.ssreflect.seq]
SeriesDefs [section, in mathcomp.solvable.nilpotent]
SeriesDefs.A [variable, in mathcomp.solvable.nilpotent]
SeriesDefs.gT [variable, in mathcomp.solvable.nilpotent]
@@ -1084,10 +1085,10 @@
simple_compsP [lemma, in mathcomp.solvable.jordanholder]
simple_maxnormal [lemma, in mathcomp.solvable.gseries]
simple_sol_prime [lemma, in mathcomp.solvable.maximal]
+SimplRel [definition, in mathcomp.ssreflect.ssrbool]
+simpl_rel [definition, in mathcomp.ssreflect.ssrbool]
+simpl_pred_sortE [lemma, in mathcomp.ssreflect.ssrbool]
size [definition, in mathcomp.ssreflect.seq]
-sizeT [definition, in mathcomp.field.closed_field]
-sizeTP [lemma, in mathcomp.field.closed_field]
-sizeT_qf [lemma, in mathcomp.field.closed_field]
sizeY [definition, in mathcomp.algebra.polyXY]
sizeYE [lemma, in mathcomp.algebra.polyXY]
sizeY_mulX [lemma, in mathcomp.algebra.polyXY]
@@ -1109,7 +1110,10 @@
size_poly_XaY [lemma, in mathcomp.algebra.polyXY]
size_Cyclotomic [lemma, in mathcomp.field.cyclotomic]
size_cyclotomic [lemma, in mathcomp.field.cyclotomic]
+size_permutations [lemma, in mathcomp.ssreflect.seq]
+size_tally_seq [lemma, in mathcomp.ssreflect.seq]
size_allpairs [lemma, in mathcomp.ssreflect.seq]
+size_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
size_reshape [lemma, in mathcomp.ssreflect.seq]
size_flatten [lemma, in mathcomp.ssreflect.seq]
size_zip [lemma, in mathcomp.ssreflect.seq]
@@ -1150,6 +1154,10 @@
size_comp_poly2 [lemma, in mathcomp.algebra.poly]
size_comp_poly [lemma, in mathcomp.algebra.poly]
size_exp [lemma, in mathcomp.algebra.poly]
+size_prod_eq1 [lemma, in mathcomp.algebra.poly]
+size_prod_seq_eq1 [lemma, in mathcomp.algebra.poly]
+size_mul_eq1 [lemma, in mathcomp.algebra.poly]
+size_prod_seq [lemma, in mathcomp.algebra.poly]
size_prod [lemma, in mathcomp.algebra.poly]
size_Cmul [lemma, in mathcomp.algebra.poly]
size_scale [lemma, in mathcomp.algebra.poly]
@@ -1181,6 +1189,7 @@
size_addl [lemma, in mathcomp.algebra.poly]
size_add [lemma, in mathcomp.algebra.poly]
size_opp [lemma, in mathcomp.algebra.poly]
+size_polyC_leq1 [lemma, in mathcomp.algebra.poly]
size_poly1P [lemma, in mathcomp.algebra.poly]
size_poly_gt0 [lemma, in mathcomp.algebra.poly]
size_poly_leq0P [lemma, in mathcomp.algebra.poly]
@@ -1257,12 +1266,15 @@
sol_der1_proper [lemma, in mathcomp.solvable.nilpotent]
SomeHall [section, in mathcomp.solvable.sylow]
SomeHall.gT [variable, in mathcomp.solvable.sylow]
+Some_inj [lemma, in mathcomp.ssreflect.ssrfun]
sop [definition, in mathcomp.solvable.burnside_app]
sop_morph [lemma, in mathcomp.solvable.burnside_app]
sop_spec [lemma, in mathcomp.solvable.burnside_app]
sop_inj [lemma, in mathcomp.solvable.burnside_app]
sort [definition, in mathcomp.ssreflect.path]
sorted [definition, in mathcomp.ssreflect.path]
+sorted_le_nth [lemma, in mathcomp.ssreflect.path]
+sorted_lt_nth [lemma, in mathcomp.ssreflect.path]
sorted_uniq [lemma, in mathcomp.ssreflect.path]
sorted_filter [lemma, in mathcomp.ssreflect.path]
sorted_divisors_ltn [lemma, in mathcomp.ssreflect.prime]
@@ -1347,8 +1359,8 @@
SplittingField.Exports [module, in mathcomp.field.galois]
SplittingField.Exports.SplittingFieldType [abbreviation, in mathcomp.field.galois]
SplittingField.Exports.splittingFieldType [abbreviation, in mathcomp.field.galois]
-[ splittingFieldType _ of _ ] (form_scope) [notation, in mathcomp.field.galois]
-[ splittingFieldType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.galois]
+[ splittingFieldType _ of _ ] (form_scope) [notation, in mathcomp.field.galois]
+[ splittingFieldType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.galois]
SplittingField.FalgType [definition, in mathcomp.field.galois]
SplittingField.fieldExtType [definition, in mathcomp.field.galois]
SplittingField.fieldType [definition, in mathcomp.field.galois]
@@ -1453,6 +1465,7 @@
StrongJordanHolder.rT [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.to [variable, in mathcomp.solvable.jordanholder]
strong_Primitive_Element_Theorem [lemma, in mathcomp.field.separable]
+Sub [abbreviation, in mathcomp.ssreflect.eqtype]
Sub [projection, in mathcomp.ssreflect.eqtype]
subact [definition, in mathcomp.fingroup.action]
SubAction [section, in mathcomp.fingroup.action]
@@ -1540,7 +1553,7 @@
SubFieldExtension.z [variable, in mathcomp.field.fieldext]
SubFieldExtension.z0 [variable, in mathcomp.field.fieldext]
SubFieldExtension.z0Ciota [variable, in mathcomp.field.fieldext]
-_ ^iota (ring_scope) [notation, in mathcomp.field.fieldext]
+_ ^iota (ring_scope) [notation, in mathcomp.field.fieldext]
SubFieldExtType [definition, in mathcomp.field.fieldext]
subfield_closed [lemma, in mathcomp.field.fieldext]
subFinGroupMixin [definition, in mathcomp.fingroup.fingroup]
@@ -1683,6 +1696,9 @@
SubP [lemma, in mathcomp.ssreflect.eqtype]
subq [definition, in mathcomp.algebra.rat]
subq_ge0 [lemma, in mathcomp.algebra.rat]
+subr_lersif0 [definition, in mathcomp.algebra.interval]
+subr_lersif0r [lemma, in mathcomp.algebra.interval]
+subr_lersifr0 [lemma, in mathcomp.algebra.interval]
subseq [definition, in mathcomp.ssreflect.seq]
Subseq [section, in mathcomp.ssreflect.seq]
subseqP [lemma, in mathcomp.ssreflect.seq]
@@ -1693,8 +1709,8 @@
subseq_uniq [lemma, in mathcomp.ssreflect.seq]
subseq_rcons [lemma, in mathcomp.ssreflect.seq]
subseq_cons [lemma, in mathcomp.ssreflect.seq]
-subseq_refl [lemma, in mathcomp.ssreflect.seq]
subseq_trans [lemma, in mathcomp.ssreflect.seq]
+subseq_refl [lemma, in mathcomp.ssreflect.seq]
Subseq.T [variable, in mathcomp.ssreflect.seq]
subseq0 [lemma, in mathcomp.ssreflect.seq]
subseries_repr [definition, in mathcomp.character.mxrepresentation]
@@ -1761,8 +1777,10 @@
SubType [constructor, in mathcomp.ssreflect.eqtype]
SubType [section, in mathcomp.ssreflect.eqtype]
SubType.P [variable, in mathcomp.ssreflect.eqtype]
-SubType.sT [variable, in mathcomp.ssreflect.eqtype]
SubType.T [variable, in mathcomp.ssreflect.eqtype]
+SubType.Theory [section, in mathcomp.ssreflect.eqtype]
+SubType.Theory.insub_eq_aux [variable, in mathcomp.ssreflect.eqtype]
+SubType.Theory.sT [variable, in mathcomp.ssreflect.eqtype]
subUset [lemma, in mathcomp.ssreflect.finset]
subUsetP [lemma, in mathcomp.ssreflect.finset]
subV [abbreviation, in mathcomp.algebra.vector]
@@ -1949,13 +1967,14 @@
summx_sub [lemma, in mathcomp.algebra.mxalgebra]
sumMz [lemma, in mathcomp.algebra.ssrint]
sumn [definition, in mathcomp.ssreflect.seq]
+sumnE [lemma, in mathcomp.ssreflect.bigop]
sumn_flatten [lemma, in mathcomp.ssreflect.seq]
sumn_rev [lemma, in mathcomp.ssreflect.seq]
+sumn_rot [lemma, in mathcomp.ssreflect.seq]
sumn_rcons [lemma, in mathcomp.ssreflect.seq]
sumn_count [lemma, in mathcomp.ssreflect.seq]
sumn_cat [lemma, in mathcomp.ssreflect.seq]
sumn_nseq [lemma, in mathcomp.ssreflect.seq]
-sumpT [definition, in mathcomp.field.closed_field]
sumsmxMr [lemma, in mathcomp.algebra.mxalgebra]
sumsmxMr_gen [lemma, in mathcomp.algebra.mxalgebra]
sumsmxS [lemma, in mathcomp.algebra.mxalgebra]
@@ -2000,7 +2019,7 @@
sum_eq [definition, in mathcomp.ssreflect.eqtype]
sum_totient_dvd [lemma, in mathcomp.solvable.cyclic]
sum_ncycle_totient [lemma, in mathcomp.solvable.cyclic]
-sum_nat_dep_const [lemma, in mathcomp.ssreflect.finset]
+sum_nat_cond_const [lemma, in mathcomp.ssreflect.finset]
sum1dep_card [lemma, in mathcomp.ssreflect.finset]
sum1_size [lemma, in mathcomp.ssreflect.bigop]
sum1_count [lemma, in mathcomp.ssreflect.bigop]
@@ -2074,8 +2093,8 @@
SymAltDef [section, in mathcomp.solvable.alt]
SymAltDef.n [variable, in mathcomp.solvable.alt]
SymAltDef.T [variable, in mathcomp.solvable.alt]
-'Alt_T [notation, in mathcomp.solvable.alt]
-'Sym_T [notation, in mathcomp.solvable.alt]
+'Alt_T [notation, in mathcomp.solvable.alt]
+'Sym_T [notation, in mathcomp.solvable.alt]
symplectic_type_group_structure [lemma, in mathcomp.solvable.extremal]
Sym_trans [lemma, in mathcomp.solvable.alt]
s0 [definition, in mathcomp.solvable.burnside_app]
@@ -2153,7 +2172,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -2185,14 +2204,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -2217,7 +2236,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -2249,7 +2268,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -2281,7 +2300,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -2313,7 +2332,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -2345,7 +2364,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -2377,7 +2396,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -2409,14 +2428,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -2441,7 +2460,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -2473,7 +2492,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -2505,7 +2524,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -2537,14 +2556,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -2569,7 +2588,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
--
cgit v1.2.3