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 | (69505 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 | (1943 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 | (39748 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 | (379 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 | (3958 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 | (91 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 | (13542 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 | (480 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 | (45 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 | (134 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 | (452 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 | (1344 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 | (1014 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 | (6127 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 | (248 entries) |

## T (definition)

tagged_choiceType [in mathcomp.ssreflect.choice]tagged_as [in mathcomp.ssreflect.eqtype]

tag_countType [in mathcomp.ssreflect.choice]

tag_countMixin [in mathcomp.ssreflect.choice]

tag_of_pair [in mathcomp.ssreflect.choice]

tag_finType [in mathcomp.ssreflect.fintype]

tag_finMixin [in mathcomp.ssreflect.fintype]

tag_enum [in mathcomp.ssreflect.fintype]

tag_eqType [in mathcomp.ssreflect.eqtype]

tag_eqMixin [in mathcomp.ssreflect.eqtype]

tag_eq [in mathcomp.ssreflect.eqtype]

take [in mathcomp.ssreflect.seq]

take_tuple [in mathcomp.ssreflect.tuple]

tally [in mathcomp.ssreflect.seq]

tally_seq [in mathcomp.ssreflect.seq]

tcast [in mathcomp.ssreflect.tuple]

tfgraph [in mathcomp.ssreflect.finfun]

tfgraph_inv [in mathcomp.ssreflect.finfun]

thead [in mathcomp.ssreflect.tuple]

tnth [in mathcomp.ssreflect.tuple]

to [in mathcomp.solvable.burnside_app]

tofrac_rmorphism [in mathcomp.algebra.fraction]

tofrac_additive [in mathcomp.algebra.fraction]

TotalAction [in mathcomp.fingroup.action]

total_fun [in mathcomp.ssreflect.finfun]

totient [in mathcomp.ssreflect.prime]

to_dirr [in mathcomp.character.vcharacter]

to_g [in mathcomp.solvable.burnside_app]

tperm [in mathcomp.fingroup.perm]

tperm_mx [in mathcomp.algebra.matrix]

tprod [in mathcomp.character.character]

traject [in mathcomp.ssreflect.path]

transfer [in mathcomp.solvable.finmodule]

transfer_morphism [in mathcomp.solvable.finmodule]

transversal [in mathcomp.ssreflect.finset]

transversal_repr [in mathcomp.ssreflect.finset]

tree_countType [in mathcomp.ssreflect.choice]

tree_countMixin [in mathcomp.ssreflect.choice]

tree_choiceType [in mathcomp.ssreflect.choice]

tree_choiceMixin [in mathcomp.ssreflect.choice]

tree_eqType [in mathcomp.ssreflect.choice]

tree_eqMixin [in mathcomp.ssreflect.choice]

trivGfun [in mathcomp.solvable.gfunctor]

trivGfun_pgFun [in mathcomp.solvable.gfunctor]

trivGfun_gFun [in mathcomp.solvable.gfunctor]

trivGfun_igFun [in mathcomp.solvable.gfunctor]

trivial_addv [in mathcomp.algebra.vector]

trivial_mxsum [in mathcomp.algebra.mxalgebra]

trivIset [in mathcomp.ssreflect.finset]

trivm [in mathcomp.fingroup.morphism]

triv_morph [in mathcomp.fingroup.morphism]

trmx [in mathcomp.algebra.matrix]

trmx_linear [in mathcomp.algebra.matrix]

trmx_additive [in mathcomp.algebra.matrix]

trow [in mathcomp.character.character]

trowb [in mathcomp.character.character]

trowb_linear [in mathcomp.character.character]

trow_linear [in mathcomp.character.character]

trunc_log [in mathcomp.ssreflect.prime]

tsize [in mathcomp.ssreflect.tuple]

tuple [in mathcomp.ssreflect.tuple]

tuple_subFinType [in mathcomp.ssreflect.tuple]

tuple_finType [in mathcomp.ssreflect.tuple]

tuple_finMixin [in mathcomp.ssreflect.tuple]

tuple_subCountType [in mathcomp.ssreflect.tuple]

tuple_countType [in mathcomp.ssreflect.tuple]

tuple_countMixin [in mathcomp.ssreflect.tuple]

tuple_choiceType [in mathcomp.ssreflect.tuple]

tuple_choiceMixin [in mathcomp.ssreflect.tuple]

tuple_predType [in mathcomp.ssreflect.tuple]

tuple_eqType [in mathcomp.ssreflect.tuple]

tuple_eqMixin [in mathcomp.ssreflect.tuple]

tuple_subType [in mathcomp.ssreflect.tuple]

tuple_of_finfun [in mathcomp.ssreflect.finfun]

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 | (69505 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 | (1943 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 | (39748 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 | (379 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 | (3958 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 | (91 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 | (13542 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 | (480 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 | (45 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 | (134 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 | (452 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 | (1344 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 | (1014 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 | (6127 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 | (248 entries) |