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_*.html | 36 ++++----- docs/htmldoc/index_lemma_A.html | 89 ++++++++++++---------- docs/htmldoc/index_lemma_B.html | 79 +++++++++++--------- docs/htmldoc/index_lemma_C.html | 140 +++++++++++++++++++++++++---------- docs/htmldoc/index_lemma_D.html | 73 +++++++++--------- docs/htmldoc/index_lemma_E.html | 100 +++++++++++++------------ docs/htmldoc/index_lemma_F.html | 82 ++++++++++---------- docs/htmldoc/index_lemma_G.html | 77 ++++++++++--------- docs/htmldoc/index_lemma_H.html | 82 ++++++++++---------- docs/htmldoc/index_lemma_I.html | 81 ++++++++++---------- docs/htmldoc/index_lemma_J.html | 36 ++++----- docs/htmldoc/index_lemma_K.html | 70 +++++++++--------- docs/htmldoc/index_lemma_L.html | 136 ++++++++++++++++++++++++---------- docs/htmldoc/index_lemma_M.html | 79 +++++++++++--------- docs/htmldoc/index_lemma_N.html | 160 +++++++++++++++++++++++++--------------- docs/htmldoc/index_lemma_O.html | 70 +++++++++--------- docs/htmldoc/index_lemma_P.html | 123 +++++++++++++++++------------- docs/htmldoc/index_lemma_Q.html | 70 +++++++++--------- docs/htmldoc/index_lemma_R.html | 97 ++++++++++-------------- docs/htmldoc/index_lemma_S.html | 94 +++++++++++++---------- docs/htmldoc/index_lemma_T.html | 83 ++++++++++++--------- docs/htmldoc/index_lemma_U.html | 73 +++++++++--------- docs/htmldoc/index_lemma_V.html | 70 +++++++++--------- docs/htmldoc/index_lemma_W.html | 37 +++++----- docs/htmldoc/index_lemma_X.html | 36 ++++----- docs/htmldoc/index_lemma_Y.html | 36 ++++----- docs/htmldoc/index_lemma_Z.html | 70 +++++++++--------- docs/htmldoc/index_lemma__.html | 36 ++++----- 28 files changed, 1229 insertions(+), 986 deletions(-) (limited to 'docs/htmldoc/index_lemma_*.html') diff --git a/docs/htmldoc/index_lemma_*.html b/docs/htmldoc/index_lemma_*.html index c9bd28e..ecb788b 100644 --- a/docs/htmldoc/index_lemma_*.html +++ b/docs/htmldoc/index_lemma_*.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)
diff --git a/docs/htmldoc/index_lemma_A.html b/docs/htmldoc/index_lemma_A.html index fa3086e..ba5d7b7 100644 --- a/docs/htmldoc/index_lemma_A.html +++ b/docs/htmldoc/index_lemma_A.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)

A (lemma)

@@ -509,6 +509,7 @@ abelian_type_abelem [in mathcomp.solvable.abelian]
abelian_type_homocyclic [in mathcomp.solvable.abelian]
abelian_rank1_cyclic [in mathcomp.solvable.abelian]
+abelian_type_pgroup [in mathcomp.solvable.abelian]
abelian_structure [in mathcomp.solvable.abelian]
abelian_type_sorted [in mathcomp.solvable.abelian]
abelian_type_gt1 [in mathcomp.solvable.abelian]
@@ -523,9 +524,6 @@ abelian_nil [in mathcomp.solvable.nilpotent]
abelian_gen [in mathcomp.fingroup.fingroup]
abelian1 [in mathcomp.fingroup.fingroup]
-abstrXP [in mathcomp.field.closed_field]
-abstrX_mulM [in mathcomp.field.closed_field]
-abstrX1 [in mathcomp.field.closed_field]
abszE [in mathcomp.algebra.ssrint]
abszEsg [in mathcomp.algebra.ssrint]
abszEsign [in mathcomp.algebra.ssrint]
@@ -614,9 +612,12 @@ addmx_sub_adds [in mathcomp.algebra.mxalgebra]
addmx_sub [in mathcomp.algebra.mxalgebra]
addnA [in mathcomp.ssreflect.ssrnat]
+addnABC [in mathcomp.ssreflect.ssrnat]
addnAC [in mathcomp.ssreflect.ssrnat]
addnACA [in mathcomp.ssreflect.ssrnat]
addnBA [in mathcomp.ssreflect.ssrnat]
+addnBAC [in mathcomp.ssreflect.ssrnat]
+addnBCA [in mathcomp.ssreflect.ssrnat]
addnC [in mathcomp.ssreflect.ssrnat]
addnCA [in mathcomp.ssreflect.ssrnat]
addnE [in mathcomp.ssreflect.ssrnat]
@@ -868,12 +869,21 @@ alg_integral [in mathcomp.field.algebraics_fundamentals]
allP [in mathcomp.ssreflect.seq]
allpairsP [in mathcomp.ssreflect.seq]
+allpairsPdep [in mathcomp.ssreflect.seq]
allpairs_tupleP [in mathcomp.ssreflect.tuple]
allpairs_uniq [in mathcomp.ssreflect.seq]
+allpairs_f [in mathcomp.ssreflect.seq]
+allpairs_uniq_dep [in mathcomp.ssreflect.seq]
allpairs_catr [in mathcomp.ssreflect.seq]
+allpairs_f_dep [in mathcomp.ssreflect.seq]
+allpairs_mapr [in mathcomp.ssreflect.seq]
+allpairs_mapl [in mathcomp.ssreflect.seq]
allpairs_cat [in mathcomp.ssreflect.seq]
allPn [in mathcomp.ssreflect.seq]
+allPP [in mathcomp.ssreflect.seq]
all_tnthP [in mathcomp.ssreflect.tuple]
+all_iffP [in mathcomp.ssreflect.seq]
+all_iffLR [in mathcomp.ssreflect.seq]
all_map [in mathcomp.ssreflect.seq]
all_nthP [in mathcomp.ssreflect.seq]
all_pred1_nseq [in mathcomp.ssreflect.seq]
@@ -893,6 +903,7 @@ all_filterP [in mathcomp.ssreflect.seq]
all_count [in mathcomp.ssreflect.seq]
all_roots_prod_XsubC [in mathcomp.algebra.poly]
+all2E [in mathcomp.ssreflect.seq]
Alt_trans [in mathcomp.solvable.alt]
Alt_index [in mathcomp.solvable.alt]
Alt_norm [in mathcomp.solvable.alt]
@@ -910,6 +921,8 @@ amulr_inj [in mathcomp.field.falgebra]
annihilator_mxP [in mathcomp.character.mxrepresentation]
anti_leq [in mathcomp.ssreflect.ssrnat]
+anti_mono [in mathcomp.ssreflect.eqtype]
+anti_mono_in [in mathcomp.ssreflect.eqtype]
apermE [in mathcomp.fingroup.perm]
aperm_faithful [in mathcomp.solvable.alt]
aperm_is_action [in mathcomp.fingroup.action]
@@ -1074,7 +1087,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1106,14 +1119,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1138,7 +1151,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1170,7 +1183,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1202,7 +1215,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1234,7 +1247,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1266,7 +1279,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1298,7 +1311,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1330,14 +1343,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1362,7 +1375,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1394,7 +1407,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1426,7 +1439,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1458,14 +1471,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1490,7 +1503,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_B.html b/docs/htmldoc/index_lemma_B.html index 3f21f60..3713431 100644 --- a/docs/htmldoc/index_lemma_B.html +++ b/docs/htmldoc/index_lemma_B.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)

B (lemma)

@@ -575,11 +575,16 @@ big_pred1 [in mathcomp.ssreflect.bigop]
big_pred1_eq [in mathcomp.ssreflect.bigop]
big_allpairs [in mathcomp.ssreflect.bigop]
+big_allpairs_dep [in mathcomp.ssreflect.bigop]
big_cat [in mathcomp.ssreflect.bigop]
big_mkcondl [in mathcomp.ssreflect.bigop]
big_mkcondr [in mathcomp.ssreflect.bigop]
big_mkcond [in mathcomp.ssreflect.bigop]
big_seq1 [in mathcomp.ssreflect.bigop]
+big_image_id [in mathcomp.ssreflect.bigop]
+big_image_cond_id [in mathcomp.ssreflect.bigop]
+big_image [in mathcomp.ssreflect.bigop]
+big_image_cond [in mathcomp.ssreflect.bigop]
big_nseq [in mathcomp.ssreflect.bigop]
big_nseq_cond [in mathcomp.ssreflect.bigop]
big_const_ord [in mathcomp.ssreflect.bigop]
@@ -609,6 +614,7 @@ big_nat_cond [in mathcomp.ssreflect.bigop]
big_seq [in mathcomp.ssreflect.bigop]
big_seq_cond [in mathcomp.ssreflect.bigop]
+big_map_id [in mathcomp.ssreflect.bigop]
big_const_seq [in mathcomp.ssreflect.bigop]
big_catr [in mathcomp.ssreflect.bigop]
big_catl [in mathcomp.ssreflect.bigop]
@@ -636,11 +642,12 @@ big_ord1 [in mathcomp.algebra.zmodp]
big_trivIset [in mathcomp.ssreflect.finset]
big_trivIset_cond [in mathcomp.ssreflect.finset]
+big_imset_cond [in mathcomp.ssreflect.finset]
big_imset [in mathcomp.ssreflect.finset]
big_setU1 [in mathcomp.ssreflect.finset]
big_setD1 [in mathcomp.ssreflect.finset]
+big_setIDcond [in mathcomp.ssreflect.finset]
big_setID [in mathcomp.ssreflect.finset]
-big_setIDdep [in mathcomp.ssreflect.finset]
big_set1 [in mathcomp.ssreflect.finset]
big_set0 [in mathcomp.ssreflect.finset]
big1 [in mathcomp.ssreflect.bigop]
@@ -731,7 +738,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -763,14 +770,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -795,7 +802,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -827,7 +834,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -859,7 +866,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -891,7 +898,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -923,7 +930,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -955,7 +962,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -987,14 +994,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1019,7 +1026,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1051,7 +1058,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1083,7 +1090,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1115,14 +1122,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1147,7 +1154,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_C.html b/docs/htmldoc/index_lemma_C.html index accf48b..0ab5840 100644 --- a/docs/htmldoc/index_lemma_C.html +++ b/docs/htmldoc/index_lemma_C.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)

C (lemma)

@@ -641,8 +641,9 @@ card_ffun [in mathcomp.ssreflect.finfun]
card_ffun_on [in mathcomp.ssreflect.finfun]
card_pffun_on [in mathcomp.ssreflect.finfun]
-card_family [in mathcomp.ssreflect.finfun]
card_pfamily [in mathcomp.ssreflect.finfun]
+card_dep_ffun [in mathcomp.ssreflect.finfun]
+card_family [in mathcomp.ssreflect.finfun]
card_rVabelem [in mathcomp.character.mxabelem]
card_abelem_rV [in mathcomp.character.mxabelem]
card_rowg [in mathcomp.character.mxabelem]
@@ -1042,6 +1043,7 @@ cfExp_prime_transitive [in mathcomp.character.character]
cfIirrE [in mathcomp.character.character]
cfIirrPE [in mathcomp.character.character]
+cfIirr_key [in mathcomp.character.character]
cfIndE [in mathcomp.character.classfun]
cfIndEout [in mathcomp.character.classfun]
cfIndEsdprod [in mathcomp.character.classfun]
@@ -1363,6 +1365,7 @@ chinese_modr [in mathcomp.ssreflect.div]
chinese_modl [in mathcomp.ssreflect.div]
chinese_remainder [in mathcomp.ssreflect.div]
+choiceMixin [in mathcomp.ssreflect.finfun]
Choice.InternalTheory.complete [in mathcomp.ssreflect.choice]
Choice.InternalTheory.correct [in mathcomp.ssreflect.choice]
Choice.InternalTheory.extensional [in mathcomp.ssreflect.choice]
@@ -1449,6 +1452,55 @@ Clifford_hom [in mathcomp.character.mxrepresentation]
Clifford_simple [in mathcomp.character.mxrepresentation]
Clifford_Res_sum_cfclass [in mathcomp.character.inertia]
+ClosedFieldQE.abstrXP [in mathcomp.field.closed_field]
+ClosedFieldQE.abstrX_mulM [in mathcomp.field.closed_field]
+ClosedFieldQE.abstrX1 [in mathcomp.field.closed_field]
+ClosedFieldQE.eval_poly1 [in mathcomp.field.closed_field]
+ClosedFieldQE.eval_poly_mulM [in mathcomp.field.closed_field]
+ClosedFieldQE.eval_natmulpT [in mathcomp.field.closed_field]
+ClosedFieldQE.eval_opppT [in mathcomp.field.closed_field]
+ClosedFieldQE.eval_mulpT [in mathcomp.field.closed_field]
+ClosedFieldQE.eval_sumpT [in mathcomp.field.closed_field]
+ClosedFieldQE.eval_amulXnT [in mathcomp.field.closed_field]
+ClosedFieldQE.eval_lift [in mathcomp.field.closed_field]
+ClosedFieldQE.ex_elim_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.ex_elim_seq_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.ex_elim_seqP [in mathcomp.field.closed_field]
+ClosedFieldQE.holds_ex_elim [in mathcomp.field.closed_field]
+ClosedFieldQE.holds_conjn [in mathcomp.field.closed_field]
+ClosedFieldQE.holds_conj [in mathcomp.field.closed_field]
+ClosedFieldQE.isnullP [in mathcomp.field.closed_field]
+ClosedFieldQE.isnull_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.lead_coefT_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.lead_coefTP [in mathcomp.field.closed_field]
+ClosedFieldQE.qf_cps_if [in mathcomp.field.closed_field]
+ClosedFieldQE.qf_cps_bind [in mathcomp.field.closed_field]
+ClosedFieldQE.qf_cps_ret [in mathcomp.field.closed_field]
+ClosedFieldQE.qf_simpl [in mathcomp.field.closed_field]
+ClosedFieldQE.rabstrX [in mathcomp.field.closed_field]
+ClosedFieldQE.ramulXnT [in mathcomp.field.closed_field]
+ClosedFieldQE.redivpTP [in mathcomp.field.closed_field]
+ClosedFieldQE.redivpT_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.redivp_rec_loopP [in mathcomp.field.closed_field]
+ClosedFieldQE.redivp_rec_loopT_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.redivp_rec_loopTP [in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpTP [in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpTsP [in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpTs_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpT_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdp_loopT_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdp_loopP [in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcopTP [in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcopT_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcop_recT_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcop_recTP [in mathcomp.field.closed_field]
+ClosedFieldQE.rmulpT [in mathcomp.field.closed_field]
+ClosedFieldQE.rpoly_map_mul [in mathcomp.field.closed_field]
+ClosedFieldQE.rseq_poly_map [in mathcomp.field.closed_field]
+ClosedFieldQE.rsumpT [in mathcomp.field.closed_field]
+ClosedFieldQE.sizeTP [in mathcomp.field.closed_field]
+ClosedFieldQE.sizeT_qf [in mathcomp.field.closed_field]
+ClosedFieldQE.wf_ex_elim [in mathcomp.field.closed_field]
closed_field_poly_normal [in mathcomp.algebra.poly]
closed_nonrootP [in mathcomp.algebra.poly]
closed_rootP [in mathcomp.algebra.poly]
@@ -1485,6 +1537,7 @@ codom_val [in mathcomp.ssreflect.fintype]
codom_f [in mathcomp.ssreflect.fintype]
codom_ffun [in mathcomp.ssreflect.finfun]
+codom_tffun [in mathcomp.ssreflect.finfun]
coefB [in mathcomp.algebra.poly]
coefC [in mathcomp.algebra.poly]
coefCM [in mathcomp.algebra.poly]
@@ -1508,6 +1561,7 @@ coef_rVpoly_ord [in mathcomp.algebra.mxpoly]
coef_rVpoly [in mathcomp.algebra.mxpoly]
coef_swapXY [in mathcomp.algebra.polyXY]
+coef_comp_poly [in mathcomp.algebra.poly]
coef_map [in mathcomp.algebra.poly]
coef_map_id0 [in mathcomp.algebra.poly]
coef_nderivn [in mathcomp.algebra.poly]
@@ -1623,6 +1677,8 @@ comm1G [in mathcomp.solvable.commutator]
comm1g [in mathcomp.fingroup.fingroup]
comm3G1P [in mathcomp.solvable.commutator]
+companionmxK [in mathcomp.algebra.mxpoly]
+companion_map_poly [in mathcomp.algebra.mxpoly]
compareP [in mathcomp.ssreflect.eqtype]
complete_unitmx [in mathcomp.algebra.mxalgebra]
ComplexNumMixin [in mathcomp.field.algC]
@@ -1659,6 +1715,7 @@ comp_actE [in mathcomp.fingroup.action]
comp_is_action [in mathcomp.fingroup.action]
comp_poly2_eq0 [in mathcomp.algebra.poly]
+comp_poly_eq0 [in mathcomp.algebra.poly]
comp_polyA [in mathcomp.algebra.poly]
comp_polyM [in mathcomp.algebra.poly]
comp_poly_multiplicative [in mathcomp.algebra.poly]
@@ -1800,8 +1857,13 @@ contraTeq [in mathcomp.ssreflect.eqtype]
contraTneq [in mathcomp.ssreflect.eqtype]
contra_orbit [in mathcomp.fingroup.action]
+contra_eq_neq [in mathcomp.ssreflect.eqtype]
+contra_neq_eq [in mathcomp.ssreflect.eqtype]
contra_neq [in mathcomp.ssreflect.eqtype]
contra_eq [in mathcomp.ssreflect.eqtype]
+contra_neqT [in mathcomp.ssreflect.eqtype]
+contra_neqF [in mathcomp.ssreflect.eqtype]
+contra_neqN [in mathcomp.ssreflect.eqtype]
contra_eqT [in mathcomp.ssreflect.eqtype]
contra_eqF [in mathcomp.ssreflect.eqtype]
contra_eqN [in mathcomp.ssreflect.eqtype]
@@ -1920,8 +1982,9 @@ coset_splitting_field [in mathcomp.character.mxrepresentation]
coset1 [in mathcomp.fingroup.quotient]
coset1_injm [in mathcomp.fingroup.quotient]
-countable_algebraic_closure [in mathcomp.field.countalg]
-countable_field_extension [in mathcomp.field.countalg]
+countable_algebraic_closure [in mathcomp.field.closed_field]
+countable_field_extension [in mathcomp.field.closed_field]
+countMixin [in mathcomp.ssreflect.finfun]
count_flatten [in mathcomp.ssreflect.seq]
count_map [in mathcomp.ssreflect.seq]
count_mem_uniq [in mathcomp.ssreflect.seq]
@@ -1934,6 +1997,7 @@ count_predT [in mathcomp.ssreflect.seq]
count_pred0 [in mathcomp.ssreflect.seq]
count_cat [in mathcomp.ssreflect.seq]
+count_nseq [in mathcomp.ssreflect.seq]
count_size [in mathcomp.ssreflect.seq]
count_logn_dprod_cycle [in mathcomp.solvable.abelian]
cover_partition [in mathcomp.ssreflect.finset]
@@ -2087,7 +2151,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -2119,14 +2183,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -2151,7 +2215,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -2183,7 +2247,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -2215,7 +2279,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -2247,7 +2311,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -2279,7 +2343,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -2311,7 +2375,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -2343,14 +2407,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -2375,7 +2439,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -2407,7 +2471,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -2439,7 +2503,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -2471,14 +2535,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -2503,7 +2567,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_D.html b/docs/htmldoc/index_lemma_D.html index 0ec853a..811fcd8 100644 --- a/docs/htmldoc/index_lemma_D.html +++ b/docs/htmldoc/index_lemma_D.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)

D (lemma)

@@ -473,6 +473,8 @@ dchi_vchar [in mathcomp.character.vcharacter]
dchi_ndirrE [in mathcomp.character.vcharacter]
dchi1 [in mathcomp.character.vcharacter]
+decrn_inj_in [in mathcomp.ssreflect.ssrnat]
+decrn_inj [in mathcomp.ssreflect.ssrnat]
DecSocleType [in mathcomp.character.mxrepresentation]
dec_mx_reducible_semisimple [in mathcomp.character.mxrepresentation]
dec_mxsimple_exists [in mathcomp.character.mxrepresentation]
@@ -819,6 +821,7 @@ dprod_nil [in mathcomp.solvable.nilpotent]
dprod1g [in mathcomp.fingroup.gproduct]
drop_tupleP [in mathcomp.ssreflect.tuple]
+drop_subseq [in mathcomp.ssreflect.seq]
drop_rev [in mathcomp.ssreflect.seq]
drop_nth [in mathcomp.ssreflect.seq]
drop_rcons [in mathcomp.ssreflect.seq]
@@ -979,7 +982,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1011,14 +1014,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1043,7 +1046,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1075,7 +1078,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1107,7 +1110,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1139,7 +1142,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1171,7 +1174,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1203,7 +1206,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1235,14 +1238,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1267,7 +1270,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1299,7 +1302,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1331,7 +1334,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1363,14 +1366,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1395,7 +1398,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_E.html b/docs/htmldoc/index_lemma_E.html index 0e90174..a86d944 100644 --- a/docs/htmldoc/index_lemma_E.html +++ b/docs/htmldoc/index_lemma_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 (lemma)

@@ -471,7 +471,6 @@ edivnP [in mathcomp.ssreflect.div]
edivn_def [in mathcomp.ssreflect.div]
edivn_eq [in mathcomp.ssreflect.div]
-edivn2P [in mathcomp.ssreflect.prime]
egcdnP [in mathcomp.ssreflect.div]
egcdzP [in mathcomp.algebra.intdiv]
egcd0n [in mathcomp.ssreflect.div]
@@ -480,7 +479,6 @@ eigenvalue_root_min [in mathcomp.algebra.mxpoly]
eigenvalue_root_char [in mathcomp.algebra.mxpoly]
eigenvalue_map [in mathcomp.algebra.mxalgebra]
-elogn2P [in mathcomp.ssreflect.prime]
eltmE [in mathcomp.solvable.cyclic]
eltmM [in mathcomp.solvable.cyclic]
eltm_id [in mathcomp.solvable.cyclic]
@@ -578,13 +576,16 @@ eqg_mx_irr [in mathcomp.character.mxrepresentation]
eqg_mx_faithful [in mathcomp.character.mxrepresentation]
eqg_repr_proof [in mathcomp.character.mxrepresentation]
+eqitvP [in mathcomp.algebra.interval]
eqlfunP [in mathcomp.algebra.vector]
eqlfun_inP [in mathcomp.algebra.vector]
+eqMixin [in mathcomp.ssreflect.finfun]
eqmodE [in mathcomp.ssreflect.generic_quotient]
eqmodP [in mathcomp.ssreflect.generic_quotient]
eqmxMfree [in mathcomp.algebra.mxalgebra]
eqmxMfull [in mathcomp.algebra.mxalgebra]
eqmxMr [in mathcomp.algebra.mxalgebra]
+eqmxMunitP [in mathcomp.algebra.mxalgebra]
eqmxP [in mathcomp.algebra.mxalgebra]
eqmx_semisimple [in mathcomp.character.mxrepresentation]
eqmx_iso [in mathcomp.character.mxrepresentation]
@@ -697,10 +698,13 @@ eq_quot_countMixin [in mathcomp.ssreflect.generic_quotient]
eq_op_trans [in mathcomp.ssreflect.generic_quotient]
eq_lock [in mathcomp.ssreflect.generic_quotient]
+eq_itv_boundP [in mathcomp.algebra.interval]
+eq_mktuple [in mathcomp.ssreflect.tuple]
eq_from_tnth [in mathcomp.ssreflect.tuple]
eq_block_mx [in mathcomp.algebra.matrix]
eq_col_mx [in mathcomp.algebra.matrix]
eq_row_mx [in mathcomp.algebra.matrix]
+eq_mx [in mathcomp.algebra.matrix]
eq_Aut [in mathcomp.fingroup.automorphism]
eq_subZnat_irr [in mathcomp.character.character]
eq_addZ_irr [in mathcomp.character.character]
@@ -710,11 +714,15 @@ eq_irr_mem_classP [in mathcomp.character.character]
eq_sum_nth_irr [in mathcomp.character.character]
eq_Mod8_D8 [in mathcomp.solvable.extremal]
+eq_in_allpairs [in mathcomp.ssreflect.seq]
+eq_in_allpairs_dep [in mathcomp.ssreflect.seq]
+eq_allpairs [in mathcomp.ssreflect.seq]
eq_from_flatten_shape [in mathcomp.ssreflect.seq]
eq_mkseq [in mathcomp.ssreflect.seq]
eq_pmap [in mathcomp.ssreflect.seq]
eq_in_map [in mathcomp.ssreflect.seq]
eq_map [in mathcomp.ssreflect.seq]
+eq_uniq [in mathcomp.ssreflect.seq]
eq_all_r [in mathcomp.ssreflect.seq]
eq_has_r [in mathcomp.ssreflect.seq]
eq_in_has [in mathcomp.ssreflect.seq]
@@ -774,11 +782,11 @@ eq_ex_minn [in mathcomp.ssreflect.ssrnat]
eq_leq [in mathcomp.ssreflect.ssrnat]
eq_map_poly [in mathcomp.algebra.poly]
+eq_poly [in mathcomp.algebra.poly]
eq_prim_root_expr [in mathcomp.algebra.poly]
eq_bigmax [in mathcomp.ssreflect.bigop]
eq_bigmax_cond [in mathcomp.ssreflect.bigop]
eq_big_idem [in mathcomp.ssreflect.bigop]
-eq_big_perm [in mathcomp.ssreflect.bigop]
eq_big_idx [in mathcomp.ssreflect.bigop]
eq_big_idx_seq [in mathcomp.ssreflect.bigop]
eq_big_nat [in mathcomp.ssreflect.bigop]
@@ -787,6 +795,8 @@ eq_bigr [in mathcomp.ssreflect.bigop]
eq_bigl [in mathcomp.ssreflect.bigop]
eq_big_op [in mathcomp.ssreflect.bigop]
+eq_ffun [in mathcomp.ssreflect.finfun]
+eq_dffun [in mathcomp.ssreflect.finfun]
eq_Tagged [in mathcomp.ssreflect.eqtype]
eq_tag [in mathcomp.ssreflect.eqtype]
eq_frel [in mathcomp.ssreflect.eqtype]
@@ -828,19 +838,12 @@ eq_in_imset [in mathcomp.ssreflect.finset]
eq_imset [in mathcomp.ssreflect.finset]
eq_preimset [in mathcomp.ssreflect.finset]
+eq_finset [in mathcomp.ssreflect.finset]
Euclid_dvdX [in mathcomp.ssreflect.prime]
Euclid_dvd1 [in mathcomp.ssreflect.prime]
Euclid_dvdM [in mathcomp.ssreflect.prime]
Euler_exp_totient [in mathcomp.solvable.cyclic]
eval_mxmodule [in mathcomp.character.mxrepresentation]
-eval_poly1 [in mathcomp.field.closed_field]
-eval_poly_mulM [in mathcomp.field.closed_field]
-eval_natmulpT [in mathcomp.field.closed_field]
-eval_opppT [in mathcomp.field.closed_field]
-eval_mulpT [in mathcomp.field.closed_field]
-eval_sumpT [in mathcomp.field.closed_field]
-eval_amulXnT [in mathcomp.field.closed_field]
-eval_lift [in mathcomp.field.closed_field]
even_prime [in mathcomp.ssreflect.prime]
exchange_big_nat [in mathcomp.ssreflect.bigop]
exchange_big_dep_nat [in mathcomp.ssreflect.bigop]
@@ -852,6 +855,7 @@ exists_acomps [in mathcomp.solvable.jordanholder]
exists_comps [in mathcomp.solvable.jordanholder]
exists_eq_inP [in mathcomp.ssreflect.fintype]
+exists_inPP [in mathcomp.ssreflect.fintype]
exists_inP [in mathcomp.ssreflect.fintype]
exists_eqP [in mathcomp.ssreflect.fintype]
expand_det_col [in mathcomp.algebra.matrix]
@@ -999,6 +1003,7 @@ Extremal.Grp [in mathcomp.solvable.extremal]
Extremal.gtype_key [in mathcomp.solvable.extremal]
extremal2_structure [in mathcomp.solvable.extremal]
+extremumP [in mathcomp.ssreflect.fintype]
ext_coprime_quotient_cent [in mathcomp.solvable.hall]
ext_coprime_Hall_subset [in mathcomp.solvable.hall]
ext_norm_conj_cent [in mathcomp.solvable.hall]
@@ -1008,9 +1013,6 @@ ex_maxnP [in mathcomp.ssreflect.ssrnat]
ex_maxn_subproof [in mathcomp.ssreflect.ssrnat]
ex_minnP [in mathcomp.ssreflect.ssrnat]
-ex_elim_qf [in mathcomp.field.closed_field]
-ex_elim_seq_qf [in mathcomp.field.closed_field]
-ex_elim_seqP [in mathcomp.field.closed_field]
ex_mingroup [in mathcomp.fingroup.fingroup]
ex_maxgroup [in mathcomp.fingroup.fingroup]
ex_maxset [in mathcomp.ssreflect.finset]
@@ -1046,7 +1048,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1078,14 +1080,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1110,7 +1112,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1142,7 +1144,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1174,7 +1176,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1206,7 +1208,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1238,7 +1240,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1270,7 +1272,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1302,14 +1304,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1334,7 +1336,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1366,7 +1368,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1398,7 +1400,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1430,14 +1432,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1462,7 +1464,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_F.html b/docs/htmldoc/index_lemma_F.html index 97a2f94..537c384 100644 --- a/docs/htmldoc/index_lemma_F.html +++ b/docs/htmldoc/index_lemma_F.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)

F (lemma)

@@ -561,8 +561,11 @@ ffun_addA [in mathcomp.algebra.ssralg]
ffun_vect_iso [in mathcomp.algebra.vector]
ffun_onP [in mathcomp.ssreflect.finfun]
+ffun0 [in mathcomp.ssreflect.finfun]
ffun1_nonzero [in mathcomp.algebra.ssralg]
+fgraphK [in mathcomp.ssreflect.finfun]
fgraph_codom [in mathcomp.ssreflect.finfun]
+fgraph_ffun0 [in mathcomp.ssreflect.finfun]
Fid [in mathcomp.solvable.burnside_app]
Fid3 [in mathcomp.solvable.burnside_app]
fieldExt_hornerZ [in mathcomp.field.fieldext]
@@ -601,6 +604,7 @@ filter_pred0 [in mathcomp.ssreflect.seq]
filter_rcons [in mathcomp.ssreflect.seq]
filter_cat [in mathcomp.ssreflect.seq]
+filter_nseq [in mathcomp.ssreflect.seq]
filter_id [in mathcomp.ssreflect.seq]
filter_all [in mathcomp.ssreflect.seq]
filter_pairwise_orthogonal [in mathcomp.character.classfun]
@@ -620,6 +624,8 @@ finField_galois [in mathcomp.field.finfield]
finField_is_abelem [in mathcomp.field.finfield]
finField_genPoly [in mathcomp.field.finfield]
+FinfunDef.finfunE [in mathcomp.ssreflect.finfun]
+FinfunK [in mathcomp.ssreflect.finfun]
FinGroup.mk_invMg [in mathcomp.fingroup.fingroup]
FinGroup.mk_invgK [in mathcomp.fingroup.fingroup]
FiniteModule.actAr [in mathcomp.solvable.finmodule]
@@ -756,13 +762,17 @@ fmorph_primitive_root [in mathcomp.algebra.poly]
fmorph_unity_root [in mathcomp.algebra.poly]
fmorph_root [in mathcomp.algebra.poly]
+foldlE [in mathcomp.ssreflect.bigop]
foldl_cat [in mathcomp.ssreflect.seq]
foldl_rev [in mathcomp.ssreflect.seq]
+foldl_idx [in mathcomp.ssreflect.bigop]
+foldrE [in mathcomp.ssreflect.bigop]
foldr_map [in mathcomp.ssreflect.seq]
foldr_cat [in mathcomp.ssreflect.seq]
forallb_tnth [in mathcomp.ssreflect.tuple]
forallP [in mathcomp.ssreflect.fintype]
forallPP [in mathcomp.ssreflect.fintype]
+forall_inPP [in mathcomp.ssreflect.fintype]
forall_inP [in mathcomp.ssreflect.fintype]
fpathP [in mathcomp.ssreflect.path]
fpath_traject [in mathcomp.ssreflect.path]
@@ -857,8 +867,6 @@ froot_id [in mathcomp.ssreflect.fingraph]
fst_morphM [in mathcomp.fingroup.gproduct]
Fundamental_Theorem_of_Algebraics [in mathcomp.field.algebraics_fundamentals]
-FunFinfun.finfunE [in mathcomp.ssreflect.finfun]
-FunFinfun.fun_of_finE [in mathcomp.ssreflect.finfun]
fun_of_lfunK [in mathcomp.algebra.vector]
f_invF [in mathcomp.ssreflect.fintype]
f_iinv [in mathcomp.ssreflect.fintype]
@@ -925,7 +933,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -957,14 +965,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -989,7 +997,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1021,7 +1029,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1053,7 +1061,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1085,7 +1093,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1117,7 +1125,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1149,7 +1157,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1181,14 +1189,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1213,7 +1221,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1245,7 +1253,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1277,7 +1285,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1309,14 +1317,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1341,7 +1349,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_G.html b/docs/htmldoc/index_lemma_G.html index f91903a..f324abc 100644 --- a/docs/htmldoc/index_lemma_G.html +++ b/docs/htmldoc/index_lemma_G.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)

G (lemma)

@@ -901,6 +901,7 @@ GRing.invr1 [in mathcomp.algebra.ssralg]
GRing.in_algE [in mathcomp.algebra.ssralg]
GRing.in_alg_is_rmorphism [in mathcomp.algebra.ssralg]
+GRing.lastr_eq0 [in mathcomp.algebra.ssralg]
GRing.linearB [in mathcomp.algebra.ssralg]
GRing.linearD [in mathcomp.algebra.ssralg]
GRing.linearMn [in mathcomp.algebra.ssralg]
@@ -1317,11 +1318,6 @@ group0 [in mathcomp.fingroup.gproduct]
group1 [in mathcomp.fingroup.fingroup]
group1_contra [in mathcomp.fingroup.fingroup]
-group1_finType [in mathcomp.fingroup.fingroup]
-group1_eqType [in mathcomp.fingroup.fingroup]
-group1_class12 [in mathcomp.fingroup.fingroup]
-group1_class2 [in mathcomp.fingroup.fingroup]
-group1_class1 [in mathcomp.fingroup.fingroup]
Grp_pX1p2 [in mathcomp.solvable.extraspecial]
Grp_quaternion [in mathcomp.solvable.extremal]
Grp_semidihedral [in mathcomp.solvable.extremal]
@@ -1338,6 +1334,7 @@ gtz0_abs [in mathcomp.algebra.ssrint]
gtz0_ge1 [in mathcomp.algebra.ssrint]
gt_rat0 [in mathcomp.algebra.rat]
+gt_size_poly_neq0 [in mathcomp.algebra.poly]
gt0CG [in mathcomp.character.classfun]
gt0CiG [in mathcomp.character.classfun]


@@ -1371,7 +1368,7 @@ - + @@ -1403,14 +1400,14 @@ - + - + @@ -1435,7 +1432,7 @@ - + @@ -1467,7 +1464,7 @@ - + @@ -1499,7 +1496,7 @@ - + @@ -1531,7 +1528,7 @@ - + @@ -1563,7 +1560,7 @@ - + @@ -1595,7 +1592,7 @@ - + @@ -1627,14 +1624,14 @@ - + - + @@ -1659,7 +1656,7 @@ - + @@ -1691,7 +1688,7 @@ - + @@ -1723,7 +1720,7 @@ - + @@ -1755,14 +1752,14 @@ - + - + @@ -1787,7 +1784,7 @@ - +
Z _ other(23233 entries)(23836 entries)
Notation IndexZ _ other(1373 entries)(1409 entries)
Module Index A B CDD E F GZ _ other(213 entries)(221 entries)
Variable IndexZ _ other(3475 entries)(3574 entries)
Library IndexZ _ other(89 entries)(90 entries)
Lemma IndexZ _ other(11853 entries)(12096 entries)
Constructor IndexZ _ other(359 entries)(368 entries)
Axiom IndexZ _ other(47 entries)(45 entries)
Inductive IndexZ _ other(103 entries)(107 entries)
Projection Index A B CDD E F GZ _ other(266 entries)(273 entries)
Section IndexZ _ other(1118 entries)(1140 entries)
Abbreviation IndexZ _ other(691 entries)(728 entries)
Definition IndexZ _ other(3461 entries)(3596 entries)
Record Index A B CDD E F GZ _ other(185 entries)(189 entries)
diff --git a/docs/htmldoc/index_lemma_H.html b/docs/htmldoc/index_lemma_H.html index 85ef710..b6868bf 100644 --- a/docs/htmldoc/index_lemma_H.html +++ b/docs/htmldoc/index_lemma_H.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)

H (lemma)

@@ -489,6 +489,7 @@ Hall1 [in mathcomp.solvable.pgroup]
hasP [in mathcomp.ssreflect.seq]
hasPn [in mathcomp.ssreflect.seq]
+hasPP [in mathcomp.ssreflect.seq]
has_tnthP [in mathcomp.ssreflect.tuple]
has_nonprincipal_irr [in mathcomp.character.character]
has_map [in mathcomp.ssreflect.seq]
@@ -519,9 +520,6 @@ has_non_scalar_mxP [in mathcomp.algebra.mxalgebra]
headI [in mathcomp.ssreflect.seq]
Hilbert's_theorem_90 [in mathcomp.field.galois]
-holds_ex_elim [in mathcomp.field.closed_field]
-holds_conjn [in mathcomp.field.closed_field]
-holds_conj [in mathcomp.field.closed_field]
homgP [in mathcomp.fingroup.morphism]
homGrp_trans [in mathcomp.fingroup.presentation]
homg_quotientS [in mathcomp.fingroup.quotient]
@@ -529,6 +527,14 @@ homg_refl [in mathcomp.fingroup.morphism]
homocyclic_Ohm_Mho [in mathcomp.solvable.abelian]
homocyclic1 [in mathcomp.solvable.abelian]
+homoW [in mathcomp.ssreflect.eqtype]
+homoW_in [in mathcomp.ssreflect.eqtype]
+homo_inj_lt_in [in mathcomp.ssreflect.ssrnat]
+homo_inj_lt [in mathcomp.ssreflect.ssrnat]
+homo_leq [in mathcomp.ssreflect.ssrnat]
+homo_leq_in [in mathcomp.ssreflect.ssrnat]
+homo_ltn [in mathcomp.ssreflect.ssrnat]
+homo_ltn_in [in mathcomp.ssreflect.ssrnat]
hom_component_mx [in mathcomp.character.mxrepresentation]
hom_component_mx_iso [in mathcomp.character.mxrepresentation]
hom_mxsemisimple_iso [in mathcomp.character.mxrepresentation]
@@ -615,7 +621,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -647,14 +653,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -679,7 +685,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -711,7 +717,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -743,7 +749,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -775,7 +781,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -807,7 +813,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -839,7 +845,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -871,14 +877,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -903,7 +909,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -935,7 +941,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -967,7 +973,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -999,14 +1005,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1031,7 +1037,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_I.html b/docs/htmldoc/index_lemma_I.html index e7eb210..7985b79 100644 --- a/docs/htmldoc/index_lemma_I.html +++ b/docs/htmldoc/index_lemma_I.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)

I (lemma)

@@ -482,7 +482,6 @@ id_is_ahom [in mathcomp.field.falgebra]
ieexprIz [in mathcomp.algebra.ssrint]
ifactmE [in mathcomp.fingroup.morphism]
-ifnzP [in mathcomp.ssreflect.prime]
ifN_eqC [in mathcomp.ssreflect.eqtype]
ifN_eq [in mathcomp.ssreflect.eqtype]
iinv_f [in mathcomp.ssreflect.fintype]
@@ -563,6 +562,9 @@ im_eltm [in mathcomp.solvable.cyclic]
im_Zpm [in mathcomp.solvable.cyclic]
im_transversal_repr [in mathcomp.ssreflect.finset]
+incrn_inj_in [in mathcomp.ssreflect.ssrnat]
+incrn_inj [in mathcomp.ssreflect.ssrnat]
+incr_tallyP [in mathcomp.ssreflect.seq]
incr_nthC [in mathcomp.ssreflect.seq]
incr_nth_inj [in mathcomp.ssreflect.seq]
indexgg [in mathcomp.fingroup.fingroup]
@@ -732,6 +734,8 @@ inj_map [in mathcomp.ssreflect.seq]
inj_card_bij [in mathcomp.ssreflect.fintype]
inj_card_onto [in mathcomp.ssreflect.fintype]
+inj_homo [in mathcomp.ssreflect.eqtype]
+inj_homo_in [in mathcomp.ssreflect.eqtype]
inj_eqAxiom [in mathcomp.ssreflect.eqtype]
inj_in_eq [in mathcomp.ssreflect.eqtype]
inj_eq [in mathcomp.ssreflect.eqtype]
@@ -989,8 +993,6 @@ irr1_gt0 [in mathcomp.character.character]
irr1_degree [in mathcomp.character.character]
isgroupP [in mathcomp.fingroup.fingroup]
-isnullP [in mathcomp.field.closed_field]
-isnull_qf [in mathcomp.field.closed_field]
isogEcard [in mathcomp.fingroup.morphism]
isogEhom [in mathcomp.fingroup.morphism]
isogP [in mathcomp.fingroup.morphism]
@@ -1100,9 +1102,12 @@ iter_in [in mathcomp.ssreflect.fingraph]
iter_findex [in mathcomp.ssreflect.fingraph]
itvP [in mathcomp.algebra.interval]
+itv_intersectionA [in mathcomp.algebra.interval]
+itv_intersectionC [in mathcomp.algebra.interval]
itv_splitU2 [in mathcomp.algebra.interval]
itv_splitU [in mathcomp.algebra.interval]
itv_splitI [in mathcomp.algebra.interval]
+itv_intersectionii [in mathcomp.algebra.interval]
itv_gte [in mathcomp.algebra.interval]
itv_xx [in mathcomp.algebra.interval]
itv_boundlr [in mathcomp.algebra.interval]
@@ -1138,7 +1143,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1170,14 +1175,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1202,7 +1207,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1234,7 +1239,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1266,7 +1271,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1298,7 +1303,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1330,7 +1335,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1362,7 +1367,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1394,14 +1399,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1426,7 +1431,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1458,7 +1463,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1490,7 +1495,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1522,14 +1527,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1554,7 +1559,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_J.html b/docs/htmldoc/index_lemma_J.html index ade4879..ec8f1f7 100644 --- a/docs/htmldoc/index_lemma_J.html +++ b/docs/htmldoc/index_lemma_J.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)

J (lemma)

diff --git a/docs/htmldoc/index_lemma_K.html b/docs/htmldoc/index_lemma_K.html index 87a0ee2..ec66145 100644 --- a/docs/htmldoc/index_lemma_K.html +++ b/docs/htmldoc/index_lemma_K.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)

K (lemma)

@@ -576,7 +576,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -608,14 +608,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -640,7 +640,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -672,7 +672,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -704,7 +704,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -736,7 +736,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -768,7 +768,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -800,7 +800,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -832,14 +832,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -864,7 +864,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -896,7 +896,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -928,7 +928,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -960,14 +960,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -992,7 +992,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_L.html b/docs/htmldoc/index_lemma_L.html index 01a0b94..762636e 100644 --- a/docs/htmldoc/index_lemma_L.html +++ b/docs/htmldoc/index_lemma_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 (lemma)

@@ -477,6 +477,7 @@ lastP [in mathcomp.ssreflect.seq]
last_traject [in mathcomp.ssreflect.path]
last_map [in mathcomp.ssreflect.seq]
+last_eq [in mathcomp.ssreflect.seq]
last_nth [in mathcomp.ssreflect.seq]
last_ind [in mathcomp.ssreflect.seq]
last_rcons [in mathcomp.ssreflect.seq]
@@ -556,6 +557,7 @@ lead_coefX [in mathcomp.algebra.poly]
lead_coef_proper_mul [in mathcomp.algebra.poly]
lead_coef1 [in mathcomp.algebra.poly]
+lead_coefDr [in mathcomp.algebra.poly]
lead_coefDl [in mathcomp.algebra.poly]
lead_coef_opp [in mathcomp.algebra.poly]
lead_coef_eq0 [in mathcomp.algebra.poly]
@@ -563,8 +565,6 @@ lead_coef_poly [in mathcomp.algebra.poly]
lead_coefC [in mathcomp.algebra.poly]
lead_coefE [in mathcomp.algebra.poly]
-lead_coefT_qf [in mathcomp.field.closed_field]
-lead_coefTP [in mathcomp.field.closed_field]
left_arc [in mathcomp.ssreflect.path]
left_trans [in mathcomp.ssreflect.generic_quotient]
leNz_nat [in mathcomp.algebra.ssrint]
@@ -584,8 +584,13 @@ leqP [in mathcomp.ssreflect.ssrnat]
leqSpred [in mathcomp.ssreflect.ssrnat]
leqW [in mathcomp.ssreflect.ssrnat]
+leqW_nmono_in [in mathcomp.ssreflect.ssrnat]
+leqW_mono_in [in mathcomp.ssreflect.ssrnat]
+leqW_nmono [in mathcomp.ssreflect.ssrnat]
+leqW_mono [in mathcomp.ssreflect.ssrnat]
leq_quotient [in mathcomp.fingroup.quotient]
leq_bin2l [in mathcomp.ssreflect.binomial]
+leq_index [in mathcomp.ssreflect.path]
leq_divLR [in mathcomp.ssreflect.div]
leq_divDl [in mathcomp.ssreflect.div]
leq_div2l [in mathcomp.ssreflect.div]
@@ -594,12 +599,15 @@ leq_div [in mathcomp.ssreflect.div]
leq_mod [in mathcomp.ssreflect.div]
leq_trunc_div [in mathcomp.ssreflect.div]
-leq_size_perm [in mathcomp.ssreflect.seq]
leq_size_uniq [in mathcomp.ssreflect.seq]
leq_ord [in mathcomp.ssreflect.fintype]
leq_bump2 [in mathcomp.ssreflect.fintype]
leq_bump [in mathcomp.ssreflect.fintype]
leq_image_card [in mathcomp.ssreflect.fintype]
+leq_nmono_in [in mathcomp.ssreflect.ssrnat]
+leq_mono_in [in mathcomp.ssreflect.ssrnat]
+leq_nmono [in mathcomp.ssreflect.ssrnat]
+leq_mono [in mathcomp.ssreflect.ssrnat]
leq_sqr [in mathcomp.ssreflect.ssrnat]
leq_Sdouble [in mathcomp.ssreflect.ssrnat]
leq_double [in mathcomp.ssreflect.ssrnat]
@@ -632,6 +640,7 @@ leq_ltn_trans [in mathcomp.ssreflect.ssrnat]
leq_trans [in mathcomp.ssreflect.ssrnat]
leq_eqVlt [in mathcomp.ssreflect.ssrnat]
+leq_gtF [in mathcomp.ssreflect.ssrnat]
leq_pred [in mathcomp.ssreflect.ssrnat]
leq_sizeP [in mathcomp.algebra.poly]
leq_bigmax [in mathcomp.ssreflect.bigop]
@@ -652,7 +661,43 @@ lersifW [in mathcomp.algebra.interval]
lersifxx [in mathcomp.algebra.interval]
lersif_in_itv [in mathcomp.algebra.interval]
+lersif_ndivr_mull [in mathcomp.algebra.interval]
+lersif_ndivl_mull [in mathcomp.algebra.interval]
+lersif_ndivr_mulr [in mathcomp.algebra.interval]
+lersif_ndivl_mulr [in mathcomp.algebra.interval]
+lersif_pdivr_mull [in mathcomp.algebra.interval]
+lersif_pdivl_mull [in mathcomp.algebra.interval]
+lersif_pdivr_mulr [in mathcomp.algebra.interval]
+lersif_pdivl_mulr [in mathcomp.algebra.interval]
+lersif_maxl [in mathcomp.algebra.interval]
+lersif_maxr [in mathcomp.algebra.interval]
+lersif_minl [in mathcomp.algebra.interval]
+lersif_minr [in mathcomp.algebra.interval]
+lersif_distl [in mathcomp.algebra.interval]
+lersif_normr [in mathcomp.algebra.interval]
+lersif_norml [in mathcomp.algebra.interval]
+lersif_nnormr [in mathcomp.algebra.interval]
+lersif_nmul2r [in mathcomp.algebra.interval]
+lersif_nmul2l [in mathcomp.algebra.interval]
+lersif_pmul2r [in mathcomp.algebra.interval]
+lersif_pmul2l [in mathcomp.algebra.interval]
+lersif_imply [in mathcomp.algebra.interval]
+lersif_orb [in mathcomp.algebra.interval]
+lersif_andb [in mathcomp.algebra.interval]
+lersif_subr_addl [in mathcomp.algebra.interval]
+lersif_subl_addl [in mathcomp.algebra.interval]
+lersif_subr_addr [in mathcomp.algebra.interval]
+lersif_subl_addr [in mathcomp.algebra.interval]
+lersif_add2r [in mathcomp.algebra.interval]
+lersif_add2l [in mathcomp.algebra.interval]
+lersif_opp2 [in mathcomp.algebra.interval]
+lersif_oppr0 [in mathcomp.algebra.interval]
+lersif_0oppr [in mathcomp.algebra.interval]
+lersif_oppr [in mathcomp.algebra.interval]
+lersif_oppl [in mathcomp.algebra.interval]
+lersif_anti [in mathcomp.algebra.interval]
lersif_trans [in mathcomp.algebra.interval]
+lersif01 [in mathcomp.algebra.interval]
lerz0 [in mathcomp.algebra.ssrint]
lerz1 [in mathcomp.algebra.ssrint]
ler_rat [in mathcomp.algebra.rat]
@@ -696,10 +741,16 @@ le_rat0M [in mathcomp.algebra.rat]
le_rat0D [in mathcomp.algebra.rat]
le_rat0 [in mathcomp.algebra.rat]
+le_boundr_total [in mathcomp.algebra.interval]
+le_boundl_total [in mathcomp.algebra.interval]
+le_boundr_anti [in mathcomp.algebra.interval]
+le_boundl_anti [in mathcomp.algebra.interval]
le_boundr_bb [in mathcomp.algebra.interval]
le_boundl_bb [in mathcomp.algebra.interval]
-le_boundl_refl [in mathcomp.algebra.interval]
+le_boundr_trans [in mathcomp.algebra.interval]
+le_boundl_trans [in mathcomp.algebra.interval]
le_boundr_refl [in mathcomp.algebra.interval]
+le_boundl_refl [in mathcomp.algebra.interval]
le_irrelevance [in mathcomp.ssreflect.ssrnat]
le0z_nat [in mathcomp.algebra.ssrint]
lfunE [in mathcomp.algebra.vector]
@@ -846,9 +897,14 @@ ltnS [in mathcomp.ssreflect.ssrnat]
ltnSn [in mathcomp.ssreflect.ssrnat]
ltnW [in mathcomp.ssreflect.ssrnat]
+ltnW_nhomo_in [in mathcomp.ssreflect.ssrnat]
+ltnW_homo_in [in mathcomp.ssreflect.ssrnat]
+ltnW_nhomo [in mathcomp.ssreflect.ssrnat]
+ltnW_homo [in mathcomp.ssreflect.ssrnat]
ltNz_nat [in mathcomp.algebra.ssrint]
ltn_log_quotient [in mathcomp.solvable.pgroup]
ltn_quotient [in mathcomp.fingroup.quotient]
+ltn_index [in mathcomp.ssreflect.path]
ltn_sorted_uniq_leq [in mathcomp.ssreflect.path]
ltn_odd_Frobenius_ker [in mathcomp.solvable.frobenius]
ltn_logl [in mathcomp.ssreflect.prime]
@@ -887,6 +943,7 @@ ltn_add2l [in mathcomp.ssreflect.ssrnat]
ltn_trans [in mathcomp.ssreflect.ssrnat]
ltn_neqAle [in mathcomp.ssreflect.ssrnat]
+ltn_geF [in mathcomp.ssreflect.ssrnat]
ltn_eqF [in mathcomp.ssreflect.ssrnat]
ltn_predK [in mathcomp.ssreflect.ssrnat]
ltn_morphim [in mathcomp.fingroup.morphism]
@@ -894,6 +951,7 @@ ltn0Sn [in mathcomp.ssreflect.ssrnat]
ltP [in mathcomp.ssreflect.ssrnat]
ltrq0 [in mathcomp.algebra.rat]
+ltrW_lersif [in mathcomp.algebra.interval]
ltrz0 [in mathcomp.algebra.ssrint]
ltrz1 [in mathcomp.algebra.ssrint]
ltr_rat [in mathcomp.algebra.rat]
@@ -965,7 +1023,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -997,14 +1055,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1029,7 +1087,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1061,7 +1119,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1093,7 +1151,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1125,7 +1183,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1157,7 +1215,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1189,7 +1247,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1221,14 +1279,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1253,7 +1311,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1285,7 +1343,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1317,7 +1375,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1349,14 +1407,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1381,7 +1439,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_M.html b/docs/htmldoc/index_lemma_M.html index 72cf96d..a223f25 100644 --- a/docs/htmldoc/index_lemma_M.html +++ b/docs/htmldoc/index_lemma_M.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)

M (lemma)

@@ -547,6 +547,7 @@ map_trmx [in mathcomp.algebra.matrix]
map_mx_key [in mathcomp.algebra.matrix]
map_mx_inv_horner [in mathcomp.algebra.mxpoly]
+map_mx_companion [in mathcomp.algebra.mxpoly]
map_horner_mx [in mathcomp.algebra.mxpoly]
map_powers_mx [in mathcomp.algebra.mxpoly]
map_resultant [in mathcomp.algebra.mxpoly]
@@ -557,6 +558,7 @@ map_div_annihilantP [in mathcomp.algebra.polyXY]
map_sub_annihilantP [in mathcomp.algebra.polyXY]
map_Qnum_poly [in mathcomp.field.algnum]
+map_allpairs [in mathcomp.ssreflect.seq]
map_reshape [in mathcomp.ssreflect.seq]
map_flatten [in mathcomp.ssreflect.seq]
map_pK [in mathcomp.ssreflect.seq]
@@ -889,11 +891,14 @@ mem_Cint_span [in mathcomp.field.algnum]
mem_Crat_span [in mathcomp.field.algnum]
mem_irr [in mathcomp.character.character]
+mem_permutations [in mathcomp.ssreflect.seq]
mem_allpairs [in mathcomp.ssreflect.seq]
+mem_allpairs_dep [in mathcomp.ssreflect.seq]
mem_iota [in mathcomp.ssreflect.seq]
mem_pmap_sub [in mathcomp.ssreflect.seq]
mem_pmap [in mathcomp.ssreflect.seq]
mem_map [in mathcomp.ssreflect.seq]
+mem_rem_uniqF [in mathcomp.ssreflect.seq]
mem_rem_uniq [in mathcomp.ssreflect.seq]
mem_rem [in mathcomp.ssreflect.seq]
mem_subseq [in mathcomp.ssreflect.seq]
@@ -903,6 +908,7 @@ mem_rotr [in mathcomp.ssreflect.seq]
mem_rot [in mathcomp.ssreflect.seq]
mem_undup [in mathcomp.ssreflect.seq]
+mem_nseq [in mathcomp.ssreflect.seq]
mem_rev [in mathcomp.ssreflect.seq]
mem_filter [in mathcomp.ssreflect.seq]
mem_drop [in mathcomp.ssreflect.seq]
@@ -1167,6 +1173,8 @@ Monoid.Theory.mul0m [in mathcomp.ssreflect.bigop]
Monoid.Theory.mul1m [in mathcomp.ssreflect.bigop]
mono_leqif [in mathcomp.ssreflect.ssrnat]
+mono_inj [in mathcomp.ssreflect.eqtype]
+mono_inj_in [in mathcomp.ssreflect.eqtype]
morphicP [in mathcomp.fingroup.morphism]
morphic_aut [in mathcomp.fingroup.automorphism]
morphimD [in mathcomp.fingroup.morphism]
@@ -1426,6 +1434,7 @@ mulmx_sumr [in mathcomp.algebra.matrix]
mulmx_suml [in mathcomp.algebra.matrix]
mulmx_key [in mathcomp.algebra.matrix]
+mulmx_delta_companion [in mathcomp.algebra.mxpoly]
mulmx_ker [in mathcomp.algebra.mxalgebra]
mulmx_sub [in mathcomp.algebra.mxalgebra]
mulmx_coker [in mathcomp.algebra.mxalgebra]
@@ -1827,7 +1836,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1859,14 +1868,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1891,7 +1900,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1923,7 +1932,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1955,7 +1964,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1987,7 +1996,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -2019,7 +2028,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -2051,7 +2060,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -2083,14 +2092,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -2115,7 +2124,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -2147,7 +2156,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -2179,7 +2188,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -2211,14 +2220,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -2243,7 +2252,7 @@ Z _ other -(185 entries) +(189 entries) 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) diff --git a/docs/htmldoc/index_lemma_O.html b/docs/htmldoc/index_lemma_O.html index 30aee80..ca61880 100644 --- a/docs/htmldoc/index_lemma_O.html +++ b/docs/htmldoc/index_lemma_O.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)

O (lemma)

@@ -663,7 +663,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -695,14 +695,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -727,7 +727,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -759,7 +759,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -791,7 +791,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -823,7 +823,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -855,7 +855,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -887,7 +887,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -919,14 +919,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -951,7 +951,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -983,7 +983,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1015,7 +1015,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1047,14 +1047,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1079,7 +1079,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_P.html b/docs/htmldoc/index_lemma_P.html index 4907493..f9827ec 100644 --- a/docs/htmldoc/index_lemma_P.html +++ b/docs/htmldoc/index_lemma_P.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)

P (lemma)

@@ -994,11 +994,19 @@ PermDef.fun_of_permE [in mathcomp.fingroup.perm]
PermDef.permE [in mathcomp.fingroup.perm]
permE [in mathcomp.fingroup.perm]
+permEl [in mathcomp.ssreflect.seq]
permJ [in mathcomp.fingroup.perm]
permK [in mathcomp.fingroup.perm]
permKV [in mathcomp.fingroup.perm]
permM [in mathcomp.fingroup.perm]
permP [in mathcomp.fingroup.perm]
+permP [in mathcomp.ssreflect.seq]
+permPl [in mathcomp.ssreflect.seq]
+permPr [in mathcomp.ssreflect.seq]
+permutationsE [in mathcomp.ssreflect.seq]
+permutationsErot [in mathcomp.ssreflect.seq]
+permutations_all_uniq [in mathcomp.ssreflect.seq]
+permutations_uniq [in mathcomp.ssreflect.seq]
permX [in mathcomp.fingroup.perm]
perm_sortP [in mathcomp.ssreflect.path]
perm_sort [in mathcomp.ssreflect.path]
@@ -1023,40 +1031,49 @@ perm_inE [in mathcomp.fingroup.automorphism]
perm_in_on [in mathcomp.fingroup.automorphism]
perm_in_inj [in mathcomp.fingroup.automorphism]
-perm_undup_count [in mathcomp.ssreflect.seq]
-perm_eq_iotaP [in mathcomp.ssreflect.seq]
+perm_permutations [in mathcomp.ssreflect.seq]
+perm_count_undup [in mathcomp.ssreflect.seq]
+perm_tally_seq [in mathcomp.ssreflect.seq]
+perm_tally [in mathcomp.ssreflect.seq]
+perm_flatten [in mathcomp.ssreflect.seq]
+perm_sumn [in mathcomp.ssreflect.seq]
+perm_iotaP [in mathcomp.ssreflect.seq]
+perm_pmap [in mathcomp.ssreflect.seq]
+perm_map_inj [in mathcomp.ssreflect.seq]
perm_map [in mathcomp.ssreflect.seq]
perm_to_subseq [in mathcomp.ssreflect.seq]
perm_to_rem [in mathcomp.ssreflect.seq]
-perm_eq_uniq [in mathcomp.ssreflect.seq]
+perm_undup [in mathcomp.ssreflect.seq]
perm_uniq [in mathcomp.ssreflect.seq]
-perm_eq_small [in mathcomp.ssreflect.seq]
-perm_eq_size [in mathcomp.ssreflect.seq]
-perm_eq_all [in mathcomp.ssreflect.seq]
-perm_eq_mem [in mathcomp.ssreflect.seq]
+perm_small_eq [in mathcomp.ssreflect.seq]
+perm_all [in mathcomp.ssreflect.seq]
+perm_has [in mathcomp.ssreflect.seq]
+perm_consP [in mathcomp.ssreflect.seq]
+perm_nilP [in mathcomp.ssreflect.seq]
+perm_mem [in mathcomp.ssreflect.seq]
+perm_size [in mathcomp.ssreflect.seq]
perm_filterC [in mathcomp.ssreflect.seq]
perm_filter [in mathcomp.ssreflect.seq]
-perm_eq_rev [in mathcomp.ssreflect.seq]
+perm_rev [in mathcomp.ssreflect.seq]
perm_rotr [in mathcomp.ssreflect.seq]
perm_rot [in mathcomp.ssreflect.seq]
perm_rcons [in mathcomp.ssreflect.seq]
perm_catCA [in mathcomp.ssreflect.seq]
perm_catAC [in mathcomp.ssreflect.seq]
+perm_cat [in mathcomp.ssreflect.seq]
+perm_catr [in mathcomp.ssreflect.seq]
perm_cat2r [in mathcomp.ssreflect.seq]
perm_cons [in mathcomp.ssreflect.seq]
+perm_catl [in mathcomp.ssreflect.seq]
perm_cat2l [in mathcomp.ssreflect.seq]
perm_catC [in mathcomp.ssreflect.seq]
-perm_eqrP [in mathcomp.ssreflect.seq]
-perm_eqlP [in mathcomp.ssreflect.seq]
-perm_eqlE [in mathcomp.ssreflect.seq]
-perm_eq_trans [in mathcomp.ssreflect.seq]
-perm_eq_sym [in mathcomp.ssreflect.seq]
-perm_eq_refl [in mathcomp.ssreflect.seq]
-perm_eqP [in mathcomp.ssreflect.seq]
-perm_eq_abelian_type [in mathcomp.solvable.abelian]
+perm_trans [in mathcomp.ssreflect.seq]
+perm_sym [in mathcomp.ssreflect.seq]
+perm_refl [in mathcomp.ssreflect.seq]
perm_faithful [in mathcomp.fingroup.action]
perm_act1P [in mathcomp.fingroup.action]
perm_mact [in mathcomp.fingroup.action]
+perm_big [in mathcomp.ssreflect.bigop]
perm1 [in mathcomp.fingroup.perm]
pexpIrz [in mathcomp.algebra.ssrint]
pexprz_eq1 [in mathcomp.algebra.ssrint]
@@ -1169,6 +1186,7 @@ pmapS_filter [in mathcomp.ssreflect.seq]
pmap_sub_uniq [in mathcomp.ssreflect.seq]
pmap_uniq [in mathcomp.ssreflect.seq]
+pmap_cat [in mathcomp.ssreflect.seq]
pmap_filter [in mathcomp.ssreflect.seq]
pmaxElemJ [in mathcomp.solvable.abelian]
pmaxElemP [in mathcomp.solvable.abelian]
@@ -1358,6 +1376,9 @@ primeChar_scaleDr [in mathcomp.field.finfield]
primeChar_scale1 [in mathcomp.field.finfield]
primeChar_scaleA [in mathcomp.field.finfield]
+PrimeDecompAux.edivn2P [in mathcomp.ssreflect.prime]
+PrimeDecompAux.elogn2P [in mathcomp.ssreflect.prime]
+PrimeDecompAux.ifnzP [in mathcomp.ssreflect.prime]
primeP [in mathcomp.ssreflect.prime]
primePn [in mathcomp.ssreflect.prime]
primePns [in mathcomp.ssreflect.prime]
@@ -1583,7 +1604,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1615,14 +1636,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1647,7 +1668,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1679,7 +1700,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1711,7 +1732,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1743,7 +1764,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1775,7 +1796,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1807,7 +1828,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1839,14 +1860,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1871,7 +1892,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1903,7 +1924,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1935,7 +1956,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1967,14 +1988,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1999,7 +2020,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_Q.html b/docs/htmldoc/index_lemma_Q.html index 1b966ed..de28ad9 100644 --- a/docs/htmldoc/index_lemma_Q.html +++ b/docs/htmldoc/index_lemma_Q.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)

Q (lemma)

@@ -660,7 +660,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -692,14 +692,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -724,7 +724,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -756,7 +756,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -788,7 +788,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -820,7 +820,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -852,7 +852,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -884,7 +884,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -916,14 +916,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -948,7 +948,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -980,7 +980,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1012,7 +1012,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1044,14 +1044,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1076,7 +1076,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_R.html b/docs/htmldoc/index_lemma_R.html index 2022c3a..25a39fd 100644 --- a/docs/htmldoc/index_lemma_R.html +++ b/docs/htmldoc/index_lemma_R.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,11 +463,10 @@ Z _ other -(185 entries) +(189 entries)

R (lemma)

-rabstrX [in mathcomp.field.closed_field]
ractE [in mathcomp.fingroup.action]
ractpermE [in mathcomp.fingroup.action]
ract_is_groupAction [in mathcomp.fingroup.action]
@@ -476,7 +475,6 @@ raddfZ_Cint [in mathcomp.field.algC]
raddfZ_Cnat [in mathcomp.field.algC]
raddf_int_scalable [in mathcomp.algebra.ssrint]
-ramulXnT [in mathcomp.field.closed_field]
rankJ [in mathcomp.solvable.abelian]
rankS [in mathcomp.solvable.abelian]
rank_Wedderburn_subring [in mathcomp.character.mxrepresentation]
@@ -545,6 +543,9 @@ rcons_path [in mathcomp.ssreflect.path]
rcons_tupleP [in mathcomp.ssreflect.tuple]
rcons_uniq [in mathcomp.ssreflect.seq]
+rcons_injr [in mathcomp.ssreflect.seq]
+rcons_injl [in mathcomp.ssreflect.seq]
+rcons_inj [in mathcomp.ssreflect.seq]
rcons_cat [in mathcomp.ssreflect.seq]
rcons_cons [in mathcomp.ssreflect.seq]
rcosetE [in mathcomp.fingroup.fingroup]
@@ -574,12 +575,9 @@ rcoset_inj [in mathcomp.fingroup.fingroup]
rcoset1 [in mathcomp.fingroup.fingroup]
realz [in mathcomp.algebra.ssrint]
+real_lersif_normr [in mathcomp.algebra.interval]
+real_lersif_norml [in mathcomp.algebra.interval]
real_lersifN [in mathcomp.algebra.interval]
-redivpTP [in mathcomp.field.closed_field]
-redivpT_qf [in mathcomp.field.closed_field]
-redivp_rec_loopP [in mathcomp.field.closed_field]
-redivp_rec_loopT_qf [in mathcomp.field.closed_field]
-redivp_rec_loopTP [in mathcomp.field.closed_field]
reducible_Socle1 [in mathcomp.character.mxrepresentation]
reducible_Socle [in mathcomp.character.mxrepresentation]
refBaseField_key [in mathcomp.field.fieldext]
@@ -700,16 +698,6 @@ rfix_mxP [in mathcomp.character.mxrepresentation]
rfix_pgroup_char [in mathcomp.character.mxabelem]
rfix_abelem [in mathcomp.character.mxabelem]
-rgcdpTP [in mathcomp.field.closed_field]
-rgcdpTsP [in mathcomp.field.closed_field]
-rgcdpTs_qf [in mathcomp.field.closed_field]
-rgcdpT_qf [in mathcomp.field.closed_field]
-rgcdp_loopT_qf [in mathcomp.field.closed_field]
-rgcdp_loopP [in mathcomp.field.closed_field]
-rgdcopTP [in mathcomp.field.closed_field]
-rgdcopT_qf [in mathcomp.field.closed_field]
-rgdcop_recT_qf [in mathcomp.field.closed_field]
-rgdcop_recTP [in mathcomp.field.closed_field]
rgdP [in mathcomp.solvable.alt]
rgraphK [in mathcomp.ssreflect.fingraph]
right_arc [in mathcomp.ssreflect.path]
@@ -737,7 +725,6 @@ rmorph_unity_root [in mathcomp.algebra.poly]
rmorph_root [in mathcomp.algebra.poly]
rmorph_int [in mathcomp.algebra.ssrint]
-rmulpT [in mathcomp.field.closed_field]
rootC [in mathcomp.algebra.poly]
rootE [in mathcomp.algebra.poly]
rootM [in mathcomp.algebra.poly]
@@ -746,6 +733,7 @@ rootP [in mathcomp.ssreflect.fingraph]
rootPf [in mathcomp.algebra.poly]
rootPt [in mathcomp.algebra.poly]
+roots_geq_poly_eq0 [in mathcomp.algebra.poly]
roots_root [in mathcomp.ssreflect.fingraph]
rootX [in mathcomp.algebra.poly]
rootZ [in mathcomp.algebra.poly]
@@ -862,7 +850,6 @@ row'_const [in mathcomp.algebra.matrix]
row0 [in mathcomp.algebra.matrix]
row1 [in mathcomp.algebra.matrix]
-rpoly_map_mul [in mathcomp.field.closed_field]
rpredMz [in mathcomp.algebra.ssrint]
rpredXsign [in mathcomp.algebra.ssrint]
rpredXz [in mathcomp.algebra.ssrint]
@@ -880,7 +867,6 @@ rreg_size [in mathcomp.algebra.poly]
rreg_lead0 [in mathcomp.algebra.poly]
rreg_lead [in mathcomp.algebra.poly]
-rseq_poly_map [in mathcomp.field.closed_field]
rshift_subproof [in mathcomp.ssreflect.fintype]
rshift1 [in mathcomp.algebra.zmodp]
rsim_irr_comp [in mathcomp.character.mxrepresentation]
@@ -920,7 +906,6 @@ rstab_sub [in mathcomp.character.mxrepresentation]
rstab_abelem [in mathcomp.character.mxabelem]
rsubmx_key [in mathcomp.algebra.matrix]
-rsumpT [in mathcomp.field.closed_field]
rVabelemD [in mathcomp.character.mxabelem]
rVabelemJ [in mathcomp.character.mxabelem]
rVabelemK [in mathcomp.character.mxabelem]
@@ -993,7 +978,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1025,14 +1010,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1057,7 +1042,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1089,7 +1074,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1121,7 +1106,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1153,7 +1138,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1185,7 +1170,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1217,7 +1202,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1249,14 +1234,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1281,7 +1266,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1313,7 +1298,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1345,7 +1330,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1377,14 +1362,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1409,7 +1394,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_S.html b/docs/htmldoc/index_lemma_S.html index 72d70ad..1ef1855 100644 --- a/docs/htmldoc/index_lemma_S.html +++ b/docs/htmldoc/index_lemma_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 (lemma)

@@ -642,13 +642,13 @@ seqs1 [in mathcomp.solvable.burnside_app]
seqv_sub_adjoin [in mathcomp.field.falgebra]
seq_tnthP [in mathcomp.ssreflect.tuple]
+seq_ind2 [in mathcomp.ssreflect.seq]
seq_choiceMixin [in mathcomp.ssreflect.choice]
seq_of_optK [in mathcomp.ssreflect.choice]
seq_sub_axiom [in mathcomp.ssreflect.fintype]
seq_sub_pickleK [in mathcomp.ssreflect.fintype]
seq1_basis [in mathcomp.algebra.vector]
seq1_free [in mathcomp.algebra.vector]
-seq2_ind [in mathcomp.ssreflect.seq]
series_sol [in mathcomp.solvable.nilpotent]
setactE [in mathcomp.fingroup.action]
setactJ [in mathcomp.fingroup.action]
@@ -835,8 +835,7 @@ simple_compsP [in mathcomp.solvable.jordanholder]
simple_maxnormal [in mathcomp.solvable.gseries]
simple_sol_prime [in mathcomp.solvable.maximal]
-sizeTP [in mathcomp.field.closed_field]
-sizeT_qf [in mathcomp.field.closed_field]
+simpl_pred_sortE [in mathcomp.ssreflect.ssrbool]
sizeYE [in mathcomp.algebra.polyXY]
sizeY_mulX [in mathcomp.algebra.polyXY]
sizeY_eq0 [in mathcomp.algebra.polyXY]
@@ -857,7 +856,10 @@ size_poly_XaY [in mathcomp.algebra.polyXY]
size_Cyclotomic [in mathcomp.field.cyclotomic]
size_cyclotomic [in mathcomp.field.cyclotomic]
+size_permutations [in mathcomp.ssreflect.seq]
+size_tally_seq [in mathcomp.ssreflect.seq]
size_allpairs [in mathcomp.ssreflect.seq]
+size_allpairs_dep [in mathcomp.ssreflect.seq]
size_reshape [in mathcomp.ssreflect.seq]
size_flatten [in mathcomp.ssreflect.seq]
size_zip [in mathcomp.ssreflect.seq]
@@ -898,6 +900,10 @@ size_comp_poly2 [in mathcomp.algebra.poly]
size_comp_poly [in mathcomp.algebra.poly]
size_exp [in mathcomp.algebra.poly]
+size_prod_eq1 [in mathcomp.algebra.poly]
+size_prod_seq_eq1 [in mathcomp.algebra.poly]
+size_mul_eq1 [in mathcomp.algebra.poly]
+size_prod_seq [in mathcomp.algebra.poly]
size_prod [in mathcomp.algebra.poly]
size_Cmul [in mathcomp.algebra.poly]
size_scale [in mathcomp.algebra.poly]
@@ -929,6 +935,7 @@ size_addl [in mathcomp.algebra.poly]
size_add [in mathcomp.algebra.poly]
size_opp [in mathcomp.algebra.poly]
+size_polyC_leq1 [in mathcomp.algebra.poly]
size_poly1P [in mathcomp.algebra.poly]
size_poly_gt0 [in mathcomp.algebra.poly]
size_poly_leq0P [in mathcomp.algebra.poly]
@@ -975,9 +982,12 @@ sol_coprime_Sylow_exists [in mathcomp.solvable.hall]
sol_prime_factor_exists [in mathcomp.solvable.maximal]
sol_der1_proper [in mathcomp.solvable.nilpotent]
+Some_inj [in mathcomp.ssreflect.ssrfun]
sop_morph [in mathcomp.solvable.burnside_app]
sop_spec [in mathcomp.solvable.burnside_app]
sop_inj [in mathcomp.solvable.burnside_app]
+sorted_le_nth [in mathcomp.ssreflect.path]
+sorted_lt_nth [in mathcomp.ssreflect.path]
sorted_uniq [in mathcomp.ssreflect.path]
sorted_filter [in mathcomp.ssreflect.path]
sorted_divisors_ltn [in mathcomp.ssreflect.prime]
@@ -1143,6 +1153,8 @@ subn2 [in mathcomp.ssreflect.ssrnat]
SubP [in mathcomp.ssreflect.eqtype]
subq_ge0 [in mathcomp.algebra.rat]
+subr_lersif0r [in mathcomp.algebra.interval]
+subr_lersifr0 [in mathcomp.algebra.interval]
subseqP [in mathcomp.ssreflect.seq]
subseq_sorted [in mathcomp.ssreflect.path]
subseq_order_path [in mathcomp.ssreflect.path]
@@ -1151,8 +1163,8 @@ subseq_uniq [in mathcomp.ssreflect.seq]
subseq_rcons [in mathcomp.ssreflect.seq]
subseq_cons [in mathcomp.ssreflect.seq]
-subseq_refl [in mathcomp.ssreflect.seq]
subseq_trans [in mathcomp.ssreflect.seq]
+subseq_refl [in mathcomp.ssreflect.seq]
subseq0 [in mathcomp.ssreflect.seq]
subsetC [in mathcomp.ssreflect.finset]
subsetD [in mathcomp.ssreflect.finset]
@@ -1352,8 +1364,10 @@ summx_sub_sums [in mathcomp.algebra.mxalgebra]
summx_sub [in mathcomp.algebra.mxalgebra]
sumMz [in mathcomp.algebra.ssrint]
+sumnE [in mathcomp.ssreflect.bigop]
sumn_flatten [in mathcomp.ssreflect.seq]
sumn_rev [in mathcomp.ssreflect.seq]
+sumn_rot [in mathcomp.ssreflect.seq]
sumn_rcons [in mathcomp.ssreflect.seq]
sumn_count [in mathcomp.ssreflect.seq]
sumn_cat [in mathcomp.ssreflect.seq]
@@ -1389,7 +1403,7 @@ sum_eqP [in mathcomp.ssreflect.eqtype]
sum_totient_dvd [in mathcomp.solvable.cyclic]
sum_ncycle_totient [in mathcomp.solvable.cyclic]
-sum_nat_dep_const [in mathcomp.ssreflect.finset]
+sum_nat_cond_const [in mathcomp.ssreflect.finset]
sum1dep_card [in mathcomp.ssreflect.finset]
sum1_size [in mathcomp.ssreflect.bigop]
sum1_count [in mathcomp.ssreflect.bigop]
@@ -1481,7 +1495,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1513,14 +1527,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1545,7 +1559,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1577,7 +1591,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1609,7 +1623,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1641,7 +1655,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1673,7 +1687,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1705,7 +1719,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1737,14 +1751,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1769,7 +1783,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1801,7 +1815,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1833,7 +1847,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1865,14 +1879,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1897,7 +1911,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_T.html b/docs/htmldoc/index_lemma_T.html index 7f8e930..deb283e 100644 --- a/docs/htmldoc/index_lemma_T.html +++ b/docs/htmldoc/index_lemma_T.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,11 +463,12 @@ Z _ other -(185 entries) +(189 entries)

T (lemma)

tagged_choiceMixin [in mathcomp.ssreflect.choice]
+tagged_tfgraph [in mathcomp.ssreflect.finfun]
tagged_asE [in mathcomp.ssreflect.eqtype]
tag_of_pairK [in mathcomp.ssreflect.choice]
tag_enumP [in mathcomp.ssreflect.fintype]
@@ -475,6 +476,7 @@ tag_eqP [in mathcomp.ssreflect.eqtype]
takel_cat [in mathcomp.ssreflect.seq]
take_tupleP [in mathcomp.ssreflect.tuple]
+take_subseq [in mathcomp.ssreflect.seq]
take_rev [in mathcomp.ssreflect.seq]
take_nth [in mathcomp.ssreflect.seq]
take_size_cat [in mathcomp.ssreflect.seq]
@@ -483,12 +485,19 @@ take_size [in mathcomp.ssreflect.seq]
take_oversize [in mathcomp.ssreflect.seq]
take0 [in mathcomp.ssreflect.seq]
+tallyE [in mathcomp.ssreflect.seq]
+tallyEl [in mathcomp.ssreflect.seq]
+tallyK [in mathcomp.ssreflect.seq]
+tallyP [in mathcomp.ssreflect.seq]
+tally_seqK [in mathcomp.ssreflect.seq]
tcastE [in mathcomp.ssreflect.tuple]
tcastK [in mathcomp.ssreflect.tuple]
tcastKV [in mathcomp.ssreflect.tuple]
tcast_trans [in mathcomp.ssreflect.tuple]
tcast_id [in mathcomp.ssreflect.tuple]
textbook_triangular_sum [in mathcomp.ssreflect.binomial]
+tfgraphK [in mathcomp.ssreflect.finfun]
+tfgraph_inj [in mathcomp.ssreflect.finfun]
theadE [in mathcomp.ssreflect.tuple]
thinmx0 [in mathcomp.algebra.matrix]
third_isog [in mathcomp.fingroup.quotient]
@@ -523,6 +532,8 @@ tofrac_is_additive [in mathcomp.algebra.fraction]
tofrac0 [in mathcomp.algebra.fraction]
tofrac1 [in mathcomp.algebra.fraction]
+total_homo_mono [in mathcomp.ssreflect.eqtype]
+total_homo_mono_in [in mathcomp.ssreflect.eqtype]
totientE [in mathcomp.ssreflect.prime]
totient_count_coprime [in mathcomp.ssreflect.prime]
totient_coprime [in mathcomp.ssreflect.prime]
@@ -648,7 +659,7 @@ tr_row_perm [in mathcomp.algebra.matrix]
tupleE [in mathcomp.ssreflect.tuple]
tupleP [in mathcomp.ssreflect.tuple]
-tuple_perm_eqP [in mathcomp.fingroup.perm]
+tuple_permP [in mathcomp.fingroup.perm]
tuple_map_ord [in mathcomp.ssreflect.tuple]
tuple_eta [in mathcomp.ssreflect.tuple]
tuple0 [in mathcomp.ssreflect.tuple]
@@ -684,7 +695,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -716,14 +727,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -748,7 +759,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -780,7 +791,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -812,7 +823,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -844,7 +855,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -876,7 +887,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -908,7 +919,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -940,14 +951,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -972,7 +983,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1004,7 +1015,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -1036,7 +1047,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -1068,14 +1079,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1100,7 +1111,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_U.html b/docs/htmldoc/index_lemma_U.html index 383e56e..d2df217 100644 --- a/docs/htmldoc/index_lemma_U.html +++ b/docs/htmldoc/index_lemma_U.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)

U (lemma)

@@ -505,7 +505,8 @@ uniqPn [in mathcomp.ssreflect.seq]
uniq_normal_Hall [in mathcomp.solvable.pgroup]
uniq_traject_pcycle [in mathcomp.fingroup.perm]
-uniq_perm_eq [in mathcomp.ssreflect.seq]
+uniq_perm [in mathcomp.ssreflect.seq]
+uniq_min_size [in mathcomp.ssreflect.seq]
uniq_size_uniq [in mathcomp.ssreflect.seq]
uniq_leq_size [in mathcomp.ssreflect.seq]
uniq_catCA [in mathcomp.ssreflect.seq]
@@ -576,7 +577,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -608,14 +609,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -640,7 +641,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -672,7 +673,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -704,7 +705,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -736,7 +737,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -768,7 +769,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -800,7 +801,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -832,14 +833,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -864,7 +865,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -896,7 +897,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -928,7 +929,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -960,14 +961,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -992,7 +993,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_V.html b/docs/htmldoc/index_lemma_V.html index cb73143..cd60453 100644 --- a/docs/htmldoc/index_lemma_V.html +++ b/docs/htmldoc/index_lemma_V.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)

V (lemma)

@@ -588,7 +588,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -620,14 +620,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -652,7 +652,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -684,7 +684,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -716,7 +716,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -748,7 +748,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -780,7 +780,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -812,7 +812,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -844,14 +844,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -876,7 +876,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -908,7 +908,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -940,7 +940,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -972,14 +972,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -1004,7 +1004,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma_W.html b/docs/htmldoc/index_lemma_W.html index 569bf93..216a810 100644 --- a/docs/htmldoc/index_lemma_W.html +++ b/docs/htmldoc/index_lemma_W.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)

W (lemma)

@@ -483,7 +483,6 @@ Wedderburn_direct [in mathcomp.character.mxrepresentation]
Wedderburn_ideal [in mathcomp.character.mxrepresentation]
Wedderburn_id_expansion [in mathcomp.character.character]
-wf_ex_elim [in mathcomp.field.closed_field]
widen_partn [in mathcomp.ssreflect.prime]
widen_ord_proof [in mathcomp.ssreflect.fintype]
Wilson [in mathcomp.ssreflect.binomial]
diff --git a/docs/htmldoc/index_lemma_X.html b/docs/htmldoc/index_lemma_X.html index 5caf809..7140a67 100644 --- a/docs/htmldoc/index_lemma_X.html +++ b/docs/htmldoc/index_lemma_X.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)

X (lemma)

diff --git a/docs/htmldoc/index_lemma_Y.html b/docs/htmldoc/index_lemma_Y.html index c9bd28e..ecb788b 100644 --- a/docs/htmldoc/index_lemma_Y.html +++ b/docs/htmldoc/index_lemma_Y.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)
diff --git a/docs/htmldoc/index_lemma_Z.html b/docs/htmldoc/index_lemma_Z.html index 79874c2..497a1df 100644 --- a/docs/htmldoc/index_lemma_Z.html +++ b/docs/htmldoc/index_lemma_Z.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)

Z (lemma)

@@ -582,7 +582,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -614,14 +614,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -646,7 +646,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -678,7 +678,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -710,7 +710,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -742,7 +742,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -774,7 +774,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -806,7 +806,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -838,14 +838,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -870,7 +870,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -902,7 +902,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -934,7 +934,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -966,14 +966,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -998,7 +998,7 @@ Z _ other -(185 entries) +(189 entries) diff --git a/docs/htmldoc/index_lemma__.html b/docs/htmldoc/index_lemma__.html index c9bd28e..ecb788b 100644 --- a/docs/htmldoc/index_lemma__.html +++ b/docs/htmldoc/index_lemma__.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)
-- cgit v1.2.3