From ed05182cece6bb3706e09b2ce14af4a41a2e8141 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Apr 2018 10:54:22 +0200 Subject: generate the documentation for 1.7 --- docs/htmldoc/index_global_V.html | 1158 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 1158 insertions(+) create mode 100644 docs/htmldoc/index_global_V.html (limited to 'docs/htmldoc/index_global_V.html') diff --git a/docs/htmldoc/index_global_V.html b/docs/htmldoc/index_global_V.html new file mode 100644 index 0000000..faca1fb --- /dev/null +++ b/docs/htmldoc/index_global_V.html @@ -0,0 +1,1158 @@ + + + + + +mathcomp.ssreflect.tuple + + + + +
+ + + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(23233 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1373 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(213 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3475 entries)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(89 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(11853 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(359 entries)
Axiom IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(47 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(103 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(266 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1118 entries)
Abbreviation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(691 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3461 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(185 entries)
+

V

+val [projection, in mathcomp.ssreflect.eqtype]
+valG [lemma, in mathcomp.fingroup.fingroup]
+valgM [lemma, in mathcomp.fingroup.fingroup]
+valK [lemma, in mathcomp.ssreflect.eqtype]
+valKd [lemma, in mathcomp.ssreflect.eqtype]
+valP [lemma, in mathcomp.ssreflect.eqtype]
+valq [projection, in mathcomp.algebra.rat]
+valqK [lemma, in mathcomp.algebra.rat]
+valq_frac [lemma, in mathcomp.algebra.rat]
+valZpK [lemma, in mathcomp.algebra.zmodp]
+val_qisom [lemma, in mathcomp.fingroup.quotient]
+val_quotient [lemma, in mathcomp.fingroup.quotient]
+val_coset [lemma, in mathcomp.fingroup.quotient]
+val_coset_prim [lemma, in mathcomp.fingroup.quotient]
+val_Clifford_act [lemma, in mathcomp.character.mxrepresentation]
+val_factmod_module [lemma, in mathcomp.character.mxrepresentation]
+val_submod_module [lemma, in mathcomp.character.mxrepresentation]
+val_factmodJ [lemma, in mathcomp.character.mxrepresentation]
+val_submodJ [lemma, in mathcomp.character.mxrepresentation]
+val_factmod_eq0 [lemma, in mathcomp.character.mxrepresentation]
+val_factmodS [lemma, in mathcomp.character.mxrepresentation]
+val_factmod_inj [lemma, in mathcomp.character.mxrepresentation]
+val_factmodK [lemma, in mathcomp.character.mxrepresentation]
+val_factmodP [lemma, in mathcomp.character.mxrepresentation]
+val_factmodE [lemma, in mathcomp.character.mxrepresentation]
+val_factmod [definition, in mathcomp.character.mxrepresentation]
+val_submod_eq0 [lemma, in mathcomp.character.mxrepresentation]
+val_submodS [lemma, in mathcomp.character.mxrepresentation]
+val_submod_inj [lemma, in mathcomp.character.mxrepresentation]
+val_submodK [lemma, in mathcomp.character.mxrepresentation]
+val_submodP [lemma, in mathcomp.character.mxrepresentation]
+val_submod1 [lemma, in mathcomp.character.mxrepresentation]
+val_submodE [lemma, in mathcomp.character.mxrepresentation]
+val_submod [definition, in mathcomp.character.mxrepresentation]
+val_ord_tuple [lemma, in mathcomp.ssreflect.tuple]
+val_enum_ord [lemma, in mathcomp.ssreflect.fintype]
+val_ord_enum [lemma, in mathcomp.ssreflect.fintype]
+val_seq_sub_enum [lemma, in mathcomp.ssreflect.fintype]
+val_sub_enum [lemma, in mathcomp.ssreflect.fintype]
+val_subact [lemma, in mathcomp.fingroup.action]
+val_eqE [lemma, in mathcomp.ssreflect.eqtype]
+val_eqP [lemma, in mathcomp.ssreflect.eqtype]
+val_insubd [lemma, in mathcomp.ssreflect.eqtype]
+val_inj [lemma, in mathcomp.ssreflect.eqtype]
+val_reprGLm [lemma, in mathcomp.character.mxabelem]
+val_Fp_nat [lemma, in mathcomp.algebra.zmodp]
+val_Zp_nat [lemma, in mathcomp.algebra.zmodp]
+Vandermonde [lemma, in mathcomp.ssreflect.binomial]
+vbasis [definition, in mathcomp.algebra.vector]
+vbasisP [lemma, in mathcomp.algebra.vector]
+vbasis_mem [lemma, in mathcomp.algebra.vector]
+vbasis_def [definition, in mathcomp.algebra.vector]
+vbasis1 [lemma, in mathcomp.field.falgebra]
+VChar [section, in mathcomp.character.vcharacter]
+vcharacter [library]
+vcharP [lemma, in mathcomp.character.vcharacter]
+vchar_aut [lemma, in mathcomp.character.vcharacter]
+vchar_norm2 [lemma, in mathcomp.character.vcharacter]
+vchar_norm1P [lemma, in mathcomp.character.vcharacter]
+vchar_orthonormalP [lemma, in mathcomp.character.vcharacter]
+vchar_mulr_closed [lemma, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal [section, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal.freeS [variable, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal.Inu [variable, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal.M [variable, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal.nS1 [variable, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal.nu [variable, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal.onS [variable, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal.oSS [variable, in mathcomp.character.vcharacter]
+VChar.CfDotOrthonormal.S [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal [section, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.dotSS [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.freeS [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.Inu [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.M [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.notS0 [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.nu [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.oSS [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.S [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.uniqS [variable, in mathcomp.character.vcharacter]
+VChar.CfdotPairwiseOrthogonal.Z_S [variable, in mathcomp.character.vcharacter]
+VChar.G [variable, in mathcomp.character.vcharacter]
+VChar.gT [variable, in mathcomp.character.vcharacter]
+VectFinMixin [lemma, in mathcomp.field.finfield]
+Vector [module, in mathcomp.algebra.vector]
+vector [library]
+VectorTheory [section, in mathcomp.algebra.vector]
+VectorTheory.BigCap [section, in mathcomp.algebra.vector]
+VectorTheory.BigCap.I [variable, in mathcomp.algebra.vector]
+VectorTheory.BigSum [section, in mathcomp.algebra.vector]
+VectorTheory.BigSumBasis [section, in mathcomp.algebra.vector]
+VectorTheory.BigSumBasis.I [variable, in mathcomp.algebra.vector]
+VectorTheory.BigSumBasis.P [variable, in mathcomp.algebra.vector]
+VectorTheory.BigSumBasis.Xs [variable, in mathcomp.algebra.vector]
+VectorTheory.BigSum.I [variable, in mathcomp.algebra.vector]
+VectorTheory.BinaryDirect [section, in mathcomp.algebra.vector]
+VectorTheory.free_b2mx [variable, in mathcomp.algebra.vector]
+VectorTheory.K [variable, in mathcomp.algebra.vector]
+VectorTheory.lin_b2mx [variable, in mathcomp.algebra.vector]
+VectorTheory.memvK [variable, in mathcomp.algebra.vector]
+VectorTheory.mem_r2v [variable, in mathcomp.algebra.vector]
+VectorTheory.mul_b2mx [variable, in mathcomp.algebra.vector]
+VectorTheory.NaryDirect [section, in mathcomp.algebra.vector]
+VectorTheory.row_b2mx [variable, in mathcomp.algebra.vector]
+VectorTheory.span_b2mx [variable, in mathcomp.algebra.vector]
+VectorTheory.SumExpr [section, in mathcomp.algebra.vector]
+VectorTheory.SumExpr.Binary [section, in mathcomp.algebra.vector]
+VectorTheory.SumExpr.Binary.S1 [variable, in mathcomp.algebra.vector]
+VectorTheory.SumExpr.Binary.S2 [variable, in mathcomp.algebra.vector]
+VectorTheory.SumExpr.Nary [section, in mathcomp.algebra.vector]
+VectorTheory.SumExpr.Nary.I [variable, in mathcomp.algebra.vector]
+VectorTheory.SumExpr.Nary.P [variable, in mathcomp.algebra.vector]
+VectorTheory.SumExpr.Nary.r [variable, in mathcomp.algebra.vector]
+VectorTheory.SumExpr.Nary.S_ [variable, in mathcomp.algebra.vector]
+VectorTheory.vs2mxD [variable, in mathcomp.algebra.vector]
+VectorTheory.vs2mxF [variable, in mathcomp.algebra.vector]
+VectorTheory.vs2mxI [variable, in mathcomp.algebra.vector]
+VectorTheory.vs2mxP [variable, in mathcomp.algebra.vector]
+VectorTheory.vs2mx_sum [variable, in mathcomp.algebra.vector]
+VectorTheory.vs2mx0 [variable, in mathcomp.algebra.vector]
+VectorTheory.vT [variable, in mathcomp.algebra.vector]
+Vector.axiom [abbreviation, in mathcomp.algebra.vector]
+Vector.axiom_def [definition, in mathcomp.algebra.vector]
+Vector.base [projection, in mathcomp.algebra.vector]
+Vector.choiceType [definition, in mathcomp.algebra.vector]
+Vector.class [definition, in mathcomp.algebra.vector]
+Vector.Class [constructor, in mathcomp.algebra.vector]
+Vector.ClassDef [section, in mathcomp.algebra.vector]
+Vector.ClassDef.cT [variable, in mathcomp.algebra.vector]
+Vector.ClassDef.phR [variable, in mathcomp.algebra.vector]
+Vector.ClassDef.R [variable, in mathcomp.algebra.vector]
+Vector.ClassDef.T [variable, in mathcomp.algebra.vector]
+Vector.ClassDef.xT [variable, in mathcomp.algebra.vector]
+Vector.class_of [record, in mathcomp.algebra.vector]
+Vector.clone [definition, in mathcomp.algebra.vector]
+Vector.dim [definition, in mathcomp.algebra.vector]
+Vector.eqType [definition, in mathcomp.algebra.vector]
+Vector.Exports [module, in mathcomp.algebra.vector]
+Vector.Exports.VectMixin [abbreviation, in mathcomp.algebra.vector]
+Vector.Exports.VectType [abbreviation, in mathcomp.algebra.vector]
+Vector.Exports.vectType [abbreviation, in mathcomp.algebra.vector]
+[ vectType _ of _ ] (form_scope) [notation, in mathcomp.algebra.vector]
+[ vectType _ of _ for _ ] (form_scope) [notation, in mathcomp.algebra.vector]
+'End ( _ ) (type_scope) [notation, in mathcomp.algebra.vector]
+'Hom ( _ , _ ) (type_scope) [notation, in mathcomp.algebra.vector]
+{ vspace _ } (type_scope) [notation, in mathcomp.algebra.vector]
+Vector.Hom [constructor, in mathcomp.algebra.vector]
+Vector.hom [inductive, in mathcomp.algebra.vector]
+Vector.InternalTheory [module, in mathcomp.algebra.vector]
+Vector.InternalTheory.b2mx [definition, in mathcomp.algebra.vector]
+Vector.InternalTheory.b2mxK [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.f2mx [definition, in mathcomp.algebra.vector]
+Vector.InternalTheory.gen_vs2mx [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.Hom [section, in mathcomp.algebra.vector]
+Vector.InternalTheory.Hom.aT [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.Hom.R [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.Hom.rT [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.Iso [section, in mathcomp.algebra.vector]
+Vector.InternalTheory.Iso.R [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.Iso.rT [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.Iso.vT [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.Iso.v2r_bij [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.mx2vs [definition, in mathcomp.algebra.vector]
+Vector.InternalTheory.mx2vsK [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.mx2vs_subproof [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.r2v [definition, in mathcomp.algebra.vector]
+Vector.InternalTheory.r2vK [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.r2v_inj [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.r2v_subproof [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.Vspace [section, in mathcomp.algebra.vector]
+Vector.InternalTheory.Vspace.K [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.Vspace.vT [variable, in mathcomp.algebra.vector]
+Vector.InternalTheory.vs2mx [definition, in mathcomp.algebra.vector]
+Vector.InternalTheory.vs2mxK [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.v2r [definition, in mathcomp.algebra.vector]
+Vector.InternalTheory.v2rK [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.v2r_inj [lemma, in mathcomp.algebra.vector]
+Vector.InternalTheory.v2r_subproof [lemma, in mathcomp.algebra.vector]
+Vector.lmodType [definition, in mathcomp.algebra.vector]
+Vector.mixin [projection, in mathcomp.algebra.vector]
+Vector.Mixin [constructor, in mathcomp.algebra.vector]
+Vector.mixin_of [inductive, in mathcomp.algebra.vector]
+Vector.OtherDefs [section, in mathcomp.algebra.vector]
+Vector.pack [definition, in mathcomp.algebra.vector]
+Vector.Pack [constructor, in mathcomp.algebra.vector]
+Vector.sort [projection, in mathcomp.algebra.vector]
+Vector.Space [constructor, in mathcomp.algebra.vector]
+Vector.space [inductive, in mathcomp.algebra.vector]
+Vector.type [record, in mathcomp.algebra.vector]
+Vector.xclass [abbreviation, in mathcomp.algebra.vector]
+Vector.zmodType [definition, in mathcomp.algebra.vector]
+vec_mx_delta [lemma, in mathcomp.algebra.matrix]
+vec_mx_eq0 [lemma, in mathcomp.algebra.matrix]
+vec_mxK [lemma, in mathcomp.algebra.matrix]
+vec_mx [definition, in mathcomp.algebra.matrix]
+vec_mx_key [lemma, in mathcomp.algebra.matrix]
+vline [definition, in mathcomp.algebra.vector]
+vlineP [lemma, in mathcomp.algebra.vector]
+vpick [definition, in mathcomp.algebra.vector]
+vpick0 [lemma, in mathcomp.algebra.vector]
+vrefl [lemma, in mathcomp.ssreflect.eqtype]
+vrefl_rect [definition, in mathcomp.ssreflect.eqtype]
+vsolve_eqP [lemma, in mathcomp.algebra.vector]
+vsolve_eq [definition, in mathcomp.algebra.vector]
+VspaceDefs [section, in mathcomp.algebra.vector]
+VspaceDefs.K [variable, in mathcomp.algebra.vector]
+VspaceDefs.vT [variable, in mathcomp.algebra.vector]
+vspaceOver [definition, in mathcomp.field.fieldext]
+vspaceOverP [lemma, in mathcomp.field.fieldext]
+vspaceOver_refBase [lemma, in mathcomp.field.fieldext]
+vspaceP [lemma, in mathcomp.algebra.vector]
+vspace_modr [lemma, in mathcomp.algebra.vector]
+vspace_modl [lemma, in mathcomp.algebra.vector]
+vspace_key [lemma, in mathcomp.algebra.vector]
+vspace1_neq0 [lemma, in mathcomp.field.falgebra]
+vsproj [definition, in mathcomp.algebra.vector]
+vsprojK [lemma, in mathcomp.algebra.vector]
+vsproj_is_linear [lemma, in mathcomp.algebra.vector]
+vsproj_def [definition, in mathcomp.algebra.vector]
+vsproj_key [lemma, in mathcomp.algebra.vector]
+vsubmxK [lemma, in mathcomp.algebra.matrix]
+vsval [definition, in mathcomp.algebra.vector]
+vsvalK [lemma, in mathcomp.algebra.vector]
+vsval_invf [lemma, in mathcomp.field.fieldext]
+vsval_multiplicative [lemma, in mathcomp.field.fieldext]
+vsval_is_linear [lemma, in mathcomp.algebra.vector]
+vsval_invr [lemma, in mathcomp.field.falgebra]
+vsval_unitr [lemma, in mathcomp.field.falgebra]
+vs2mx_sum_expr_subproof [definition, in mathcomp.algebra.vector]
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(23233 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1373 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(213 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3475 entries)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(89 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(11853 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(359 entries)
Axiom IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(47 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(103 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(266 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1118 entries)
Abbreviation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(691 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3461 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(185 entries)
+
+ + + +
+ + + \ No newline at end of file -- cgit v1.2.3