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_C.html | 140 +++++++++++++++++++++++++++++----------- 1 file changed, 102 insertions(+), 38 deletions(-) (limited to 'docs/htmldoc/index_lemma_C.html') 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) -- cgit v1.2.3