V (Global Index)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
V
v2r [proj, in mathcomp.algebra.vector]v2r_bijective [proj, in mathcomp.algebra.vector]
v2r_semilinear [proj, in mathcomp.algebra.vector]
val [abbrev, in mathcomp.boot.monoid]
val [abbrev, in mathcomp.boot.monoid]
val [abbrev, in mathcomp.boot.eqtype]
val [abbrev, in mathcomp.boot.eqtype]
val1 [prf, in mathcomp.boot.monoid]
val_castt [prf, in mathcomp.algebra.tensor]
val_Clifford_act [prf, in mathcomp.group_representation.mxrepresentation]
val_coset [prf, in mathcomp.finite_group.quotient]
val_coset_prim [prf, in mathcomp.finite_group.quotient]
val_enum_ord [prf, in mathcomp.boot.fintype]
val_eqE [prf, in mathcomp.boot.eqtype]
val_eqP [prf, in mathcomp.boot.eqtype]
val_factmod [def, in mathcomp.group_representation.mxrepresentation]
val_factmod_eq0 [prf, in mathcomp.group_representation.mxrepresentation]
val_factmod_inj [prf, in mathcomp.group_representation.mxrepresentation]
val_factmod_module [prf, in mathcomp.group_representation.mxrepresentation]
val_factmodE [prf, in mathcomp.group_representation.mxrepresentation]
val_factmodJ [prf, in mathcomp.group_representation.mxrepresentation]
val_factmodK [prf, in mathcomp.group_representation.mxrepresentation]
val_factmodP [prf, in mathcomp.group_representation.mxrepresentation]
val_factmodS [prf, in mathcomp.group_representation.mxrepresentation]
val_Fp_nat [prf, in mathcomp.algebra.zmodp]
val_fracq [prf, in mathcomp.algebra.rat]
val_inj [prf, in mathcomp.boot.eqtype]
val_insubd [prf, in mathcomp.boot.eqtype]
val_ord_enum [prf, in mathcomp.boot.fintype]
val_ord_tuple [prf, in mathcomp.boot.tuple]
val_qisom [prf, in mathcomp.finite_group.quotient]
val_quotient [prf, in mathcomp.finite_group.quotient]
val_reprGLm [prf, in mathcomp.group_representation.mxabelem]
val_seq_sub_enum [prf, in mathcomp.boot.fintype]
val_subact [prf, in mathcomp.finite_group.action]
val_subdef [def, in mathcomp.boot.eqtype]
val_submod [def, in mathcomp.group_representation.mxrepresentation]
val_submod1 [prf, in mathcomp.group_representation.mxrepresentation]
val_submod_eq0 [prf, in mathcomp.group_representation.mxrepresentation]
val_submod_inj [prf, in mathcomp.group_representation.mxrepresentation]
val_submod_module [prf, in mathcomp.group_representation.mxrepresentation]
val_submodE [prf, in mathcomp.group_representation.mxrepresentation]
val_submodJ [prf, in mathcomp.group_representation.mxrepresentation]
val_submodK [prf, in mathcomp.group_representation.mxrepresentation]
val_submodP [prf, in mathcomp.group_representation.mxrepresentation]
val_submodS [prf, in mathcomp.group_representation.mxrepresentation]
val_tcast [prf, in mathcomp.boot.tuple]
val_Zp_nat [prf, in mathcomp.algebra.zmodp]
valG [prf, in mathcomp.finite_group.fingroup]
valgM [prf, in mathcomp.finite_group.fingroup]
valK [prf, in mathcomp.boot.eqtype]
valKd [prf, in mathcomp.boot.eqtype]
valM [prf, in mathcomp.boot.monoid]
valP [prf, in mathcomp.boot.eqtype]
valq [proj, in mathcomp.algebra.rat]
valq_frac [prf, in mathcomp.algebra.rat]
valqK [prf, in mathcomp.algebra.rat]
valZpK [prf, in mathcomp.boot.fintype]
Vandermonde [prf, in mathcomp.boot.binomial]
Vandermonde [def, in mathcomp.algebra.matrix]
vbasis [def, in mathcomp.algebra.vector]
vbasis1 [prf, in mathcomp.field.falgebra]
vbasis_def [def, in mathcomp.algebra.vector]
vbasis_mem [prf, in mathcomp.algebra.vector]
vbasis_unlockable [def, in mathcomp.algebra.vector]
vbasisP [prf, in mathcomp.algebra.vector]
vchar_aut [prf, in mathcomp.group_representation.vcharacter]
vchar_mulr_closed [prf, in mathcomp.group_representation.vcharacter]
vchar_norm1P [prf, in mathcomp.group_representation.vcharacter]
vchar_norm2 [prf, in mathcomp.group_representation.vcharacter]
vchar_orthonormalP [prf, in mathcomp.group_representation.vcharacter]
vcharacter [file, in mathcomp.group_representation.vcharacter]
vcharP [prf, in mathcomp.group_representation.vcharacter]
vec_mx [def, in mathcomp.algebra.matrix]
vec_mx_delta [prf, in mathcomp.algebra.matrix]
vec_mx_eq0 [prf, in mathcomp.algebra.matrix]
vec_mx_key [prf, in mathcomp.algebra.matrix]
vec_mxK [prf, in mathcomp.algebra.matrix]
vector [file, in mathcomp.algebra.vector]
Vector [abbrev, in mathcomp.algebra.vector]
Vector [mod, in mathcomp.algebra.vector]
Vector.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.algebra.vector]
Vector.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.algebra.vector]
Vector.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.algebra.vector]
Vector.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.algebra.vector]
Vector.Algebra_hasAdd_mixin [proj, in mathcomp.algebra.vector]
Vector.Algebra_hasOpp_mixin [proj, in mathcomp.algebra.vector]
Vector.Algebra_hasZero_mixin [proj, in mathcomp.algebra.vector]
Vector.axioms_ [rec, in mathcomp.algebra.vector]
Vector.choice_hasChoice_mixin [proj, in mathcomp.algebra.vector]
Vector.class [proj, in mathcomp.algebra.vector]
Vector.clone [abbrev, in mathcomp.algebra.vector]
Vector.copy [abbrev, in mathcomp.algebra.vector]
Vector.eqtype_hasDecEq_mixin [proj, in mathcomp.algebra.vector]
Vector.Exports [mod, in mathcomp.algebra.vector]
Vector.Exports.join_vector_Vector_between_Algebra_BaseZmodule_and_vector_SemiVector [def, in mathcomp.algebra.vector]
Vector.Exports.join_vector_Vector_between_GRing_Lmodule_and_vector_SemiVector [def, in mathcomp.algebra.vector]
Vector.Exports.join_vector_Vector_between_vector_SemiVector_and_Algebra_Zmodule [def, in mathcomp.algebra.vector]
Vector.Exports.vectType [abbrev, in mathcomp.algebra.vector]
Vector.GRing_Nmodule_isLSemiModule_mixin [proj, in mathcomp.algebra.vector]
Vector.on [abbrev, in mathcomp.algebra.vector]
Vector.on_ [abbrev, in mathcomp.algebra.vector]
Vector.pack_ [def, in mathcomp.algebra.vector]
Vector.phant_clone [def, in mathcomp.algebra.vector]
Vector.phant_on_ [def, in mathcomp.algebra.vector]
Vector.sort [proj, in mathcomp.algebra.vector]
Vector.type [rec, in mathcomp.algebra.vector]
Vector.vector_LSemiModule_hasFinDim_mixin [proj, in mathcomp.algebra.vector]
vector_axiom [abbrev, in mathcomp.algebra.vector]
vector_axiom_def [def, in mathcomp.algebra.vector]
vector_subdef [def, in mathcomp.algebra.vector]
VectorElpiOperations [mod, in mathcomp.algebra.vector]
VectorExports [mod, in mathcomp.algebra.vector]
VectorInternalTheory [mod, in mathcomp.algebra.vector]
VectorInternalTheory.b2mx [def, in mathcomp.algebra.vector]
VectorInternalTheory.b2mxK [prf, in mathcomp.algebra.vector]
VectorInternalTheory.f2mx [def, in mathcomp.algebra.vector]
VectorInternalTheory.gen_vs2mx [prf, in mathcomp.algebra.vector]
VectorInternalTheory.mx2vs [def, in mathcomp.algebra.vector]
VectorInternalTheory.mx2vsK [prf, in mathcomp.algebra.vector]
VectorInternalTheory.r2v [def, in mathcomp.algebra.vector]
VectorInternalTheory.r2v_inj [prf, in mathcomp.algebra.vector]
VectorInternalTheory.r2vK [prf, in mathcomp.algebra.vector]
VectorInternalTheory.v2r [def, in mathcomp.algebra.vector]
VectorInternalTheory.v2r_inj [prf, in mathcomp.algebra.vector]
VectorInternalTheory.v2rK [prf, in mathcomp.algebra.vector]
VectorInternalTheory.vs2mx [def, in mathcomp.algebra.vector]
VectorInternalTheory.vs2mxK [prf, in mathcomp.algebra.vector]
vline [def, in mathcomp.algebra.vector]
vlineP [prf, in mathcomp.algebra.vector]
vmrefl [abbrev, in mathcomp.boot.ssrAC]
void_enumP [prf, in mathcomp.boot.fintype]
vpick [def, in mathcomp.algebra.vector]
vpick0 [prf, in mathcomp.algebra.vector]
vrefl [prf, in mathcomp.boot.eqtype]
vrefl_rect [def, in mathcomp.boot.eqtype]
vs2mx_sum_expr [def, in mathcomp.algebra.vector]
vsolve_eq [def, in mathcomp.algebra.vector]
vsolve_eqP [prf, in mathcomp.algebra.vector]
vspace1_neq0 [prf, in mathcomp.field.falgebra]
vspace_modl [prf, in mathcomp.algebra.vector]
vspace_modr [prf, in mathcomp.algebra.vector]
vspace_predType [def, in mathcomp.algebra.vector]
vspaceOver [def, in mathcomp.field.fieldext]
vspaceOver_refBase [prf, in mathcomp.field.fieldext]
vspaceOverP [prf, in mathcomp.field.fieldext]
vspaceP [prf, in mathcomp.algebra.vector]
vsproj [def, in mathcomp.algebra.vector]
vsproj_def [def, in mathcomp.algebra.vector]
vsproj_is_linear [prf, in mathcomp.algebra.vector]
vsproj_key [prf, in mathcomp.algebra.vector]
vsproj_unlockable [def, in mathcomp.algebra.vector]
vsprojK [prf, in mathcomp.algebra.vector]
vsubmxK [prf, in mathcomp.algebra.matrix]
vsval [def, in mathcomp.algebra.vector]
vsval_invf [prf, in mathcomp.field.fieldext]
vsval_invr [prf, in mathcomp.field.falgebra]
vsval_is_linear [prf, in mathcomp.algebra.vector]
vsval_is_multiplicative [def, in mathcomp.field.fieldext]
vsval_monoid_morphism [prf, in mathcomp.field.fieldext]
vsval_unitr [prf, in mathcomp.field.falgebra]
vsvalK [prf, in mathcomp.algebra.vector]