Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (14626 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (165 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (112 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7292 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (250 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (390 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (84 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3144 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (126 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2221 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (53 entries)

V

V [definition, in finmodule]
val [projection, in eqtype]
valG [lemma, in fingroup]
valgM [lemma, in fingroup]
valK [lemma, in eqtype]
valKd [lemma, in eqtype]
valP [lemma, in eqtype]
valWact [definition, in mxrepresentation]
valZpK [lemma, in zmodp]
val_submodS [lemma, in mxrepresentation]
val_subact [lemma, in action]
val_factmodK [lemma, in mxrepresentation]
val_factmodS [lemma, in mxrepresentation]
val_submodP [lemma, in mxrepresentation]
val_factmod_linear [definition, in mxrepresentation]
val_submod_linear [definition, in mxrepresentation]
val_submodE [lemma, in mxrepresentation]
val_submod_inj [lemma, in mxrepresentation]
val_factmod_module [lemma, in mxrepresentation]
val_factmodP [lemma, in mxrepresentation]
val_insubd [lemma, in eqtype]
val_inj [lemma, in eqtype]
val_submod_eq0 [lemma, in mxrepresentation]
val_submodK [lemma, in mxrepresentation]
val_quotient [lemma, in quotient]
val_coset_prim [lemma, in quotient]
val_submodJ [lemma, in mxrepresentation]
val_submod_module [lemma, in mxrepresentation]
val_factmodJ [lemma, in mxrepresentation]
val_factmod [definition, in mxrepresentation]
val_eqP [lemma, in eqtype]
val_reprGLm [lemma, in mxabelem]
val_qisom [lemma, in quotient]
val_eqE [lemma, in eqtype]
val_submod1 [lemma, in mxrepresentation]
val_sub_enum [lemma, in fintype]
val_Clifford_act [lemma, in mxrepresentation]
val_enum_ord [lemma, in fintype]
val_factmod_eq0 [lemma, in mxrepresentation]
val_factmodE [lemma, in mxrepresentation]
val_submod [definition, in mxrepresentation]
val_ord_enum [lemma, in fintype]
val_seq_sub_enum [lemma, in fintype]
val_Fp_nat [lemma, in zmodp]
val_factmod_inj [lemma, in mxrepresentation]
val_ord_tuple [lemma, in tuple]
val_Zp_nat [lemma, in zmodp]
val_coset [lemma, in quotient]
vbasis [definition, in vector]
vbasis0 [lemma, in vector]
vdim [definition, in vector]
vector [library]
VectorType [module, in vector]
VectorTypeTheory [section, in vector]
VectorTypeTheory.m [variable, in vector]
VectorTypeTheory.n [variable, in vector]
VectorTypeTheory.R [variable, in vector]
VectorTypeTheory.V [variable, in vector]
VectorType.base [projection, in vector]
VectorType.choiceType [definition, in vector]
VectorType.Class [constructor, in vector]
VectorType.class [definition, in vector]
VectorType.ClassDef [section, in vector]
VectorType.ClassDef.R [variable, in vector]
VectorType.class_of [record, in vector]
VectorType.clone [definition, in vector]
VectorType.dim [projection, in vector]
VectorType.eqType [definition, in vector]
VectorType.Exports.VectMixin [abbreviation, in vector]
VectorType.Exports.vectType [abbreviation, in vector]
VectorType.Exports.VectType [abbreviation, in vector]
VectorType.lmodType [definition, in vector]
VectorType.Mixin [constructor, in vector]
VectorType.mixin [projection, in vector]
VectorType.mixin_of [record, in vector]
VectorType.pack [definition, in vector]
VectorType.Pack [constructor, in vector]
VectorType.sort [projection, in vector]
VectorType.type [record, in vector]
VectorType.v2rv_isomorphism [projection, in vector]
VectorType.zmodType [definition, in vector]
vector_addv_proof [lemma, in vector]
vector_addv_expr [definition, in vector]
vec_mxK [lemma, in matrix]
vec_mx_delta [lemma, in matrix]
vec_mx_linear [definition, in matrix]
vec_mx_additive [definition, in matrix]
vec_mx [definition, in matrix]
vec_mx_eq0 [lemma, in matrix]
vpick [definition, in vector]
vpick0 [lemma, in vector]
vpredType [definition, in vector]
vrefl [lemma, in eqtype]
vseq2mxeq [lemma, in vector]
vsolve_eq [definition, in vector]
vsolve_eqP [lemma, in vector]
VSpace [constructor, in vector]
vspace [record, in vector]
VSpaceDef [section, in vector]
VSpaceDef.BigCap [section, in vector]
VSpaceDef.BigCap.I [variable, in vector]
VSpaceDef.BigDim [section, in vector]
VSpaceDef.BigDim.I [variable, in vector]
VSpaceDef.BigSum [section, in vector]
VSpaceDef.BigSumBasis [section, in vector]
VSpaceDef.BigSumBasis.I [variable, in vector]
VSpaceDef.BigSum.I [variable, in vector]
VSpaceDef.BinaryDirect [section, in vector]
VSpaceDef.K [variable, in vector]
VSpaceDef.NaryDirect [section, in vector]
VSpaceDef.NaryDirect.I [variable, in vector]
VSpaceDef.NaryDirect.P [variable, in vector]
VSpaceDef.SumExpr [section, in vector]
VSpaceDef.SumExpr.Binary [section, in vector]
VSpaceDef.SumExpr.Binary.S1 [variable, in vector]
VSpaceDef.SumExpr.Binary.S2 [variable, in vector]
VSpaceDef.SumExpr.Nary [section, in vector]
VSpaceDef.SumExpr.Nary.I [variable, in vector]
VSpaceDef.SumExpr.Nary.P [variable, in vector]
VSpaceDef.SumExpr.Nary.S_ [variable, in vector]
VSpaceDef.SumExpr.Vector [section, in vector]
VSpaceDef.SumExpr.Vector.v [variable, in vector]
VSpaceDef.V [variable, in vector]
vspaceP [lemma, in vector]
vspaceType [abbreviation, in vector]
vspace_choiceMixin [definition, in vector]
vspace_modr [lemma, in vector]
vspace_modl [lemma, in vector]
vspace_ax [lemma, in vector]
vspace_of [definition, in vector]
vspace_for_choiceType [definition, in vector]
vspace_of_eqType [definition, in vector]
vspace_of_subType [definition, in vector]
vspace_choiceType [definition, in vector]
vspace_eqType [definition, in vector]
vspace_eqMixin [definition, in vector]
vspace_subType [definition, in vector]
vsubmxK [lemma, in matrix]
vs2mx [projection, in vector]
vs2mxf [lemma, in vector]
vs2mxK [lemma, in vector]
vs2mx_sum [lemma, in vector]
vs2mx_morph [lemma, in vector]
vs2mx0 [lemma, in vector]
v2rv [abbreviation, in vector]
v2rv [abbreviation, in vector]
v2rv [abbreviation, in vector]
v2rv [abbreviation, in vector]
v2rvK [lemma, in vector]
v2rv_isomorphism [definition, in vector]
v2rv_linear_proof [lemma, in vector]
v2rv_inj [lemma, in vector]
v2rv_bij [lemma, in vector]
v2rv_isom [lemma, in vector]
v2rv_linear [definition, in vector]



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (14626 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (165 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (112 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7292 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (250 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (390 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (84 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3144 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (126 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2221 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (53 entries)