From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/index_global_I.html | 149 +++++++++++++++++++-------------------- 1 file changed, 74 insertions(+), 75 deletions(-) (limited to 'docs/htmldoc/index_global_I.html') diff --git a/docs/htmldoc/index_global_I.html b/docs/htmldoc/index_global_I.html index 8f948c3..95663cd 100644 --- a/docs/htmldoc/index_global_I.html +++ b/docs/htmldoc/index_global_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

@@ -506,11 +506,6 @@ ieexprIz [lemma, in mathcomp.algebra.ssrint]
ifactm [definition, in mathcomp.fingroup.morphism]
ifactmE [lemma, in mathcomp.fingroup.morphism]
-ifnz [definition, in mathcomp.ssreflect.prime]
-ifnzP [lemma, in mathcomp.ssreflect.prime]
-IfnzPos [constructor, in mathcomp.ssreflect.prime]
-IfnzZero [constructor, in mathcomp.ssreflect.prime]
-ifnz_spec [inductive, in mathcomp.ssreflect.prime]
ifN_eqC [lemma, in mathcomp.ssreflect.eqtype]
ifN_eq [lemma, in mathcomp.ssreflect.eqtype]
iG [abbreviation, in mathcomp.character.mxrepresentation]
@@ -632,6 +627,10 @@ im_Zpm [lemma, in mathcomp.solvable.cyclic]
im_transversal_repr [lemma, in mathcomp.ssreflect.finset]
inA [abbreviation, in mathcomp.solvable.hall]
+incrn_inj_in [lemma, in mathcomp.ssreflect.ssrnat]
+incrn_inj [lemma, in mathcomp.ssreflect.ssrnat]
+incr_tallyP [lemma, in mathcomp.ssreflect.seq]
+incr_tally [definition, in mathcomp.ssreflect.seq]
incr_nthC [lemma, in mathcomp.ssreflect.seq]
incr_nth_inj [lemma, in mathcomp.ssreflect.seq]
incr_nth [definition, in mathcomp.ssreflect.seq]
@@ -686,11 +685,12 @@ Induced.H [variable, in mathcomp.character.character]
Induced.H [variable, in mathcomp.character.classfun]
Induced.K [variable, in mathcomp.character.classfun]
-'Ind[ _ ] (ring_scope) [notation, in mathcomp.character.classfun]
-'Ind[ _ , _ ] (ring_scope) [notation, in mathcomp.character.classfun]
+'Ind[ _ ] (ring_scope) [notation, in mathcomp.character.classfun]
+'Ind[ _ , _ ] (ring_scope) [notation, in mathcomp.character.classfun]
Ind_Iirr [definition, in mathcomp.character.character]
Ind_irr_neq0 [lemma, in mathcomp.character.character]
inE [definition, in mathcomp.ssreflect.seq]
+inE [definition, in mathcomp.ssreflect.ssrbool]
inE [definition, in mathcomp.ssreflect.finset]
inertia [definition, in mathcomp.character.inertia]
Inertia [section, in mathcomp.character.inertia]
@@ -752,11 +752,11 @@ Inertia.G [variable, in mathcomp.character.inertia]
Inertia.gT [variable, in mathcomp.character.inertia]
Inertia.H [variable, in mathcomp.character.inertia]
-_ ^: _ (cfun_scope) [notation, in mathcomp.character.inertia]
-'I_ _ [ _ ] (Group_scope) [notation, in mathcomp.character.inertia]
-'I[ _ ] (Group_scope) [notation, in mathcomp.character.inertia]
-'I_ _ [ _ ] (group_scope) [notation, in mathcomp.character.inertia]
-'I[ _ ] (group_scope) [notation, in mathcomp.character.inertia]
+_ ^: _ (cfun_scope) [notation, in mathcomp.character.inertia]
+'I_ _ [ _ ] (Group_scope) [notation, in mathcomp.character.inertia]
+'I[ _ ] (Group_scope) [notation, in mathcomp.character.inertia]
+'I_ _ [ _ ] (group_scope) [notation, in mathcomp.character.inertia]
+'I[ _ ] (group_scope) [notation, in mathcomp.character.inertia]
inertia0 [lemma, in mathcomp.character.inertia]
Inertia1 [lemma, in mathcomp.character.inertia]
inertia1 [lemma, in mathcomp.character.inertia]
@@ -772,9 +772,11 @@ InfinitePrimitiveElementTheorem.px_0 [variable, in mathcomp.field.separable]
InfinitePrimitiveElementTheorem.x [variable, in mathcomp.field.separable]
InfinitePrimitiveElementTheorem.y [variable, in mathcomp.field.separable]
-_ ^ _ (ring_scope) [notation, in mathcomp.field.separable]
+_ ^ _ (ring_scope) [notation, in mathcomp.field.separable]
inG [abbreviation, in mathcomp.solvable.hall]
inH [abbreviation, in mathcomp.fingroup.action]
+InheritedStructures [section, in mathcomp.ssreflect.finfun]
+InheritedStructures.aT [variable, in mathcomp.ssreflect.finfun]
inIntSpan [definition, in mathcomp.algebra.intdiv]
injectiveb [definition, in mathcomp.ssreflect.fintype]
Injectiveb [section, in mathcomp.ssreflect.fintype]
@@ -952,6 +954,8 @@ inj_map [lemma, in mathcomp.ssreflect.seq]
inj_card_bij [lemma, in mathcomp.ssreflect.fintype]
inj_card_onto [lemma, in mathcomp.ssreflect.fintype]
+inj_homo [lemma, in mathcomp.ssreflect.eqtype]
+inj_homo_in [lemma, in mathcomp.ssreflect.eqtype]
inj_eqAxiom [lemma, in mathcomp.ssreflect.eqtype]
inj_in_eq [lemma, in mathcomp.ssreflect.eqtype]
inj_eq [lemma, in mathcomp.ssreflect.eqtype]
@@ -1011,8 +1015,8 @@ IntDist.leqif_add_distz [lemma, in mathcomp.algebra.ssrint]
IntDist.leq_add_dist [lemma, in mathcomp.algebra.ssrint]
IntDist.sqrn_dist [lemma, in mathcomp.algebra.ssrint]
-_ - _ (distn_scope) [notation, in mathcomp.algebra.ssrint]
-`| _ | (nat_scope) [notation, in mathcomp.algebra.ssrint]
+_ - _ (distn_scope) [notation, in mathcomp.algebra.ssrint]
+`| _ | (nat_scope) [notation, in mathcomp.algebra.ssrint]
intdiv [library]
IntegralChar [section, in mathcomp.character.integral_char]
IntegralChar.G [variable, in mathcomp.character.integral_char]
@@ -1080,22 +1084,14 @@ Interval [constructor, in mathcomp.algebra.interval]
interval [inductive, in mathcomp.algebra.interval]
interval [library]
+IntervalEq [section, in mathcomp.algebra.interval]
+IntervalEq.T [variable, in mathcomp.algebra.interval]
IntervalField [section, in mathcomp.algebra.interval]
IntervalField.R [variable, in mathcomp.algebra.interval]
IntervalOrdered [section, in mathcomp.algebra.interval]
IntervalOrdered.R [variable, in mathcomp.algebra.interval]
IntervalPo [section, in mathcomp.algebra.interval]
IntervalPo.R [variable, in mathcomp.algebra.interval]
-_ <= _ ?< if _ (ring_scope) [notation, in mathcomp.algebra.interval]
-`] -oo , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]
-`] _ , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]
-`[ _ , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]
-`] -oo , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]
-`] -oo , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]
-`] _ , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]
-`[ _ , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]
-`] _ , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]
-`[ _ , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]
intEsg [lemma, in mathcomp.algebra.ssrint]
intEsign [lemma, in mathcomp.algebra.ssrint]
intmul [definition, in mathcomp.algebra.ssrint]
@@ -1124,9 +1120,9 @@ intRingTheory [section, in mathcomp.algebra.ssrint]
intRing.comMixin [definition, in mathcomp.algebra.ssrint]
intRing.intRing [section, in mathcomp.algebra.ssrint]
-_ * _ (int_scope) [notation, in mathcomp.algebra.ssrint]
-*%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
-1 (int_scope) [notation, in mathcomp.algebra.ssrint]
+_ * _ (int_scope) [notation, in mathcomp.algebra.ssrint]
+*%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
+1 (int_scope) [notation, in mathcomp.algebra.ssrint]
intRing.mulNz [lemma, in mathcomp.algebra.ssrint]
intRing.mulz [definition, in mathcomp.algebra.ssrint]
intRing.mulzA [lemma, in mathcomp.algebra.ssrint]
@@ -1179,12 +1175,12 @@ intZmod.add1Pz [lemma, in mathcomp.algebra.ssrint]
intZmod.intP [lemma, in mathcomp.algebra.ssrint]
intZmod.intZmod [section, in mathcomp.algebra.ssrint]
-_ - _ (int_scope) [notation, in mathcomp.algebra.ssrint]
-_ + _ (int_scope) [notation, in mathcomp.algebra.ssrint]
-+%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
-- _ (int_scope) [notation, in mathcomp.algebra.ssrint]
--%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
-0 (int_scope) [notation, in mathcomp.algebra.ssrint]
+_ - _ (int_scope) [notation, in mathcomp.algebra.ssrint]
+_ + _ (int_scope) [notation, in mathcomp.algebra.ssrint]
++%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
+- _ (int_scope) [notation, in mathcomp.algebra.ssrint]
+-%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
+0 (int_scope) [notation, in mathcomp.algebra.ssrint]
intZmod.int_spec [inductive, in mathcomp.algebra.ssrint]
intZmod.int_ind [definition, in mathcomp.algebra.ssrint]
intZmod.int_rec [definition, in mathcomp.algebra.ssrint]
@@ -1338,9 +1334,9 @@ IrrClass.gT [variable, in mathcomp.character.character]
IrrClass.R_G [variable, in mathcomp.character.character]
IrrClass.sG [variable, in mathcomp.character.character]
-'e_ _ [notation, in mathcomp.character.character]
-'n_ _ [notation, in mathcomp.character.character]
-'R_ _ [notation, in mathcomp.character.character]
+'e_ _ [notation, in mathcomp.character.character]
+'n_ _ [notation, in mathcomp.character.character]
+'R_ _ [notation, in mathcomp.character.character]
IrrConstt [section, in mathcomp.character.character]
IrrConstt.G [variable, in mathcomp.character.character]
IrrConstt.gT [variable, in mathcomp.character.character]
@@ -1423,9 +1419,6 @@ IsChar.gT [variable, in mathcomp.character.character]
isgroupP [lemma, in mathcomp.fingroup.fingroup]
IsMxvecIndex [constructor, in mathcomp.algebra.matrix]
-isnull [definition, in mathcomp.field.closed_field]
-isnullP [lemma, in mathcomp.field.closed_field]
-isnull_qf [lemma, in mathcomp.field.closed_field]
isob [abbreviation, in mathcomp.solvable.center]
IsoBoolEquiv [section, in mathcomp.fingroup.morphism]
IsoBoolEquiv.G [variable, in mathcomp.fingroup.morphism]
@@ -1637,9 +1630,15 @@ iter_in [lemma, in mathcomp.ssreflect.fingraph]
iter_findex [lemma, in mathcomp.ssreflect.fingraph]
itvP [lemma, in mathcomp.algebra.interval]
+itv_intersectionA [lemma, in mathcomp.algebra.interval]
+itv_intersectionC [lemma, in mathcomp.algebra.interval]
itv_splitU2 [lemma, in mathcomp.algebra.interval]
itv_splitU [lemma, in mathcomp.algebra.interval]
itv_splitI [lemma, in mathcomp.algebra.interval]
+itv_intersectionii [lemma, in mathcomp.algebra.interval]
+itv_intersectioni1 [definition, in mathcomp.algebra.interval]
+itv_intersection1i [definition, in mathcomp.algebra.interval]
+itv_intersection [definition, in mathcomp.algebra.interval]
itv_gte [lemma, in mathcomp.algebra.interval]
itv_xx [lemma, in mathcomp.algebra.interval]
itv_boundlr [lemma, in mathcomp.algebra.interval]
@@ -1678,7 +1677,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -1710,14 +1709,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -1742,7 +1741,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -1774,7 +1773,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -1806,7 +1805,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -1838,7 +1837,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -1870,7 +1869,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -1902,7 +1901,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -1934,14 +1933,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -1966,7 +1965,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -1998,7 +1997,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -2030,7 +2029,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -2062,14 +2061,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -2094,7 +2093,7 @@ Z _ other -(185 entries) +(189 entries) -- cgit v1.2.3