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

tag [definition, in eqtype]TagEqType [section, in eqtype]

TagEqType.I [variable, in eqtype]

TagEqType.T_ [variable, in eqtype]

TagFinType [section, in fintype]

TagFinType.I [variable, in fintype]

TagFinType.T_ [variable, in fintype]

tagged [definition, in eqtype]

Tagged [definition, in eqtype]

TaggedAs [section, in eqtype]

TaggedAs.I [variable, in eqtype]

TaggedAs.T_ [variable, in eqtype]

tagged_asE [lemma, in eqtype]

tagged_as [definition, in eqtype]

TagSeq [section, in choice]

TagSeq.I [variable, in choice]

TagSeq.T_ [variable, in choice]

tag_count_of_seq [definition, in choice]

tag_choiceMixin [definition, in choice]

tag_of_pair [definition, in choice]

tag_finType [definition, in fintype]

tag_eqP [lemma, in eqtype]

tag_eqE [lemma, in eqtype]

tag_of_pairK [lemma, in choice]

tag_eqType [definition, in eqtype]

tag_eqMixin [definition, in eqtype]

tag_finMixin [definition, in fintype]

tag_eq [definition, in eqtype]

tag_countMixin [definition, in choice]

tag_countType [definition, in choice]

tag_choiceType [definition, in choice]

tag_enum [definition, in fintype]

tag_enumP [lemma, in fintype]

take [definition, in seq]

takel_cat [lemma, in seq]

take_tuple [definition, in tuple]

take_cons [lemma, in seq]

take_tupleP [lemma, in tuple]

take_size_cat [lemma, in seq]

take_cat [lemma, in seq]

take_nth [lemma, in seq]

take_size [lemma, in seq]

take_oversize [lemma, in seq]

take0 [lemma, in seq]

term [abbreviation, in mxrepresentation]

textbook_triangular_sum [lemma, in binomial]

tG [abbreviation, in mxrepresentation]

thead [definition, in tuple]

theadE [lemma, in tuple]

TheCanonical [module, in ssreflect]

TheCanonical.get [definition, in ssreflect]

TheCanonical.get_by [definition, in ssreflect]

TheCanonical.put [inductive, in ssreflect]

TheCanonical.Put [constructor, in ssreflect]

Theory [module, in ssralg]

Theory [module, in finalg]

Theory [section, in perm]

Theory [module, in bigop]

Theory.T [variable, in perm]

thinmx0 [lemma, in matrix]

ThirdIsomorphism [section, in quotient]

ThirdIsomorphism.G [variable, in quotient]

ThirdIsomorphism.gT [variable, in quotient]

ThirdIsomorphism.H [variable, in quotient]

ThirdIsomorphism.K [variable, in quotient]

ThirdIsomorphism.sHK [variable, in quotient]

ThirdIsomorphism.snHG [variable, in quotient]

ThirdIsomorphism.snKG [variable, in quotient]

third_isog [lemma, in quotient]

third_isom [lemma, in quotient]

Thompson_critical [lemma, in maximal]

three_subgroup [lemma, in commutator]

TIconjP [lemma, in frobenius]

TIconj_SN_P [lemma, in frobenius]

TIp1ElemP [lemma, in abelian]

TIsum [definition, in vector]

TIsum [definition, in mxalgebra]

TI_cardMg [lemma, in fingroup]

TI_center_nil [lemma, in nilpotent]

TI_Ohm1 [lemma, in abelian]

TI_pcoreC [lemma, in pgroup]

tnth [definition, in tuple]

tnth_default [lemma, in tuple]

tnth_map [lemma, in tuple]

tnth_ord_tuple [lemma, in tuple]

tnth_behead [lemma, in tuple]

tnth_fgraph [lemma, in finfun]

tnth_nth [lemma, in tuple]

tnth0 [lemma, in tuple]

topred [projection, in ssrbool]

topredE [lemma, in ssrbool]

total [definition, in ssrbool]

TotalAction [section, in action]

TotalAction [definition, in action]

TotalActions [section, in action]

TotalActions.aT [variable, in action]

TotalActions.rT [variable, in action]

TotalActions.to [variable, in action]

TotalAction.aT [variable, in action]

TotalAction.rT [variable, in action]

TotalAction.to [variable, in action]

TotalAction.toM [variable, in action]

TotalAction.to1 [variable, in action]

tperm [definition, in perm]

tpermC [lemma, in perm]

tpermD [lemma, in perm]

TpermFirst [constructor, in perm]

tpermJ [lemma, in perm]

tpermK [lemma, in perm]

tpermKg [lemma, in perm]

tpermL [lemma, in perm]

TpermNone [constructor, in perm]

tpermP [lemma, in perm]

tpermR [lemma, in perm]

TpermSecond [constructor, in perm]

tpermV [lemma, in perm]

tperm_spec [inductive, in perm]

tperm_proof [lemma, in perm]

tperm_mx [definition, in matrix]

tperm1 [lemma, in perm]

tperm2 [lemma, in perm]

trace_map_mx [lemma, in matrix]

trace_mx11 [lemma, in matrix]

traject [definition, in path]

Trajectory [section, in path]

Trajectory.f [variable, in path]

Trajectory.T [variable, in path]

trajectP [lemma, in path]

trajectS [lemma, in path]

trajectSr [lemma, in path]

traject_iteri [lemma, in path]

transfer [definition, in finmodule]

Transfer [section, in finmodule]

TransferEqType [section, in eqtype]

TransferEqType.eT [variable, in eqtype]

TransferEqType.f [variable, in eqtype]

TransferEqType.T [variable, in eqtype]

TransferFinType [section, in fintype]

TransferFinType.eT [variable, in fintype]

TransferFinType.f [variable, in fintype]

TransferFinType.fT [variable, in fintype]

transferM [lemma, in finmodule]

transfer_morph_subproof [lemma, in finmodule]

transfer_morphism [definition, in finmodule]

transfer_pcycle_def [lemma, in finmodule]

transfer_indep [lemma, in finmodule]

Transfer.abelA [variable, in finmodule]

Transfer.alpha [variable, in finmodule]

Transfer.aT [variable, in finmodule]

Transfer.FactorTransfer [section, in finmodule]

Transfer.FactorTransfer.g [variable, in finmodule]

Transfer.FactorTransfer.Gg [variable, in finmodule]

Transfer.FactorTransfer.trX [variable, in finmodule]

Transfer.FactorTransfer.X [variable, in finmodule]

Transfer.G [variable, in finmodule]

Transfer.gT [variable, in finmodule]

Transfer.H [variable, in finmodule]

Transfer.sHG [variable, in finmodule]

transitive [definition, in ssrbool]

transRs_rcosets [lemma, in action]

trans_subnorm_fixP [lemma, in action]

trans_prim_astab [lemma, in primitive_action]

triangular_sum [lemma, in binomial]

trivGfun [definition, in gfunctor]

trivGfun_cont [lemma, in gfunctor]

trivGfun_pgFun [definition, in gfunctor]

trivGfun_gFun [definition, in gfunctor]

trivGfun_igFun [definition, in gfunctor]

trivGP [lemma, in fingroup]

trivgP [lemma, in fingroup]

trivgPn [lemma, in fingroup]

trivgVpdiv [lemma, in pgroup]

trivg_center_pgroup [lemma, in sylow]

trivg_Phi [lemma, in maximal]

trivg_Mho [lemma, in abelian]

trivg_card_le1 [lemma, in fingroup]

trivg_card1 [lemma, in fingroup]

trivg_exponent [lemma, in abelian]

trivg_comps [lemma, in jordanholder]

trivg_acomps [lemma, in jordanholder]

trivg_Fitting [lemma, in maximal]

trivg_pcore_quotient [lemma, in pgroup]

trivg_quotient [lemma, in quotient]

trivg_rowg [lemma, in mxabelem]

trivg0 [lemma, in gproduct]

TrivialMxsum [constructor, in mxalgebra]

TrivialSumv [constructor, in vector]

trivial_isog [lemma, in morphism]

trivial_Alt_2 [lemma, in alt]

trivial_mxsum [definition, in mxalgebra]

trivial_addv [definition, in vector]

trivIimset [lemma, in finset]

trivIset [definition, in finset]

trivIsetI [lemma, in finset]

trivIsetP [lemma, in finset]

trivIsetU1 [lemma, in finset]

trivm [definition, in morphism]

trivMg [lemma, in fingroup]

TrivMorphism [section, in morphism]

TrivMorphism.aT [variable, in morphism]

TrivMorphism.rT [variable, in morphism]

trivm_morphM [lemma, in morphism]

triv_morph [definition, in morphism]

triv_cprod [lemma, in gproduct]

triv_restr_perm [lemma, in action]

trmx [definition, in matrix]

trmxK [lemma, in matrix]

trmxV [lemma, in matrix]

trmx_cast [lemma, in matrix]

trmx_dlsub [lemma, in matrix]

trmx_delta [lemma, in matrix]

trmx_mul_rev [lemma, in matrix]

trmx_mul [lemma, in matrix]

trmx_const [lemma, in matrix]

trmx_drsub [lemma, in matrix]

trmx_inv [lemma, in matrix]

trmx_adj [lemma, in matrix]

trmx_inj [lemma, in matrix]

trmx_ulsub [lemma, in matrix]

trmx_usub [lemma, in matrix]

trmx_dsub [lemma, in matrix]

trmx_lsub [lemma, in matrix]

trmx_linear [definition, in matrix]

trmx_additive [definition, in matrix]

trmx_rsub [lemma, in matrix]

trmx_ursub [lemma, in matrix]

trmx0 [lemma, in matrix]

trmx1 [lemma, in matrix]

True [abbreviation, in mxrepresentation]

tr_pid_mx [lemma, in matrix]

tr_col_perm [lemma, in matrix]

tr_block_mx [lemma, in matrix]

tr_scalar_mx [lemma, in matrix]

tr_col' [lemma, in matrix]

tr_row [lemma, in matrix]

tr_xrow [lemma, in matrix]

tr_diag_mx [lemma, in matrix]

tr_row' [lemma, in matrix]

tr_col_mx [lemma, in matrix]

tr_row_mx [lemma, in matrix]

tr_xcol [lemma, in matrix]

tr_row_perm [lemma, in matrix]

tr_tperm_mx [lemma, in matrix]

tr_col [lemma, in matrix]

tr_perm_mx [lemma, in matrix]

tsize [definition, in tuple]

tT [abbreviation, in tuple]

tT [abbreviation, in tuple]

Tuple [constructor, in tuple]

tuple [definition, in tuple]

tuple [library]

tupleE [lemma, in tuple]

tupleP [lemma, in tuple]

tuple_subFinType [definition, in tuple]

tuple_finType [definition, in tuple]

tuple_finMixin [definition, in tuple]

tuple_subCountType [definition, in tuple]

tuple_countType [definition, in tuple]

tuple_choiceType [definition, in tuple]

tuple_predType [definition, in tuple]

tuple_eqType [definition, in tuple]

tuple_subType [definition, in tuple]

tuple_choiceMixin [definition, in tuple]

tuple_eqMixin [definition, in tuple]

tuple_eta [lemma, in tuple]

tuple_countMixin [definition, in tuple]

tuple_map_ord [lemma, in tuple]

tuple_of_ev [definition, in vector]

tuple_of [record, in tuple]

tuple_of_evK [lemma, in vector]

tuple0 [lemma, in tuple]

Tuple1spec [constructor, in tuple]

tuple1_spec [inductive, in tuple]

tval [projection, in tuple]

T' [abbreviation, in alt]

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