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

## T (lemma)

tagged_asE [in eqtype]tag_eqP [in eqtype]

tag_eqE [in eqtype]

tag_of_pairK [in choice]

tag_enumP [in fintype]

takel_cat [in seq]

take_cons [in seq]

take_tupleP [in tuple]

take_size_cat [in seq]

take_cat [in seq]

take_nth [in seq]

take_size [in seq]

take_oversize [in seq]

take0 [in seq]

textbook_triangular_sum [in binomial]

theadE [in tuple]

thinmx0 [in matrix]

third_isog [in quotient]

third_isom [in quotient]

Thompson_critical [in maximal]

three_subgroup [in commutator]

TIconjP [in frobenius]

TIconj_SN_P [in frobenius]

TIp1ElemP [in abelian]

TI_cardMg [in fingroup]

TI_center_nil [in nilpotent]

TI_Ohm1 [in abelian]

TI_pcoreC [in pgroup]

tnth_default [in tuple]

tnth_map [in tuple]

tnth_ord_tuple [in tuple]

tnth_behead [in tuple]

tnth_fgraph [in finfun]

tnth_nth [in tuple]

tnth0 [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]

tperm_proof [in perm]

tperm1 [in perm]

tperm2 [in perm]

trace_map_mx [in matrix]

trace_mx11 [in matrix]

trajectP [in path]

trajectS [in path]

trajectSr [in path]

traject_iteri [in path]

transferM [in finmodule]

transfer_morph_subproof [in finmodule]

transfer_pcycle_def [in finmodule]

transfer_indep [in finmodule]

transRs_rcosets [in action]

trans_subnorm_fixP [in action]

trans_prim_astab [in primitive_action]

triangular_sum [in binomial]

trivGfun_cont [in gfunctor]

trivGP [in fingroup]

trivgP [in fingroup]

trivgPn [in fingroup]

trivgVpdiv [in pgroup]

trivg_center_pgroup [in sylow]

trivg_Phi [in maximal]

trivg_Mho [in abelian]

trivg_card_le1 [in fingroup]

trivg_card1 [in fingroup]

trivg_exponent [in abelian]

trivg_comps [in jordanholder]

trivg_acomps [in jordanholder]

trivg_Fitting [in maximal]

trivg_pcore_quotient [in pgroup]

trivg_quotient [in quotient]

trivg_rowg [in mxabelem]

trivg0 [in gproduct]

trivial_isog [in morphism]

trivial_Alt_2 [in alt]

trivIimset [in finset]

trivIsetI [in finset]

trivIsetP [in finset]

trivIsetU1 [in finset]

trivMg [in fingroup]

trivm_morphM [in morphism]

triv_cprod [in gproduct]

triv_restr_perm [in action]

trmxK [in matrix]

trmxV [in matrix]

trmx_cast [in matrix]

trmx_dlsub [in matrix]

trmx_delta [in matrix]

trmx_mul_rev [in matrix]

trmx_mul [in matrix]

trmx_const [in matrix]

trmx_drsub [in matrix]

trmx_inv [in matrix]

trmx_adj [in matrix]

trmx_inj [in matrix]

trmx_ulsub [in matrix]

trmx_usub [in matrix]

trmx_dsub [in matrix]

trmx_lsub [in matrix]

trmx_rsub [in matrix]

trmx_ursub [in matrix]

trmx0 [in matrix]

trmx1 [in matrix]

tr_pid_mx [in matrix]

tr_col_perm [in matrix]

tr_block_mx [in matrix]

tr_scalar_mx [in matrix]

tr_col' [in matrix]

tr_row [in matrix]

tr_xrow [in matrix]

tr_diag_mx [in matrix]

tr_row' [in matrix]

tr_col_mx [in matrix]

tr_row_mx [in matrix]

tr_xcol [in matrix]

tr_row_perm [in matrix]

tr_tperm_mx [in matrix]

tr_col [in matrix]

tr_perm_mx [in matrix]

tupleE [in tuple]

tupleP [in tuple]

tuple_eta [in tuple]

tuple_map_ord [in tuple]

tuple_of_evK [in vector]

tuple0 [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 | _ | 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) |