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_lemma_N.html | 160 +++++++++++++++++++++++++---------------
1 file changed, 100 insertions(+), 60 deletions(-)
(limited to 'docs/htmldoc/index_lemma_N.html')
diff --git a/docs/htmldoc/index_lemma_N.html b/docs/htmldoc/index_lemma_N.html
index 7d12494..e6b2218 100644
--- a/docs/htmldoc/index_lemma_N.html
+++ b/docs/htmldoc/index_lemma_N.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) |
N (lemma)
@@ -491,8 +491,9 @@
nat_of_exp_bin [in mathcomp.ssreflect.ssrnat]
nat_of_mul_bin [in mathcomp.ssreflect.ssrnat]
nat_of_add_bin [in mathcomp.ssreflect.ssrnat]
-nat_of_addn_gt0 [in mathcomp.ssreflect.ssrnat]
-nat_of_succ_gt0 [in mathcomp.ssreflect.ssrnat]
+nat_of_mul_pos [in mathcomp.ssreflect.ssrnat]
+nat_of_add_pos [in mathcomp.ssreflect.ssrnat]
+nat_of_succ_pos [in mathcomp.ssreflect.ssrnat]
nat_of_binK [in mathcomp.ssreflect.ssrnat]
nat_AGM2 [in mathcomp.ssreflect.ssrnat]
nat_Cauchy [in mathcomp.ssreflect.ssrnat]
@@ -554,6 +555,8 @@
next_prev [in mathcomp.ssreflect.path]
next_cycle [in mathcomp.ssreflect.path]
next_nth [in mathcomp.ssreflect.path]
+nhomo_inj_lt_in [in mathcomp.ssreflect.ssrnat]
+nhomo_inj_lt [in mathcomp.ssreflect.ssrnat]
nilP [in mathcomp.ssreflect.seq]
nilpotentS [in mathcomp.solvable.nilpotent]
nilpotent_Fitting [in mathcomp.solvable.maximal]
@@ -704,6 +707,7 @@
not_asubv0 [in mathcomp.field.falgebra]
nseqP [in mathcomp.ssreflect.seq]
nseq_tupleP [in mathcomp.ssreflect.tuple]
+nthK [in mathcomp.ssreflect.seq]
nthP [in mathcomp.ssreflect.seq]
nth_traject [in mathcomp.ssreflect.path]
nth_mktuple [in mathcomp.ssreflect.tuple]
@@ -820,6 +824,8 @@
Num.Theory.addr_ss_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.addr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.archi_boundP [in mathcomp.algebra.ssrnum]
+Num.Theory.arg_maxrP [in mathcomp.algebra.ssrnum]
+Num.Theory.arg_minrP [in mathcomp.algebra.ssrnum]
Num.Theory.Cauchy_root_bound [in mathcomp.algebra.ssrnum]
Num.Theory.char_num [in mathcomp.algebra.ssrnum]
Num.Theory.conjCi [in mathcomp.algebra.ssrnum]
@@ -839,6 +845,12 @@
Num.Theory.Creal_Im [in mathcomp.algebra.ssrnum]
Num.Theory.Creal_Re [in mathcomp.algebra.ssrnum]
Num.Theory.Crect [in mathcomp.algebra.ssrnum]
+Num.Theory.decnr_inj_inj_in [in mathcomp.algebra.ssrnum]
+Num.Theory.decnr_inj_inj [in mathcomp.algebra.ssrnum]
+Num.Theory.decrn_inj_in [in mathcomp.algebra.ssrnum]
+Num.Theory.decrn_inj [in mathcomp.algebra.ssrnum]
+Num.Theory.decr_inj_in [in mathcomp.algebra.ssrnum]
+Num.Theory.decr_inj [in mathcomp.algebra.ssrnum]
Num.Theory.distrC [in mathcomp.algebra.ssrnum]
Num.Theory.divr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.divr_ge0 [in mathcomp.algebra.ssrnum]
@@ -911,12 +923,6 @@
Num.Theory.gtr0_sg [in mathcomp.algebra.ssrnum]
Num.Theory.gtr0_real [in mathcomp.algebra.ssrnum]
Num.Theory.gt0_cp [in mathcomp.algebra.ssrnum]
-Num.Theory.homo_mono_in [in mathcomp.algebra.ssrnum]
-Num.Theory.homo_mono [in mathcomp.algebra.ssrnum]
-Num.Theory.homo_leq_mono [in mathcomp.algebra.ssrnum]
-Num.Theory.homo_inj_ltn_lt [in mathcomp.algebra.ssrnum]
-Num.Theory.homo_inj_in_lt [in mathcomp.algebra.ssrnum]
-Num.Theory.homo_inj_lt [in mathcomp.algebra.ssrnum]
Num.Theory.ieexprIn [in mathcomp.algebra.ssrnum]
Num.Theory.ieexprn_weq1 [in mathcomp.algebra.ssrnum]
Num.Theory.imaginaryCE [in mathcomp.algebra.ssrnum]
@@ -927,6 +933,24 @@
Num.Theory.Im_conj [in mathcomp.algebra.ssrnum]
Num.Theory.Im_i [in mathcomp.algebra.ssrnum]
Num.Theory.Im_is_additive [in mathcomp.algebra.ssrnum]
+Num.Theory.incnr_inj_in [in mathcomp.algebra.ssrnum]
+Num.Theory.incnr_inj [in mathcomp.algebra.ssrnum]
+Num.Theory.incrn_inj_in [in mathcomp.algebra.ssrnum]
+Num.Theory.incrn_inj [in mathcomp.algebra.ssrnum]
+Num.Theory.incr_inj_in [in mathcomp.algebra.ssrnum]
+Num.Theory.incr_inj [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_nhomo_ltrn_in [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_homo_ltrn_in [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_nhomo_ltrn [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_homo_ltrn [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_nhomo_ltnr_in [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_homo_ltnr_in [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_nhomo_ltnr [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_homo_ltnr [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_nhomo_ltr_in [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_homo_ltr_in [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_nhomo_ltr [in mathcomp.algebra.ssrnum]
+Num.Theory.inj_homo_ltr [in mathcomp.algebra.ssrnum]
Num.Theory.invCi [in mathcomp.algebra.ssrnum]
Num.Theory.invC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.invC_norm [in mathcomp.algebra.ssrnum]
@@ -945,10 +969,14 @@
Num.Theory.invr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.lef_ninv [in mathcomp.algebra.ssrnum]
Num.Theory.lef_pinv [in mathcomp.algebra.ssrnum]
-Num.Theory.leq_lerW_nmono [in mathcomp.algebra.ssrnum]
-Num.Theory.leq_lerW_mono [in mathcomp.algebra.ssrnum]
-Num.Theory.leq_nmono_inj [in mathcomp.algebra.ssrnum]
-Num.Theory.leq_mono_inj [in mathcomp.algebra.ssrnum]
+Num.Theory.lenrW_nmono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.lenrW_mono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.lenrW_nmono [in mathcomp.algebra.ssrnum]
+Num.Theory.lenrW_mono [in mathcomp.algebra.ssrnum]
+Num.Theory.lenr_nmono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.lenr_mono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.lenr_nmono [in mathcomp.algebra.ssrnum]
+Num.Theory.lenr_mono [in mathcomp.algebra.ssrnum]
Num.Theory.lerifP [in mathcomp.algebra.ssrnum]
Num.Theory.lerif_rootC_AGM [in mathcomp.algebra.ssrnum]
Num.Theory.lerif_Re_Creal [in mathcomp.algebra.ssrnum]
@@ -973,6 +1001,14 @@
Num.Theory.lerif_trans [in mathcomp.algebra.ssrnum]
Num.Theory.lerif_refl [in mathcomp.algebra.ssrnum]
Num.Theory.lerNgt [in mathcomp.algebra.ssrnum]
+Num.Theory.lernW_nmono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.lernW_mono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.lernW_nmono [in mathcomp.algebra.ssrnum]
+Num.Theory.lernW_mono [in mathcomp.algebra.ssrnum]
+Num.Theory.lern_nmono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.lern_mono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.lern_nmono [in mathcomp.algebra.ssrnum]
+Num.Theory.lern_mono [in mathcomp.algebra.ssrnum]
Num.Theory.lern0 [in mathcomp.algebra.ssrnum]
Num.Theory.lern1 [in mathcomp.algebra.ssrnum]
Num.Theory.lerN10 [in mathcomp.algebra.ssrnum]
@@ -997,6 +1033,10 @@
Num.Theory.ler_normlP [in mathcomp.algebra.ssrnum]
Num.Theory.ler_norml [in mathcomp.algebra.ssrnum]
Num.Theory.ler_norm [in mathcomp.algebra.ssrnum]
+Num.Theory.ler_nmono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.ler_mono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.ler_nmono [in mathcomp.algebra.ssrnum]
+Num.Theory.ler_mono [in mathcomp.algebra.ssrnum]
Num.Theory.ler_total [in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivr_mull [in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivl_mull [in mathcomp.algebra.ssrnum]
@@ -1100,11 +1140,17 @@
Num.Theory.le0_cp [in mathcomp.algebra.ssrnum]
Num.Theory.ltf_ninv [in mathcomp.algebra.ssrnum]
Num.Theory.ltf_pinv [in mathcomp.algebra.ssrnum]
-Num.Theory.ltn_ltrW_nhomo [in mathcomp.algebra.ssrnum]
-Num.Theory.ltn_ltrW_homo [in mathcomp.algebra.ssrnum]
+Num.Theory.ltnrW_nhomo_in [in mathcomp.algebra.ssrnum]
+Num.Theory.ltnrW_homo_in [in mathcomp.algebra.ssrnum]
+Num.Theory.ltnrW_nhomo [in mathcomp.algebra.ssrnum]
+Num.Theory.ltnrW_homo [in mathcomp.algebra.ssrnum]
Num.Theory.ltrgtP [in mathcomp.algebra.ssrnum]
Num.Theory.ltrgt0P [in mathcomp.algebra.ssrnum]
Num.Theory.ltrNge [in mathcomp.algebra.ssrnum]
+Num.Theory.ltrnW_nhomo_in [in mathcomp.algebra.ssrnum]
+Num.Theory.ltrnW_homo_in [in mathcomp.algebra.ssrnum]
+Num.Theory.ltrnW_nhomo [in mathcomp.algebra.ssrnum]
+Num.Theory.ltrnW_homo [in mathcomp.algebra.ssrnum]
Num.Theory.ltrn0 [in mathcomp.algebra.ssrnum]
Num.Theory.ltrn1 [in mathcomp.algebra.ssrnum]
Num.Theory.ltrN10 [in mathcomp.algebra.ssrnum]
@@ -1188,8 +1234,8 @@
Num.Theory.ltr_le_sub [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_add [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_le_add [in mathcomp.algebra.ssrnum]
-Num.Theory.ltr_add2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_add2r [in mathcomp.algebra.ssrnum]
+Num.Theory.ltr_add2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_oppl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_oppr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_opp2 [in mathcomp.algebra.ssrnum]
@@ -1254,8 +1300,6 @@
Num.Theory.monic_Cauchy_bound [in mathcomp.algebra.ssrnum]
Num.Theory.mono_lerif [in mathcomp.algebra.ssrnum]
Num.Theory.mono_in_lerif [in mathcomp.algebra.ssrnum]
-Num.Theory.mono_inj_in [in mathcomp.algebra.ssrnum]
-Num.Theory.mono_inj [in mathcomp.algebra.ssrnum]
Num.Theory.mulC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.mulrIn [in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wlt0 [in mathcomp.algebra.ssrnum]
@@ -1294,16 +1338,8 @@
Num.Theory.neqr0_sign [in mathcomp.algebra.ssrnum]
Num.Theory.neq0Ci [in mathcomp.algebra.ssrnum]
Num.Theory.neq0_mulr_lt0 [in mathcomp.algebra.ssrnum]
-Num.Theory.nhomo_mono_in [in mathcomp.algebra.ssrnum]
-Num.Theory.nhomo_mono [in mathcomp.algebra.ssrnum]
-Num.Theory.nhomo_leq_mono [in mathcomp.algebra.ssrnum]
-Num.Theory.nhomo_inj_ltn_lt [in mathcomp.algebra.ssrnum]
-Num.Theory.nhomo_inj_in_lt [in mathcomp.algebra.ssrnum]
-Num.Theory.nhomo_inj_lt [in mathcomp.algebra.ssrnum]
Num.Theory.nmono_lerif [in mathcomp.algebra.ssrnum]
Num.Theory.nmono_in_lerif [in mathcomp.algebra.ssrnum]
-Num.Theory.nmono_inj_in [in mathcomp.algebra.ssrnum]
-Num.Theory.nmono_inj [in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rle0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rge0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rgt0 [in mathcomp.algebra.ssrnum]
@@ -1414,6 +1450,10 @@
Num.Theory.realN [in mathcomp.algebra.ssrnum]
Num.Theory.realn [in mathcomp.algebra.ssrnum]
Num.Theory.realNEsign [in mathcomp.algebra.ssrnum]
+Num.Theory.realn_nmono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.realn_mono_in [in mathcomp.algebra.ssrnum]
+Num.Theory.realn_nmono [in mathcomp.algebra.ssrnum]
+Num.Theory.realn_mono [in mathcomp.algebra.ssrnum]
Num.Theory.realrM [in mathcomp.algebra.ssrnum]
Num.Theory.realrMn [in mathcomp.algebra.ssrnum]
Num.Theory.realV [in mathcomp.algebra.ssrnum]
@@ -1599,7 +1639,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -1631,14 +1671,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1663,7 +1703,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -1695,7 +1735,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -1727,7 +1767,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -1759,7 +1799,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -1791,7 +1831,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -1823,7 +1863,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -1855,14 +1895,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1887,7 +1927,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -1919,7 +1959,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -1951,7 +1991,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -1983,14 +2023,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -2015,7 +2055,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
--
cgit v1.2.3