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_L.html | 163 ++++++++++++++++++++++++++++----------- 1 file changed, 120 insertions(+), 43 deletions(-) (limited to 'docs/htmldoc/index_global_L.html') diff --git a/docs/htmldoc/index_global_L.html b/docs/htmldoc/index_global_L.html index bf40c44..0864480 100644 --- a/docs/htmldoc/index_global_L.html +++ b/docs/htmldoc/index_global_L.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)

L

@@ -482,6 +482,7 @@ LastRcons [constructor, in mathcomp.ssreflect.seq]
last_traject [lemma, in mathcomp.ssreflect.path]
last_map [lemma, in mathcomp.ssreflect.seq]
+last_eq [lemma, in mathcomp.ssreflect.seq]
last_nth [lemma, in mathcomp.ssreflect.seq]
last_ind [lemma, in mathcomp.ssreflect.seq]
last_spec [inductive, in mathcomp.ssreflect.seq]
@@ -567,6 +568,7 @@ lead_coefX [lemma, in mathcomp.algebra.poly]
lead_coef_proper_mul [lemma, in mathcomp.algebra.poly]
lead_coef1 [lemma, in mathcomp.algebra.poly]
+lead_coefDr [lemma, in mathcomp.algebra.poly]
lead_coefDl [lemma, in mathcomp.algebra.poly]
lead_coef_opp [lemma, in mathcomp.algebra.poly]
lead_coef_eq0 [lemma, in mathcomp.algebra.poly]
@@ -575,9 +577,6 @@ lead_coefC [lemma, in mathcomp.algebra.poly]
lead_coefE [lemma, in mathcomp.algebra.poly]
lead_coef [definition, in mathcomp.algebra.poly]
-lead_coefT_qf [lemma, in mathcomp.field.closed_field]
-lead_coefTP [lemma, in mathcomp.field.closed_field]
-lead_coefT [definition, in mathcomp.field.closed_field]
leC_nat [definition, in mathcomp.field.algC]
left_arc [lemma, in mathcomp.ssreflect.path]
left_trans [lemma, in mathcomp.ssreflect.generic_quotient]
@@ -602,8 +601,13 @@ leqP [lemma, in mathcomp.ssreflect.ssrnat]
leqSpred [lemma, in mathcomp.ssreflect.ssrnat]
leqW [lemma, in mathcomp.ssreflect.ssrnat]
+leqW_nmono_in [lemma, in mathcomp.ssreflect.ssrnat]
+leqW_mono_in [lemma, in mathcomp.ssreflect.ssrnat]
+leqW_nmono [lemma, in mathcomp.ssreflect.ssrnat]
+leqW_mono [lemma, in mathcomp.ssreflect.ssrnat]
leq_quotient [lemma, in mathcomp.fingroup.quotient]
leq_bin2l [lemma, in mathcomp.ssreflect.binomial]
+leq_index [lemma, in mathcomp.ssreflect.path]
leq_divLR [lemma, in mathcomp.ssreflect.div]
leq_divDl [lemma, in mathcomp.ssreflect.div]
leq_div2l [lemma, in mathcomp.ssreflect.div]
@@ -612,12 +616,16 @@ leq_div [lemma, in mathcomp.ssreflect.div]
leq_mod [lemma, in mathcomp.ssreflect.div]
leq_trunc_div [lemma, in mathcomp.ssreflect.div]
-leq_size_perm [lemma, in mathcomp.ssreflect.seq]
+leq_size_perm [abbreviation, in mathcomp.ssreflect.seq]
leq_size_uniq [lemma, in mathcomp.ssreflect.seq]
leq_ord [lemma, in mathcomp.ssreflect.fintype]
leq_bump2 [lemma, in mathcomp.ssreflect.fintype]
leq_bump [lemma, in mathcomp.ssreflect.fintype]
leq_image_card [lemma, in mathcomp.ssreflect.fintype]
+leq_nmono_in [lemma, in mathcomp.ssreflect.ssrnat]
+leq_mono_in [lemma, in mathcomp.ssreflect.ssrnat]
+leq_nmono [lemma, in mathcomp.ssreflect.ssrnat]
+leq_mono [lemma, in mathcomp.ssreflect.ssrnat]
leq_sqr [lemma, in mathcomp.ssreflect.ssrnat]
leq_Sdouble [lemma, in mathcomp.ssreflect.ssrnat]
leq_double [lemma, in mathcomp.ssreflect.ssrnat]
@@ -651,6 +659,7 @@ leq_ltn_trans [lemma, in mathcomp.ssreflect.ssrnat]
leq_trans [lemma, in mathcomp.ssreflect.ssrnat]
leq_eqVlt [lemma, in mathcomp.ssreflect.ssrnat]
+leq_gtF [lemma, in mathcomp.ssreflect.ssrnat]
leq_pred [lemma, in mathcomp.ssreflect.ssrnat]
leq_sizeP [lemma, in mathcomp.algebra.poly]
leq_bigmax [lemma, in mathcomp.ssreflect.bigop]
@@ -665,14 +674,70 @@ lerq0 [lemma, in mathcomp.algebra.rat]
lersif [definition, in mathcomp.algebra.interval]
lersifF [lemma, in mathcomp.algebra.interval]
+LersifField [section, in mathcomp.algebra.interval]
+LersifField.b [variable, in mathcomp.algebra.interval]
+LersifField.F [variable, in mathcomp.algebra.interval]
+LersifField.x [variable, in mathcomp.algebra.interval]
+LersifField.y [variable, in mathcomp.algebra.interval]
+LersifField.z [variable, in mathcomp.algebra.interval]
lersifN [lemma, in mathcomp.algebra.interval]
lersifNF [lemma, in mathcomp.algebra.interval]
+LersifOrdered [section, in mathcomp.algebra.interval]
+LersifOrdered.b [variable, in mathcomp.algebra.interval]
+LersifOrdered.e [variable, in mathcomp.algebra.interval]
+LersifOrdered.R [variable, in mathcomp.algebra.interval]
+LersifOrdered.x [variable, in mathcomp.algebra.interval]
+LersifOrdered.y [variable, in mathcomp.algebra.interval]
+LersifOrdered.z [variable, in mathcomp.algebra.interval]
+LersifPo [section, in mathcomp.algebra.interval]
+LersifPo.R [variable, in mathcomp.algebra.interval]
+_ <= _ ?< if _ (ring_scope) [notation, in mathcomp.algebra.interval]
lersifS [lemma, in mathcomp.algebra.interval]
lersifT [lemma, in mathcomp.algebra.interval]
lersifW [lemma, in mathcomp.algebra.interval]
lersifxx [lemma, in mathcomp.algebra.interval]
lersif_in_itv [lemma, in mathcomp.algebra.interval]
+lersif_ndivr_mull [lemma, in mathcomp.algebra.interval]
+lersif_ndivl_mull [lemma, in mathcomp.algebra.interval]
+lersif_ndivr_mulr [lemma, in mathcomp.algebra.interval]
+lersif_ndivl_mulr [lemma, in mathcomp.algebra.interval]
+lersif_pdivr_mull [lemma, in mathcomp.algebra.interval]
+lersif_pdivl_mull [lemma, in mathcomp.algebra.interval]
+lersif_pdivr_mulr [lemma, in mathcomp.algebra.interval]
+lersif_pdivl_mulr [lemma, in mathcomp.algebra.interval]
+lersif_maxl [lemma, in mathcomp.algebra.interval]
+lersif_maxr [lemma, in mathcomp.algebra.interval]
+lersif_minl [lemma, in mathcomp.algebra.interval]
+lersif_minr [lemma, in mathcomp.algebra.interval]
+lersif_distl [lemma, in mathcomp.algebra.interval]
+lersif_normr [lemma, in mathcomp.algebra.interval]
+lersif_norml [lemma, in mathcomp.algebra.interval]
+lersif_nnormr [lemma, in mathcomp.algebra.interval]
+lersif_nmul2r [lemma, in mathcomp.algebra.interval]
+lersif_nmul2l [lemma, in mathcomp.algebra.interval]
+lersif_pmul2r [lemma, in mathcomp.algebra.interval]
+lersif_pmul2l [lemma, in mathcomp.algebra.interval]
+lersif_imply [lemma, in mathcomp.algebra.interval]
+lersif_orb [lemma, in mathcomp.algebra.interval]
+lersif_andb [lemma, in mathcomp.algebra.interval]
+lersif_sub_addl [definition, in mathcomp.algebra.interval]
+lersif_subr_addl [lemma, in mathcomp.algebra.interval]
+lersif_subl_addl [lemma, in mathcomp.algebra.interval]
+lersif_sub_addr [definition, in mathcomp.algebra.interval]
+lersif_subr_addr [lemma, in mathcomp.algebra.interval]
+lersif_subl_addr [lemma, in mathcomp.algebra.interval]
+lersif_add2 [definition, in mathcomp.algebra.interval]
+lersif_add2r [lemma, in mathcomp.algebra.interval]
+lersif_add2l [lemma, in mathcomp.algebra.interval]
+lersif_oppE [definition, in mathcomp.algebra.interval]
+lersif_opp2 [lemma, in mathcomp.algebra.interval]
+lersif_oppr0 [lemma, in mathcomp.algebra.interval]
+lersif_0oppr [lemma, in mathcomp.algebra.interval]
+lersif_oppr [lemma, in mathcomp.algebra.interval]
+lersif_oppl [lemma, in mathcomp.algebra.interval]
+lersif_anti [lemma, in mathcomp.algebra.interval]
lersif_trans [lemma, in mathcomp.algebra.interval]
+lersif01 [lemma, in mathcomp.algebra.interval]
lerz0 [lemma, in mathcomp.algebra.ssrint]
lerz1 [lemma, in mathcomp.algebra.ssrint]
ler_rat [lemma, in mathcomp.algebra.rat]
@@ -717,10 +782,16 @@ le_rat0D [lemma, in mathcomp.algebra.rat]
le_rat0 [lemma, in mathcomp.algebra.rat]
le_rat [definition, in mathcomp.algebra.rat]
+le_boundr_total [lemma, in mathcomp.algebra.interval]
+le_boundl_total [lemma, in mathcomp.algebra.interval]
+le_boundr_anti [lemma, in mathcomp.algebra.interval]
+le_boundl_anti [lemma, in mathcomp.algebra.interval]
le_boundr_bb [lemma, in mathcomp.algebra.interval]
le_boundl_bb [lemma, in mathcomp.algebra.interval]
-le_boundl_refl [lemma, in mathcomp.algebra.interval]
+le_boundr_trans [lemma, in mathcomp.algebra.interval]
+le_boundl_trans [lemma, in mathcomp.algebra.interval]
le_boundr_refl [lemma, in mathcomp.algebra.interval]
+le_boundl_refl [lemma, in mathcomp.algebra.interval]
le_boundr [definition, in mathcomp.algebra.interval]
le_boundl [definition, in mathcomp.algebra.interval]
le_irrelevance [lemma, in mathcomp.ssreflect.ssrnat]
@@ -738,7 +809,7 @@ LfunVectType.aT [variable, in mathcomp.algebra.vector]
LfunVectType.R [variable, in mathcomp.algebra.vector]
LfunVectType.rT [variable, in mathcomp.algebra.vector]
-_ *:l _ [notation, in mathcomp.algebra.vector]
+_ *:l _ [notation, in mathcomp.algebra.vector]
LfunVspaceDefs [section, in mathcomp.algebra.vector]
LfunVspaceDefs.K [variable, in mathcomp.algebra.vector]
LfunZmodType [section, in mathcomp.algebra.vector]
@@ -766,6 +837,7 @@ lfun_addA [lemma, in mathcomp.algebra.vector]
lfun_is_linear [lemma, in mathcomp.algebra.vector]
lfun_choiceMixin [definition, in mathcomp.algebra.vector]
+lfun_eqMixin [definition, in mathcomp.algebra.vector]
lfun_preim [definition, in mathcomp.algebra.vector]
lfun_img [definition, in mathcomp.algebra.vector]
lfun_img_def [definition, in mathcomp.algebra.vector]
@@ -774,7 +846,6 @@ lfun1_neq0 [lemma, in mathcomp.algebra.vector]
lfun1_poly [lemma, in mathcomp.field.falgebra]
lift [definition, in mathcomp.ssreflect.fintype]
-lift [definition, in mathcomp.field.closed_field]
liftK [lemma, in mathcomp.ssreflect.fintype]
LiftPerm [section, in mathcomp.fingroup.perm]
LiftPerm.n [variable, in mathcomp.fingroup.perm]
@@ -972,9 +1043,14 @@ ltnS [lemma, in mathcomp.ssreflect.ssrnat]
ltnSn [lemma, in mathcomp.ssreflect.ssrnat]
ltnW [lemma, in mathcomp.ssreflect.ssrnat]
+ltnW_nhomo_in [lemma, in mathcomp.ssreflect.ssrnat]
+ltnW_homo_in [lemma, in mathcomp.ssreflect.ssrnat]
+ltnW_nhomo [lemma, in mathcomp.ssreflect.ssrnat]
+ltnW_homo [lemma, in mathcomp.ssreflect.ssrnat]
ltNz_nat [lemma, in mathcomp.algebra.ssrint]
ltn_log_quotient [lemma, in mathcomp.solvable.pgroup]
ltn_quotient [lemma, in mathcomp.fingroup.quotient]
+ltn_index [lemma, in mathcomp.ssreflect.path]
ltn_sorted_uniq_leq [lemma, in mathcomp.ssreflect.path]
ltn_odd_Frobenius_ker [lemma, in mathcomp.solvable.frobenius]
ltn_logl [lemma, in mathcomp.ssreflect.prime]
@@ -1014,6 +1090,7 @@ ltn_xor_geq [inductive, in mathcomp.ssreflect.ssrnat]
ltn_trans [lemma, in mathcomp.ssreflect.ssrnat]
ltn_neqAle [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_geF [lemma, in mathcomp.ssreflect.ssrnat]
ltn_eqF [lemma, in mathcomp.ssreflect.ssrnat]
ltn_predK [lemma, in mathcomp.ssreflect.ssrnat]
ltn_morphim [lemma, in mathcomp.fingroup.morphism]
@@ -1021,6 +1098,7 @@ ltn0Sn [lemma, in mathcomp.ssreflect.ssrnat]
ltP [lemma, in mathcomp.ssreflect.ssrnat]
ltrq0 [lemma, in mathcomp.algebra.rat]
+ltrW_lersif [lemma, in mathcomp.algebra.interval]
ltrz0 [lemma, in mathcomp.algebra.ssrint]
ltrz1 [lemma, in mathcomp.algebra.ssrint]
ltr_rat [lemma, in mathcomp.algebra.rat]
@@ -1054,7 +1132,6 @@ lt_rat [definition, in mathcomp.algebra.rat]
lt_irrelevance [lemma, in mathcomp.ssreflect.ssrnat]
lt_size_deriv [lemma, in mathcomp.algebra.poly]
-lt_sizeT [definition, in mathcomp.field.closed_field]
lt_eqmx [lemma, in mathcomp.algebra.mxalgebra]
lt0b [lemma, in mathcomp.ssreflect.ssrnat]
lt0mx [lemma, in mathcomp.algebra.mxalgebra]
@@ -1096,7 +1173,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1128,14 +1205,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1160,7 +1237,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1192,7 +1269,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1224,7 +1301,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1256,7 +1333,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1288,7 +1365,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1320,7 +1397,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1352,14 +1429,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1384,7 +1461,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1416,7 +1493,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1448,7 +1525,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1480,14 +1557,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1512,7 +1589,7 @@ Z _ other -(185 entries) +(189 entries) -- cgit v1.2.3