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_E.html | 152 +++++++++++++++++++++------------------ 1 file changed, 82 insertions(+), 70 deletions(-) (limited to 'docs/htmldoc/index_global_E.html') 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 @@ -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)

E

@@ -478,8 +478,6 @@ edivn_eq [lemma, in mathcomp.ssreflect.div]
edivn_spec [inductive, in mathcomp.ssreflect.div]
edivn_rec [definition, in mathcomp.ssreflect.div]
-edivn2 [definition, in mathcomp.ssreflect.prime]
-edivn2P [lemma, in mathcomp.ssreflect.prime]
egcdn [definition, in mathcomp.ssreflect.div]
egcdnP [lemma, in mathcomp.ssreflect.div]
EgcdnSpec [constructor, in mathcomp.ssreflect.div]
@@ -537,10 +535,6 @@ Elim3.R1 [variable, in mathcomp.ssreflect.bigop]
Elim3.R2 [variable, in mathcomp.ssreflect.bigop]
Elim3.R3 [variable, in mathcomp.ssreflect.bigop]
-elogn2 [definition, in mathcomp.ssreflect.prime]
-elogn2P [lemma, in mathcomp.ssreflect.prime]
-Elogn2Spec [constructor, in mathcomp.ssreflect.prime]
-elogn2_spec [inductive, in mathcomp.ssreflect.prime]
eltm [definition, in mathcomp.solvable.cyclic]
Eltm [section, in mathcomp.solvable.cyclic]
eltmE [lemma, in mathcomp.solvable.cyclic]
@@ -625,6 +619,11 @@ envelop_mx1 [lemma, in mathcomp.character.mxrepresentation]
envelop_mx_id [lemma, in mathcomp.character.mxrepresentation]
EqAllPairs [section, in mathcomp.ssreflect.seq]
+EqAllPairsDep [section, in mathcomp.ssreflect.seq]
+EqAllPairsDep.R [variable, in mathcomp.ssreflect.seq]
+EqAllPairsDep.S [variable, in mathcomp.ssreflect.seq]
+EqAllPairsDep.T [variable, in mathcomp.ssreflect.seq]
+EqAllPairs.R [variable, in mathcomp.ssreflect.seq]
EqAllPairs.S [variable, in mathcomp.ssreflect.seq]
EqAllPairs.T [variable, in mathcomp.ssreflect.seq]
eqAmod [definition, in mathcomp.field.algnum]
@@ -719,6 +718,8 @@ EqIso.G [variable, in mathcomp.fingroup.quotient]
EqIso.gT [variable, in mathcomp.fingroup.quotient]
EqIso.H [variable, in mathcomp.fingroup.quotient]
+eqitv [definition, in mathcomp.algebra.interval]
+eqitvP [lemma, in mathcomp.algebra.interval]
eqlfunP [lemma, in mathcomp.algebra.vector]
eqlfun_inP [lemma, in mathcomp.algebra.vector]
EqMap [section, in mathcomp.ssreflect.seq]
@@ -732,12 +733,14 @@ EqMask [section, in mathcomp.ssreflect.seq]
EqMask.n0 [variable, in mathcomp.ssreflect.seq]
EqMask.T [variable, in mathcomp.ssreflect.seq]
+eqMixin [lemma, in mathcomp.ssreflect.finfun]
eqmodE [lemma, in mathcomp.ssreflect.generic_quotient]
eqmodP [lemma, in mathcomp.ssreflect.generic_quotient]
eqmx [definition, in mathcomp.algebra.mxalgebra]
eqmxMfree [lemma, in mathcomp.algebra.mxalgebra]
eqmxMfull [lemma, in mathcomp.algebra.mxalgebra]
eqmxMr [lemma, in mathcomp.algebra.mxalgebra]
+eqmxMunitP [lemma, in mathcomp.algebra.mxalgebra]
eqmxP [lemma, in mathcomp.algebra.mxalgebra]
eqmx_semisimple [lemma, in mathcomp.character.mxrepresentation]
eqmx_iso [lemma, in mathcomp.character.mxrepresentation]
@@ -830,7 +833,6 @@ eqseqE [lemma, in mathcomp.ssreflect.seq]
eqseqP [lemma, in mathcomp.ssreflect.seq]
eqseq_rot [lemma, in mathcomp.ssreflect.seq]
-eqseq_class [definition, in mathcomp.ssreflect.seq]
eqseq_rcons [lemma, in mathcomp.ssreflect.seq]
eqseq_cat [lemma, in mathcomp.ssreflect.seq]
eqseq_cons [lemma, in mathcomp.ssreflect.seq]
@@ -838,11 +840,16 @@ EqSeq.EqIn.a1 [variable, in mathcomp.ssreflect.seq]
EqSeq.EqIn.a2 [variable, in mathcomp.ssreflect.seq]
EqSeq.Filters [section, in mathcomp.ssreflect.seq]
+EqSeq.Filters.A [variable, in mathcomp.ssreflect.seq]
EqSeq.Filters.a [variable, in mathcomp.ssreflect.seq]
+EqSeq.Filters.aP [variable, in mathcomp.ssreflect.seq]
+EqSeq.Filters.s [variable, in mathcomp.ssreflect.seq]
EqSeq.inE [variable, in mathcomp.ssreflect.seq]
EqSeq.n0 [variable, in mathcomp.ssreflect.seq]
EqSeq.T [variable, in mathcomp.ssreflect.seq]
EqSeq.x0 [variable, in mathcomp.ssreflect.seq]
+'all_ _ [notation, in mathcomp.ssreflect.seq]
+'has_ _ [notation, in mathcomp.ssreflect.seq]
eqSS [lemma, in mathcomp.ssreflect.ssrnat]
eqsVneq [lemma, in mathcomp.ssreflect.finset]
EqTheory [section, in mathcomp.ssreflect.finfun]
@@ -870,13 +877,12 @@ Equality.Exports.EqMixin [abbreviation, in mathcomp.ssreflect.eqtype]
Equality.Exports.EqType [abbreviation, in mathcomp.ssreflect.eqtype]
Equality.Exports.eqType [abbreviation, in mathcomp.ssreflect.eqtype]
-[ eqType of _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
-[ eqType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
-[ eqMixin of _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
+[ eqType of _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
+[ eqType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
+[ eqMixin of _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
Equality.Mixin [constructor, in mathcomp.ssreflect.eqtype]
Equality.mixin_of [record, in mathcomp.ssreflect.eqtype]
Equality.op [projection, in mathcomp.ssreflect.eqtype]
-Equality.pack [definition, in mathcomp.ssreflect.eqtype]
Equality.Pack [constructor, in mathcomp.ssreflect.eqtype]
Equality.sort [projection, in mathcomp.ssreflect.eqtype]
Equality.type [record, in mathcomp.ssreflect.eqtype]
@@ -986,10 +992,14 @@ eq_quot_class_of [record, in mathcomp.ssreflect.generic_quotient]
eq_quot_mixin_of [definition, in mathcomp.ssreflect.generic_quotient]
eq_lock [lemma, in mathcomp.ssreflect.generic_quotient]
+eq_itv_boundP [lemma, in mathcomp.algebra.interval]
+eq_itv_bound [definition, in mathcomp.algebra.interval]
+eq_mktuple [lemma, in mathcomp.ssreflect.tuple]
eq_from_tnth [lemma, in mathcomp.ssreflect.tuple]
eq_block_mx [lemma, in mathcomp.algebra.matrix]
eq_col_mx [lemma, in mathcomp.algebra.matrix]
eq_row_mx [lemma, in mathcomp.algebra.matrix]
+eq_mx [lemma, in mathcomp.algebra.matrix]
eq_Aut [lemma, in mathcomp.fingroup.automorphism]
eq_subZnat_irr [lemma, in mathcomp.character.character]
eq_addZ_irr [lemma, in mathcomp.character.character]
@@ -999,11 +1009,15 @@ eq_irr_mem_classP [lemma, in mathcomp.character.character]
eq_sum_nth_irr [lemma, in mathcomp.character.character]
eq_Mod8_D8 [lemma, in mathcomp.solvable.extremal]
+eq_in_allpairs [lemma, in mathcomp.ssreflect.seq]
+eq_in_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
+eq_allpairs [lemma, in mathcomp.ssreflect.seq]
eq_from_flatten_shape [lemma, in mathcomp.ssreflect.seq]
eq_mkseq [lemma, in mathcomp.ssreflect.seq]
eq_pmap [lemma, in mathcomp.ssreflect.seq]
eq_in_map [lemma, in mathcomp.ssreflect.seq]
eq_map [lemma, in mathcomp.ssreflect.seq]
+eq_uniq [lemma, in mathcomp.ssreflect.seq]
eq_all_r [lemma, in mathcomp.ssreflect.seq]
eq_has_r [lemma, in mathcomp.ssreflect.seq]
eq_in_has [lemma, in mathcomp.ssreflect.seq]
@@ -1063,11 +1077,12 @@ eq_ex_minn [lemma, in mathcomp.ssreflect.ssrnat]
eq_leq [lemma, in mathcomp.ssreflect.ssrnat]
eq_map_poly [lemma, in mathcomp.algebra.poly]
+eq_poly [lemma, in mathcomp.algebra.poly]
eq_prim_root_expr [lemma, in mathcomp.algebra.poly]
+eq_big_perm [abbreviation, in mathcomp.ssreflect.bigop]
eq_bigmax [lemma, in mathcomp.ssreflect.bigop]
eq_bigmax_cond [lemma, in mathcomp.ssreflect.bigop]
eq_big_idem [lemma, in mathcomp.ssreflect.bigop]
-eq_big_perm [lemma, in mathcomp.ssreflect.bigop]
eq_big_idx [lemma, in mathcomp.ssreflect.bigop]
eq_big_idx_seq [lemma, in mathcomp.ssreflect.bigop]
eq_big_nat [lemma, in mathcomp.ssreflect.bigop]
@@ -1076,6 +1091,8 @@ eq_bigr [lemma, in mathcomp.ssreflect.bigop]
eq_bigl [lemma, in mathcomp.ssreflect.bigop]
eq_big_op [lemma, in mathcomp.ssreflect.bigop]
+eq_ffun [lemma, in mathcomp.ssreflect.finfun]
+eq_dffun [lemma, in mathcomp.ssreflect.finfun]
eq_Tagged [lemma, in mathcomp.ssreflect.eqtype]
eq_tag [lemma, in mathcomp.ssreflect.eqtype]
eq_comparable [definition, in mathcomp.ssreflect.eqtype]
@@ -1119,6 +1136,7 @@ eq_in_imset [lemma, in mathcomp.ssreflect.finset]
eq_imset [lemma, in mathcomp.ssreflect.finset]
eq_preimset [lemma, in mathcomp.ssreflect.finset]
+eq_finset [lemma, in mathcomp.ssreflect.finset]
Eq0NotPos [constructor, in mathcomp.ssreflect.ssrnat]
ErV [abbreviation, in mathcomp.character.mxabelem]
Euclid_dvdX [lemma, in mathcomp.ssreflect.prime]
@@ -1128,16 +1146,6 @@ eval [abbreviation, in mathcomp.character.mxrepresentation]
eval [abbreviation, in mathcomp.algebra.polyXY]
eval_mxmodule [lemma, in mathcomp.character.mxrepresentation]
-eval_bigmul [abbreviation, in mathcomp.field.closed_field]
-eval_poly1 [lemma, in mathcomp.field.closed_field]
-eval_poly_mulM [lemma, in mathcomp.field.closed_field]
-eval_natmulpT [lemma, in mathcomp.field.closed_field]
-eval_opppT [lemma, in mathcomp.field.closed_field]
-eval_mulpT [lemma, in mathcomp.field.closed_field]
-eval_sumpT [lemma, in mathcomp.field.closed_field]
-eval_amulXnT [lemma, in mathcomp.field.closed_field]
-eval_lift [lemma, in mathcomp.field.closed_field]
-eval_poly [definition, in mathcomp.field.closed_field]
even_prime [lemma, in mathcomp.ssreflect.prime]
ev_ax [abbreviation, in mathcomp.ssreflect.eqtype]
exchange_big_nat [lemma, in mathcomp.ssreflect.bigop]
@@ -1150,6 +1158,7 @@ exists_acomps [lemma, in mathcomp.solvable.jordanholder]
exists_comps [lemma, in mathcomp.solvable.jordanholder]
exists_eq_inP [lemma, in mathcomp.ssreflect.fintype]
+exists_inPP [lemma, in mathcomp.ssreflect.fintype]
exists_inP [lemma, in mathcomp.ssreflect.fintype]
exists_eqP [lemma, in mathcomp.ssreflect.fintype]
ExMaxn [section, in mathcomp.ssreflect.ssrnat]
@@ -1527,15 +1536,23 @@ Extremal.gtype_key [lemma, in mathcomp.solvable.extremal]
extremal2 [definition, in mathcomp.solvable.extremal]
extremal2_structure [lemma, in mathcomp.solvable.extremal]
+Extrema.ArgMinMax [section, in mathcomp.ssreflect.fintype]
+Extrema.ArgMinMax.F [variable, in mathcomp.ssreflect.fintype]
+Extrema.ArgMinMax.I [variable, in mathcomp.ssreflect.fintype]
+Extrema.ArgMinMax.i0 [variable, in mathcomp.ssreflect.fintype]
+Extrema.ArgMinMax.P [variable, in mathcomp.ssreflect.fintype]
+Extrema.ArgMinMax.Pi0 [variable, in mathcomp.ssreflect.fintype]
Extrema.arg_pred [variable, in mathcomp.ssreflect.fintype]
-Extrema.exFP [variable, in mathcomp.ssreflect.fintype]
-Extrema.F [variable, in mathcomp.ssreflect.fintype]
-Extrema.FP [variable, in mathcomp.ssreflect.fintype]
-Extrema.FP_F [variable, in mathcomp.ssreflect.fintype]
-Extrema.I [variable, in mathcomp.ssreflect.fintype]
-Extrema.i0 [variable, in mathcomp.ssreflect.fintype]
-Extrema.P [variable, in mathcomp.ssreflect.fintype]
-Extrema.Pi0 [variable, in mathcomp.ssreflect.fintype]
+Extrema.Extremum [section, in mathcomp.ssreflect.fintype]
+Extrema.Extremum.ord_total [variable, in mathcomp.ssreflect.fintype]
+Extrema.Extremum.ord_trans [variable, in mathcomp.ssreflect.fintype]
+Extrema.Extremum.ord_refl [variable, in mathcomp.ssreflect.fintype]
+Extrema.Extremum.Pi0 [variable, in mathcomp.ssreflect.fintype]
+[ arg[ _ ]_( _ < _ ) _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
+[ arg[ _ ]_( _ < _ in _ ) _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
+[ arg[ _ ]_( _ < _ | _ ) _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
+extremum [definition, in mathcomp.ssreflect.fintype]
+extremumP [lemma, in mathcomp.ssreflect.fintype]
ExtremumSpec [constructor, in mathcomp.ssreflect.fintype]
extremum_spec [inductive, in mathcomp.ssreflect.fintype]
ExtSdprodm [section, in mathcomp.fingroup.gproduct]
@@ -1563,11 +1580,6 @@ ex_minnP [lemma, in mathcomp.ssreflect.ssrnat]
ex_minn_spec [inductive, in mathcomp.ssreflect.ssrnat]
ex_minn [definition, in mathcomp.ssreflect.ssrnat]
-ex_elim_qf [lemma, in mathcomp.field.closed_field]
-ex_elim [definition, in mathcomp.field.closed_field]
-ex_elim_seq_qf [lemma, in mathcomp.field.closed_field]
-ex_elim_seqP [lemma, in mathcomp.field.closed_field]
-ex_elim_seq [definition, in mathcomp.field.closed_field]
ex_mingroup [lemma, in mathcomp.fingroup.fingroup]
ex_maxgroup [lemma, in mathcomp.fingroup.fingroup]
ex_maxset [lemma, in mathcomp.ssreflect.finset]
@@ -1610,7 +1622,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1642,14 +1654,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1674,7 +1686,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1706,7 +1718,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1738,7 +1750,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1770,7 +1782,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1802,7 +1814,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1834,7 +1846,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1866,14 +1878,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1898,7 +1910,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1930,7 +1942,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1962,7 +1974,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1994,14 +2006,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -2026,7 +2038,7 @@ Z _ other -(185 entries) +(189 entries) -- cgit v1.2.3