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_M.html | 192 ++++++++++++++++++++++++--------------- 1 file changed, 120 insertions(+), 72 deletions(-) (limited to 'docs/htmldoc/index_global_M.html') diff --git a/docs/htmldoc/index_global_M.html b/docs/htmldoc/index_global_M.html index bf4aaf2..18c6494 100644 --- a/docs/htmldoc/index_global_M.html +++ b/docs/htmldoc/index_global_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

@@ -496,7 +496,7 @@ MapComRing.f [variable, in mathcomp.algebra.mxpoly]
MapComRing.n' [variable, in mathcomp.algebra.mxpoly]
MapComRing.rR [variable, in mathcomp.algebra.mxpoly]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
MapEqPath [section, in mathcomp.ssreflect.path]
MapEqPath.e [variable, in mathcomp.ssreflect.path]
MapEqPath.e' [variable, in mathcomp.ssreflect.path]
@@ -509,25 +509,26 @@ MapFieldMatrix.aF [variable, in mathcomp.algebra.matrix]
MapFieldMatrix.f [variable, in mathcomp.algebra.matrix]
MapFieldMatrix.rF [variable, in mathcomp.algebra.matrix]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
MapFieldPoly [section, in mathcomp.algebra.poly]
MapFieldPoly.f [variable, in mathcomp.algebra.poly]
MapFieldPoly.F [variable, in mathcomp.algebra.poly]
MapFieldPoly.R [variable, in mathcomp.algebra.poly]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
MapField.A [variable, in mathcomp.algebra.mxpoly]
MapField.aF [variable, in mathcomp.algebra.mxpoly]
MapField.f [variable, in mathcomp.algebra.mxpoly]
MapField.n' [variable, in mathcomp.algebra.mxpoly]
+MapField.p [variable, in mathcomp.algebra.mxpoly]
MapField.rF [variable, in mathcomp.algebra.mxpoly]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
mapK [lemma, in mathcomp.ssreflect.seq]
MapMatrix [section, in mathcomp.algebra.matrix]
MapMatrixSpaces [section, in mathcomp.algebra.mxalgebra]
MapMatrixSpaces.aF [variable, in mathcomp.algebra.mxalgebra]
MapMatrixSpaces.f [variable, in mathcomp.algebra.mxalgebra]
MapMatrixSpaces.rF [variable, in mathcomp.algebra.mxalgebra]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.mxalgebra]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.mxalgebra]
MapMatrix.aT [variable, in mathcomp.algebra.matrix]
MapMatrix.Block [section, in mathcomp.algebra.matrix]
MapMatrix.Block.Adl [variable, in mathcomp.algebra.matrix]
@@ -547,7 +548,7 @@ MapMatrix.OneMatrix.m [variable, in mathcomp.algebra.matrix]
MapMatrix.OneMatrix.n [variable, in mathcomp.algebra.matrix]
MapMatrix.rT [variable, in mathcomp.algebra.matrix]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
MapMinPoly [section, in mathcomp.field.fieldext]
MapMinPoly.f [variable, in mathcomp.field.fieldext]
MapMinPoly.F0 [variable, in mathcomp.field.fieldext]
@@ -570,14 +571,14 @@ MapPoly.Additive [section, in mathcomp.algebra.poly]
MapPoly.Additive.f [variable, in mathcomp.algebra.poly]
MapPoly.Additive.iR [variable, in mathcomp.algebra.poly]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
MapPoly.aR [variable, in mathcomp.algebra.poly]
MapPoly.Combinatorial [section, in mathcomp.algebra.poly]
MapPoly.Combinatorial.f [variable, in mathcomp.algebra.poly]
MapPoly.Combinatorial.f_0 [variable, in mathcomp.algebra.poly]
MapPoly.Combinatorial.inj_f [variable, in mathcomp.algebra.poly]
MapPoly.Combinatorial.iR [variable, in mathcomp.algebra.poly]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
MapPoly.Definitions [section, in mathcomp.algebra.poly]
MapPoly.Definitions.aR [variable, in mathcomp.algebra.poly]
MapPoly.Definitions.f [variable, in mathcomp.algebra.poly]
@@ -587,7 +588,7 @@ MapPoly.HornerMorph.cfu [variable, in mathcomp.algebra.poly]
MapPoly.HornerMorph.u [variable, in mathcomp.algebra.poly]
MapPoly.rR [variable, in mathcomp.algebra.poly]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
MapResultant [section, in mathcomp.algebra.mxpoly]
MapRingMatrix [section, in mathcomp.algebra.matrix]
MapRingMatrix [section, in mathcomp.algebra.mxpoly]
@@ -604,15 +605,15 @@ MapRingMatrix.n [variable, in mathcomp.algebra.mxpoly]
MapRingMatrix.rR [variable, in mathcomp.algebra.matrix]
MapRingMatrix.rR [variable, in mathcomp.algebra.mxpoly]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
MapZmodMatrix [section, in mathcomp.algebra.matrix]
MapZmodMatrix.aR [variable, in mathcomp.algebra.matrix]
MapZmodMatrix.f [variable, in mathcomp.algebra.matrix]
MapZmodMatrix.m [variable, in mathcomp.algebra.matrix]
MapZmodMatrix.n [variable, in mathcomp.algebra.matrix]
MapZmodMatrix.rR [variable, in mathcomp.algebra.matrix]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
map_path [lemma, in mathcomp.ssreflect.path]
map_orthonormal [lemma, in mathcomp.character.vcharacter]
map_pairwise_orthogonal [lemma, in mathcomp.character.vcharacter]
@@ -691,6 +692,7 @@ map_mx [definition, in mathcomp.algebra.matrix]
map_mx_key [lemma, in mathcomp.algebra.matrix]
map_mx_inv_horner [lemma, in mathcomp.algebra.mxpoly]
+map_mx_companion [lemma, in mathcomp.algebra.mxpoly]
map_horner_mx [lemma, in mathcomp.algebra.mxpoly]
map_powers_mx [lemma, in mathcomp.algebra.mxpoly]
map_resultant [lemma, in mathcomp.algebra.mxpoly]
@@ -701,6 +703,7 @@ map_div_annihilantP [lemma, in mathcomp.algebra.polyXY]
map_sub_annihilantP [lemma, in mathcomp.algebra.polyXY]
map_Qnum_poly [lemma, in mathcomp.field.algnum]
+map_allpairs [lemma, in mathcomp.ssreflect.seq]
map_reshape [lemma, in mathcomp.ssreflect.seq]
map_flatten [lemma, in mathcomp.ssreflect.seq]
map_pK [lemma, in mathcomp.ssreflect.seq]
@@ -824,21 +827,21 @@ MatrixAlgebra.RingModule [section, in mathcomp.algebra.matrix]
MatrixAlgebra.RingModule.m [variable, in mathcomp.algebra.matrix]
MatrixAlgebra.RingModule.n [variable, in mathcomp.algebra.matrix]
-_ *m: _ (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ *m: _ (ring_scope) [notation, in mathcomp.algebra.matrix]
MatrixAlgebra.ScalarMx [section, in mathcomp.algebra.matrix]
MatrixAlgebra.ScalarMx.n [variable, in mathcomp.algebra.matrix]
-_ %:M (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ %:M (ring_scope) [notation, in mathcomp.algebra.matrix]
MatrixAlgebra.StructuralLinear [section, in mathcomp.algebra.matrix]
MatrixAlgebra.Trace [section, in mathcomp.algebra.matrix]
MatrixAlgebra.Trace.n [variable, in mathcomp.algebra.matrix]
-\tr _ (ring_scope) [notation, in mathcomp.algebra.matrix]
-'Z ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
-'C ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
-_ * _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
-\tr _ (ring_scope) [notation, in mathcomp.algebra.matrix]
-_ *m _ (ring_scope) [notation, in mathcomp.algebra.matrix]
-_ %:M (ring_scope) [notation, in mathcomp.algebra.matrix]
-_ \in _ [notation, in mathcomp.algebra.mxalgebra]
+\tr _ (ring_scope) [notation, in mathcomp.algebra.matrix]
+'Z ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
+'C ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
+_ * _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
+\tr _ (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ *m _ (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ %:M (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ \in _ [notation, in mathcomp.algebra.mxalgebra]
MatrixDef [section, in mathcomp.algebra.matrix]
MatrixDef.m [variable, in mathcomp.algebra.matrix]
MatrixDef.n [variable, in mathcomp.algebra.matrix]
@@ -938,9 +941,9 @@ MatrixGenField.GenField [section, in mathcomp.character.mxrepresentation]
MatrixGenField.GenField.A [variable, in mathcomp.character.mxrepresentation]
MatrixGenField.GenField.Bijection [section, in mathcomp.character.mxrepresentation]
-MatrixGenField.GenField.Bijection.m1 [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.Bijection.m [variable, in mathcomp.character.mxrepresentation]
MatrixGenField.GenField.Bijection2 [section, in mathcomp.character.mxrepresentation]
-MatrixGenField.GenField.Bijection2.m1 [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.Bijection2.m [variable, in mathcomp.character.mxrepresentation]
MatrixGenField.GenField.cGA [variable, in mathcomp.character.mxrepresentation]
MatrixGenField.GenField.d_gt0 [variable, in mathcomp.character.mxrepresentation]
MatrixGenField.GenField.F [variable, in mathcomp.character.mxrepresentation]
@@ -1007,7 +1010,6 @@ MatrixGenField.in_genK [lemma, in mathcomp.character.mxrepresentation]
MatrixGenField.in_gen [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.irr [abbreviation, in mathcomp.character.mxrepresentation]
-MatrixGenField.m [abbreviation, in mathcomp.character.mxrepresentation]
MatrixGenField.map_mxminpoly_groot [lemma, in mathcomp.character.mxrepresentation]
MatrixGenField.morphAnd [abbreviation, in mathcomp.character.mxrepresentation]
MatrixGenField.mxmodule_rowval_gen [lemma, in mathcomp.character.mxrepresentation]
@@ -1031,6 +1033,7 @@ MatrixGenField.n [abbreviation, in mathcomp.character.mxrepresentation]
MatrixGenField.n [abbreviation, in mathcomp.character.mxrepresentation]
MatrixGenField.n [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.nA [abbreviation, in mathcomp.character.mxrepresentation]
MatrixGenField.non_linear_gen_reducible [lemma, in mathcomp.character.mxrepresentation]
MatrixGenField.nth_map_rVval [lemma, in mathcomp.character.mxrepresentation]
MatrixGenField.pA [abbreviation, in mathcomp.character.mxrepresentation]
@@ -1114,7 +1117,7 @@ MatrixStructural.VecMatrix [section, in mathcomp.algebra.matrix]
MatrixStructural.VecMatrix.m [variable, in mathcomp.algebra.matrix]
MatrixStructural.VecMatrix.n [variable, in mathcomp.algebra.matrix]
-_ ^T (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ ^T (ring_scope) [notation, in mathcomp.algebra.matrix]
MatrixVectType [section, in mathcomp.algebra.vector]
MatrixVectType.m [variable, in mathcomp.algebra.vector]
MatrixVectType.n [variable, in mathcomp.algebra.vector]
@@ -1324,11 +1327,14 @@ mem_Cint_span [lemma, in mathcomp.field.algnum]
mem_Crat_span [lemma, in mathcomp.field.algnum]
mem_irr [lemma, in mathcomp.character.character]
+mem_permutations [lemma, in mathcomp.ssreflect.seq]
mem_allpairs [lemma, in mathcomp.ssreflect.seq]
+mem_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
mem_iota [lemma, in mathcomp.ssreflect.seq]
mem_pmap_sub [lemma, in mathcomp.ssreflect.seq]
mem_pmap [lemma, in mathcomp.ssreflect.seq]
mem_map [lemma, in mathcomp.ssreflect.seq]
+mem_rem_uniqF [lemma, in mathcomp.ssreflect.seq]
mem_rem_uniq [lemma, in mathcomp.ssreflect.seq]
mem_rem [lemma, in mathcomp.ssreflect.seq]
mem_subseq [lemma, in mathcomp.ssreflect.seq]
@@ -1338,6 +1344,7 @@ mem_rotr [lemma, in mathcomp.ssreflect.seq]
mem_rot [lemma, in mathcomp.ssreflect.seq]
mem_undup [lemma, in mathcomp.ssreflect.seq]
+mem_nseq [lemma, in mathcomp.ssreflect.seq]
mem_rev [lemma, in mathcomp.ssreflect.seq]
mem_filter [lemma, in mathcomp.ssreflect.seq]
mem_drop [lemma, in mathcomp.ssreflect.seq]
@@ -1665,19 +1672,42 @@ monic_neq0 [lemma, in mathcomp.algebra.poly]
monic_key [lemma, in mathcomp.algebra.poly]
monic1 [lemma, in mathcomp.algebra.poly]
+MonoHomoTheory [section, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.aR [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.aRE [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.aR_anti [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.aR_refl [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.aR' [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.aR'E [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.aT [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.D [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.f [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.InDom [section, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.InDom.aR_anti [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.InDom.D [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.InDom.DifferentDom [section, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.InDom.DifferentDom.D' [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.InDom.rR_anti [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.rR [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.rRE [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.rR_anti [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.rR_refl [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.rR' [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.rR'E [variable, in mathcomp.ssreflect.eqtype]
+MonoHomoTheory.rT [variable, in mathcomp.ssreflect.eqtype]
Monoid [module, in mathcomp.ssreflect.bigop]
MonoidProperties [section, in mathcomp.ssreflect.bigop]
MonoidProperties.Abelian [section, in mathcomp.ssreflect.bigop]
MonoidProperties.Abelian.op [variable, in mathcomp.ssreflect.bigop]
-_ * _ [notation, in mathcomp.ssreflect.bigop]
-*%M [notation, in mathcomp.ssreflect.bigop]
+_ * _ [notation, in mathcomp.ssreflect.bigop]
+*%M [notation, in mathcomp.ssreflect.bigop]
MonoidProperties.idx [variable, in mathcomp.ssreflect.bigop]
MonoidProperties.Plain [section, in mathcomp.ssreflect.bigop]
MonoidProperties.Plain.op [variable, in mathcomp.ssreflect.bigop]
-_ * _ [notation, in mathcomp.ssreflect.bigop]
-*%M [notation, in mathcomp.ssreflect.bigop]
+_ * _ [notation, in mathcomp.ssreflect.bigop]
+*%M [notation, in mathcomp.ssreflect.bigop]
MonoidProperties.R [variable, in mathcomp.ssreflect.bigop]
-1 [notation, in mathcomp.ssreflect.bigop]
+1 [notation, in mathcomp.ssreflect.bigop]
Monoid.AddLaw [constructor, in mathcomp.ssreflect.bigop]
Monoid.add_operator [projection, in mathcomp.ssreflect.bigop]
Monoid.add_law [record, in mathcomp.ssreflect.bigop]
@@ -1701,10 +1731,10 @@ Monoid.Definitions.op_id [variable, in mathcomp.ssreflect.bigop]
Monoid.Definitions.T [variable, in mathcomp.ssreflect.bigop]
Monoid.Exports [module, in mathcomp.ssreflect.bigop]
-[ add_law _ of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
-[ mul_law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
-[ com_law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
-[ law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
+[ add_law _ of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
+[ mul_law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
+[ com_law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
+[ law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
Monoid.law [record, in mathcomp.ssreflect.bigop]
Monoid.Law [constructor, in mathcomp.ssreflect.bigop]
Monoid.mulC_dist [lemma, in mathcomp.ssreflect.bigop]
@@ -1752,7 +1782,25 @@ MonotonicFunctorTheory.Composition.F2 [variable, in mathcomp.solvable.gfunctor]
MonotonicFunctorTheory.F1 [variable, in mathcomp.solvable.gfunctor]
MonotonicFunctorTheory.F2 [variable, in mathcomp.solvable.gfunctor]
+Monotonicity [section, in mathcomp.ssreflect.path]
+Monotonicity [section, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat [section, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat.anti_geq [variable, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat.anti_leq [variable, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat.D [variable, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat.D' [variable, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat.f [variable, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat.gtn_neqAge [variable, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat.leq_total [variable, in mathcomp.ssreflect.ssrnat]
+Monotonicity.NatToNat.ltn_neqAle [variable, in mathcomp.ssreflect.ssrnat]
+Monotonicity.r [variable, in mathcomp.ssreflect.path]
+Monotonicity.r_refl [variable, in mathcomp.ssreflect.path]
+Monotonicity.r_trans [variable, in mathcomp.ssreflect.path]
+Monotonicity.T [variable, in mathcomp.ssreflect.path]
+Monotonicity.T [variable, in mathcomp.ssreflect.ssrnat]
mono_leqif [lemma, in mathcomp.ssreflect.ssrnat]
+mono_inj [lemma, in mathcomp.ssreflect.eqtype]
+mono_inj_in [lemma, in mathcomp.ssreflect.eqtype]
MoreAlgCaut [section, in mathcomp.field.algnum]
MoreConstt [section, in mathcomp.character.character]
MoreConstt.G [variable, in mathcomp.character.character]
@@ -2185,7 +2233,7 @@ MorphTheory.Frobenius.charFp [variable, in mathcomp.algebra.ssrint]
MorphTheory.Frobenius.p [variable, in mathcomp.algebra.ssrint]
MorphTheory.Frobenius.R [variable, in mathcomp.algebra.ssrint]
-_ ^f [notation, in mathcomp.algebra.ssrint]
+_ ^f [notation, in mathcomp.algebra.ssrint]
MorphTheory.Linear [section, in mathcomp.algebra.ssrint]
MorphTheory.Linear.f [variable, in mathcomp.algebra.ssrint]
MorphTheory.Linear.R [variable, in mathcomp.algebra.ssrint]
@@ -2297,6 +2345,7 @@ mulmx_sumr [lemma, in mathcomp.algebra.matrix]
mulmx_suml [lemma, in mathcomp.algebra.matrix]
mulmx_key [lemma, in mathcomp.algebra.matrix]
+mulmx_delta_companion [lemma, in mathcomp.algebra.mxpoly]
mulmx_ker [lemma, in mathcomp.algebra.mxalgebra]
mulmx_sub [lemma, in mathcomp.algebra.mxalgebra]
mulmx_coker [lemma, in mathcomp.algebra.mxalgebra]
@@ -2350,7 +2399,6 @@ muln0 [lemma, in mathcomp.ssreflect.ssrnat]
muln1 [lemma, in mathcomp.ssreflect.ssrnat]
muln2 [lemma, in mathcomp.ssreflect.ssrnat]
-mulpT [definition, in mathcomp.field.closed_field]
mulpz [lemma, in mathcomp.algebra.ssrint]
mulq [definition, in mathcomp.algebra.rat]
mulqA [lemma, in mathcomp.algebra.rat]
@@ -2761,7 +2809,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -2793,14 +2841,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -2825,7 +2873,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -2857,7 +2905,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -2889,7 +2937,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -2921,7 +2969,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -2953,7 +3001,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -2985,7 +3033,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -3017,14 +3065,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -3049,7 +3097,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -3081,7 +3129,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -3113,7 +3161,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -3145,14 +3193,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -3177,7 +3225,7 @@ Z _ other -(185 entries) +(189 entries) -- cgit v1.2.3