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_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_finset [def, in mathcomp.classical.functions]
val_finsetK [prf, in mathcomp.classical.functions]
val_Fp_nat [prf, in mathcomp.algebra.zmodp]
val_fracq [prf, in mathcomp.algebra.rat]
val_fset_sub_enum [prf, in mathcomp.finmap.finmap]
val_in_fset [prf, in mathcomp.finmap.finmap]
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_seq_sub_enum [prf, in mathcomp.boot.fintype]
val_subact [prf, in mathcomp.finite_group.action]
val_subdef [def, in mathcomp.boot.eqtype]
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]
valL [abbrev, in mathcomp.classical.functions]
valL [abbrev, in mathcomp.classical.functions]
valL_ [def, in mathcomp.classical.functions]
valL_bijP [prf, in mathcomp.classical.functions]
valL_injP [prf, in mathcomp.classical.functions]
valL_isfun [prf, in mathcomp.classical.functions]
valL_some_inv [prf, in mathcomp.classical.functions]
valL_surjP [prf, in mathcomp.classical.functions]
valLfun [abbrev, in mathcomp.classical.functions]
valLfun_ [def, in mathcomp.classical.functions]
valLfunK [prf, in mathcomp.classical.functions]
valLfunP [prf, in mathcomp.classical.functions]
valLK [prf, in mathcomp.classical.functions]
valLR [def, in mathcomp.classical.functions]
valLR_bijP [prf, in mathcomp.classical.functions]
valLR_injP [prf, in mathcomp.classical.functions]
valLR_surjP [prf, in mathcomp.classical.functions]
valLRE [prf, in mathcomp.classical.functions]
valLRfun [def, in mathcomp.classical.functions]
valLRfun_inj [prf, in mathcomp.classical.functions]
valLRfunE [prf, in mathcomp.classical.functions]
valLRK [prf, in mathcomp.classical.functions]
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]
valR [def, in mathcomp.classical.functions]
valR_fun [def, in mathcomp.classical.functions]
valRK [prf, in mathcomp.classical.functions]
valRP [prf, in mathcomp.classical.functions]
valZpK [prf, in mathcomp.boot.fintype]
Vandermonde [prf, in mathcomp.boot.binomial]
Vandermonde [def, in mathcomp.algebra.matrix]
variance [def, in mathcomp.analysis.probability_theory.random_variable]
variance_cst [prf, in mathcomp.analysis.probability_theory.random_variable]
variance_fin_num [prf, in mathcomp.analysis.probability_theory.random_variable]
variance_ge0 [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceB [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceB_cst_l [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceB_cst_r [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceD [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceD_cst_l [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceD_cst_r [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceE [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceN [prf, in mathcomp.analysis.probability_theory.random_variable]
varianceZ [prf, in mathcomp.analysis.probability_theory.random_variable]
variation [def, in mathcomp.analysis.numfun]
variation_cat [prf, in mathcomp.analysis.numfun]
variation_ge0 [prf, in mathcomp.analysis.numfun]
variation_itv_partitionLR [prf, in mathcomp.analysis.numfun]
variation_le [prf, in mathcomp.analysis.numfun]
variation_next [prf, in mathcomp.analysis.numfun]
variation_nil [prf, in mathcomp.analysis.numfun]
variation_opp_rev [prf, in mathcomp.analysis.numfun]
variation_prev [prf, in mathcomp.analysis.numfun]
variation_rev_opp [prf, in mathcomp.analysis.numfun]
variation_subseq [prf, in mathcomp.analysis.numfun]
variation_zip [prf, in mathcomp.analysis.numfun]
variationD [abbrev, in mathcomp.analysis.numfun]
variationN [prf, in mathcomp.analysis.numfun]
variations [def, in mathcomp.analysis.numfun]
variations_neq0 [prf, in mathcomp.analysis.numfun]
variations_opp [prf, in mathcomp.analysis.numfun]
variations_variation [prf, in mathcomp.analysis.numfun]
variationsN [prf, in mathcomp.analysis.numfun]
variationsxx [prf, in mathcomp.analysis.numfun]
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]
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]
vitali_collection_partition [def, in mathcomp.analysis.normedtype_theory.vitali_lemma]
vitali_collection_partition_ub_gt0 [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
vitali_cover [def, in mathcomp.analysis.lebesgue_measure]
vitali_coverS [prf, in mathcomp.analysis.lebesgue_measure]
vitali_lemma [file, in mathcomp.analysis.normedtype_theory.vitali_lemma]
vitali_lemma_finite [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
vitali_lemma_finite_cover [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
vitali_lemma_infinite [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
vitali_lemma_infinite_cover [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
vitali_theorem [prf, in mathcomp.analysis.lebesgue_measure]
vitali_theorem_corollary [prf, in mathcomp.analysis.lebesgue_measure]
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]