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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |

## T (lemma)

tagged_asE [in eqtype]tag_enumP [in fintype]

tag_eqE [in eqtype]

tag_eqP [in eqtype]

tag_of_pairK [in choice]

tag_of_sumK [in choice]

tag_pickleK [in choice]

takel_cat [in seq]

take0 [in seq]

take_cat [in seq]

take_cons [in seq]

take_nth [in seq]

take_oversize [in seq]

take_size [in seq]

take_size_cat [in seq]

take_tupleP [in tuple]

theadE [in tuple]

third_isog [in normal]

third_isom [in normal]

TI_cardMg [in groups]

tnth0 [in tuple]

tnth_behead [in tuple]

tnth_default [in tuple]

tnth_fgraph [in finfun]

tnth_map [in tuple]

tnth_nth [in tuple]

topredE [in ssrbool]

tpermC [in perm]

tpermD [in perm]

tpermJ [in perm]

tpermK [in perm]

tpermKg [in perm]

tpermL [in perm]

tpermP [in perm]

tpermR [in perm]

tpermV [in perm]

tperm1 [in perm]

tperm2 [in perm]

tperm_proof [in perm]

trajectP [in paths]

trivGP [in groups]

trivgP [in groups]

trivgPn [in groups]

trivg_card1 [in groups]

trivg_card_le1 [in groups]

trivg_char [in automorphism]

trivg_quotient [in normal]

trivial_isog [in morphisms]

trivIsetI [in finset]

trivIsetP [in finset]

trivMg [in groups]

trivm_morphM [in morphisms]

trmxK [in matrix]

trmx0 [in matrix]

trmx_add [in matrix]

trmx_adj [in matrix]

trmx_block [in matrix]

trmx_col [in matrix]

trmx_col' [in matrix]

trmx_cswap [in matrix]

trmx_inj [in matrix]

trmx_inv [in matrix]

trmx_llsub [in matrix]

trmx_lrsub [in matrix]

trmx_mul [in matrix]

trmx_mul_rev [in matrix]

trmx_perm [in matrix]

trmx_row [in matrix]

trmx_row' [in matrix]

trmx_rswap [in matrix]

trmx_scalar [in matrix]

trmx_scale [in matrix]

trmx_tperm [in matrix]

trmx_ulsub [in matrix]

trmx_unit [in matrix]

trmx_ursub [in matrix]

tupleE [in tuple]

tupleP [in tuple]

tuple0 [in tuple]

tuple_eta [in tuple]

tuple_map_ord [in tuple]

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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |