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 | (100113 entries) |

Notation 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 | (1864 entries) |

Binder 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 | (49278 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 | (1631 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 | (6978 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 | (94 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 | (14781 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 | (75 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 | (222 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 | (131 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 | (2030 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 | (2189 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 | (1149 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 | (19126 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 | (565 entries) |

## V (lemma)

valG [in mathcomp.fingroup.fingroup]valgM [in mathcomp.fingroup.fingroup]

valK [in mathcomp.ssreflect.eqtype]

valKd [in mathcomp.ssreflect.eqtype]

valP [in mathcomp.ssreflect.eqtype]

valqK [in mathcomp.algebra.rat]

valq_frac [in mathcomp.algebra.rat]

valZpK [in mathcomp.algebra.zmodp]

val_qisom [in mathcomp.fingroup.quotient]

val_quotient [in mathcomp.fingroup.quotient]

val_coset [in mathcomp.fingroup.quotient]

val_coset_prim [in mathcomp.fingroup.quotient]

val_ord_tuple [in mathcomp.ssreflect.tuple]

val_tcast [in mathcomp.ssreflect.tuple]

val_Fp_nat [in mathcomp.algebra.zmodp]

val_Zp_nat [in mathcomp.algebra.zmodp]

val_subact [in mathcomp.fingroup.action]

val_reprGLm [in mathcomp.character.mxabelem]

val_Clifford_act [in mathcomp.character.mxrepresentation]

val_factmod_module [in mathcomp.character.mxrepresentation]

val_submod_module [in mathcomp.character.mxrepresentation]

val_factmodJ [in mathcomp.character.mxrepresentation]

val_submodJ [in mathcomp.character.mxrepresentation]

val_factmod_eq0 [in mathcomp.character.mxrepresentation]

val_factmodS [in mathcomp.character.mxrepresentation]

val_factmod_inj [in mathcomp.character.mxrepresentation]

val_factmodK [in mathcomp.character.mxrepresentation]

val_factmodP [in mathcomp.character.mxrepresentation]

val_factmodE [in mathcomp.character.mxrepresentation]

val_submod_eq0 [in mathcomp.character.mxrepresentation]

val_submodS [in mathcomp.character.mxrepresentation]

val_submod_inj [in mathcomp.character.mxrepresentation]

val_submodK [in mathcomp.character.mxrepresentation]

val_submodP [in mathcomp.character.mxrepresentation]

val_submod1 [in mathcomp.character.mxrepresentation]

val_submodE [in mathcomp.character.mxrepresentation]

val_fracq [in mathcomp.algebra.rat]

val_enum_ord [in mathcomp.ssreflect.fintype]

val_ord_enum [in mathcomp.ssreflect.fintype]

val_seq_sub_enum [in mathcomp.ssreflect.fintype]

val_eqE [in mathcomp.ssreflect.eqtype]

val_eqP [in mathcomp.ssreflect.eqtype]

val_insubd [in mathcomp.ssreflect.eqtype]

val_inj [in mathcomp.ssreflect.eqtype]

Vandermonde [in mathcomp.ssreflect.binomial]

vbasisP [in mathcomp.algebra.vector]

vbasis_mem [in mathcomp.algebra.vector]

vbasis1 [in mathcomp.field.falgebra]

vcharP [in mathcomp.character.vcharacter]

vchar_aut [in mathcomp.character.vcharacter]

vchar_norm2 [in mathcomp.character.vcharacter]

vchar_norm1P [in mathcomp.character.vcharacter]

vchar_orthonormalP [in mathcomp.character.vcharacter]

vchar_mulr_closed [in mathcomp.character.vcharacter]

VectorInternalTheory.b2mxK [in mathcomp.algebra.vector]

VectorInternalTheory.gen_vs2mx [in mathcomp.algebra.vector]

VectorInternalTheory.mx2vsK [in mathcomp.algebra.vector]

VectorInternalTheory.mx2vs_subproof [in mathcomp.algebra.vector]

VectorInternalTheory.r2vK [in mathcomp.algebra.vector]

VectorInternalTheory.r2v_inj [in mathcomp.algebra.vector]

VectorInternalTheory.r2v_subproof [in mathcomp.algebra.vector]

VectorInternalTheory.vs2mxK [in mathcomp.algebra.vector]

VectorInternalTheory.v2rK [in mathcomp.algebra.vector]

VectorInternalTheory.v2r_inj [in mathcomp.algebra.vector]

VectorInternalTheory.v2r_subproof [in mathcomp.algebra.vector]

vec_mx_delta [in mathcomp.algebra.matrix]

vec_mx_eq0 [in mathcomp.algebra.matrix]

vec_mxK [in mathcomp.algebra.matrix]

vec_mx_key [in mathcomp.algebra.matrix]

vlineP [in mathcomp.algebra.vector]

void_enumP [in mathcomp.ssreflect.fintype]

vpick0 [in mathcomp.algebra.vector]

vrefl [in mathcomp.ssreflect.eqtype]

vsolve_eqP [in mathcomp.algebra.vector]

vspaceOverP [in mathcomp.field.fieldext]

vspaceOver_refBase [in mathcomp.field.fieldext]

vspaceP [in mathcomp.algebra.vector]

vspace_modr [in mathcomp.algebra.vector]

vspace_modl [in mathcomp.algebra.vector]

vspace1_neq0 [in mathcomp.field.falgebra]

vsprojK [in mathcomp.algebra.vector]

vsproj_is_linear [in mathcomp.algebra.vector]

vsproj_key [in mathcomp.algebra.vector]

vsubmxK [in mathcomp.algebra.matrix]

vsvalK [in mathcomp.algebra.vector]

vsval_invf [in mathcomp.field.fieldext]

vsval_multiplicative [in mathcomp.field.fieldext]

vsval_is_linear [in mathcomp.algebra.vector]

vsval_invr [in mathcomp.field.falgebra]

vsval_unitr [in mathcomp.field.falgebra]

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 | (100113 entries) |

Notation 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 | (1864 entries) |

Binder 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 | (49278 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 | (1631 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 | (6978 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 | (94 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 | (14781 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 | (75 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 | (222 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 | (131 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 | (2030 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 | (2189 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 | (1149 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 | (19126 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 | (565 entries) |