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) |