| 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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
T
+T [abbreviation, in mathcomp.character.inertia]+tag [definition, in mathcomp.ssreflect.eqtype]
+TagCountType [section, in mathcomp.ssreflect.choice]
+TagCountType.I [variable, in mathcomp.ssreflect.choice]
+TagCountType.T_ [variable, in mathcomp.ssreflect.choice]
+TagEqType [section, in mathcomp.ssreflect.eqtype]
+TagEqType.I [variable, in mathcomp.ssreflect.eqtype]
+TagEqType.T_ [variable, in mathcomp.ssreflect.eqtype]
+TagFinType [section, in mathcomp.ssreflect.fintype]
+TagFinType.I [variable, in mathcomp.ssreflect.fintype]
+TagFinType.T_ [variable, in mathcomp.ssreflect.fintype]
+Tagged [definition, in mathcomp.ssreflect.eqtype]
+tagged [definition, in mathcomp.ssreflect.eqtype]
+TaggedAs [section, in mathcomp.ssreflect.eqtype]
+TaggedAs.I [variable, in mathcomp.ssreflect.eqtype]
+TaggedAs.T_ [variable, in mathcomp.ssreflect.eqtype]
+tagged_choiceMixin [lemma, in mathcomp.ssreflect.choice]
+tagged_asE [lemma, in mathcomp.ssreflect.eqtype]
+tagged_as [definition, in mathcomp.ssreflect.eqtype]
+tag_countMixin [definition, in mathcomp.ssreflect.choice]
+tag_of_pairK [lemma, in mathcomp.ssreflect.choice]
+tag_of_pair [definition, in mathcomp.ssreflect.choice]
+tag_finMixin [definition, in mathcomp.ssreflect.fintype]
+tag_enumP [lemma, in mathcomp.ssreflect.fintype]
+tag_enum [definition, in mathcomp.ssreflect.fintype]
+tag_eqE [lemma, in mathcomp.ssreflect.eqtype]
+tag_eqP [lemma, in mathcomp.ssreflect.eqtype]
+tag_eq [definition, in mathcomp.ssreflect.eqtype]
+take [definition, in mathcomp.ssreflect.seq]
+takel_cat [lemma, in mathcomp.ssreflect.seq]
+take_tupleP [lemma, in mathcomp.ssreflect.tuple]
+take_rev [lemma, in mathcomp.ssreflect.seq]
+take_nth [lemma, in mathcomp.ssreflect.seq]
+take_size_cat [lemma, in mathcomp.ssreflect.seq]
+take_cat [lemma, in mathcomp.ssreflect.seq]
+take_cons [lemma, in mathcomp.ssreflect.seq]
+take_size [lemma, in mathcomp.ssreflect.seq]
+take_oversize [lemma, in mathcomp.ssreflect.seq]
+take0 [lemma, in mathcomp.ssreflect.seq]
+tcast [definition, in mathcomp.ssreflect.tuple]
+tcastE [lemma, in mathcomp.ssreflect.tuple]
+tcastK [lemma, in mathcomp.ssreflect.tuple]
+tcastKV [lemma, in mathcomp.ssreflect.tuple]
+tcast_trans [lemma, in mathcomp.ssreflect.tuple]
+tcast_id [lemma, in mathcomp.ssreflect.tuple]
+Tensor [section, in mathcomp.character.character]
+Tensor.F [variable, in mathcomp.character.character]
+Tensor.tprod_tr [variable, in mathcomp.character.character]
+Tensor.trow_mul [variable, in mathcomp.character.character]
+term [abbreviation, in mathcomp.character.mxrepresentation]
+textbook_triangular_sum [lemma, in mathcomp.ssreflect.binomial]
+tG [abbreviation, in mathcomp.character.mxrepresentation]
+thead [definition, in mathcomp.ssreflect.tuple]
+theadE [lemma, in mathcomp.ssreflect.tuple]
+Theory [section, in mathcomp.fingroup.perm]
+Theory.T [variable, in mathcomp.fingroup.perm]
+theta [abbreviation, in mathcomp.character.inertia]
+thinmx0 [lemma, in mathcomp.algebra.matrix]
+ThirdIsomorphism [section, in mathcomp.fingroup.quotient]
+ThirdIsomorphism.G [variable, in mathcomp.fingroup.quotient]
+ThirdIsomorphism.gT [variable, in mathcomp.fingroup.quotient]
+ThirdIsomorphism.H [variable, in mathcomp.fingroup.quotient]
+ThirdIsomorphism.K [variable, in mathcomp.fingroup.quotient]
+ThirdIsomorphism.sHK [variable, in mathcomp.fingroup.quotient]
+ThirdIsomorphism.snHG [variable, in mathcomp.fingroup.quotient]
+ThirdIsomorphism.snKG [variable, in mathcomp.fingroup.quotient]
+third_isog [lemma, in mathcomp.fingroup.quotient]
+third_isom [lemma, in mathcomp.fingroup.quotient]
+Thompson_critical [lemma, in mathcomp.solvable.maximal]
+three_subgroup [lemma, in mathcomp.solvable.commutator]
+TIp1ElemP [lemma, in mathcomp.solvable.abelian]
+TI_pcoreC [lemma, in mathcomp.solvable.pgroup]
+TI_cfker_irr [lemma, in mathcomp.character.character]
+TI_Ohm1 [lemma, in mathcomp.solvable.abelian]
+TI_center_nil [lemma, in mathcomp.solvable.nilpotent]
+TI_cardMg [lemma, in mathcomp.fingroup.fingroup]
+tnth [definition, in mathcomp.ssreflect.tuple]
+tnthP [lemma, in mathcomp.ssreflect.tuple]
+tnth_mktuple [lemma, in mathcomp.ssreflect.tuple]
+tnth_ord_tuple [lemma, in mathcomp.ssreflect.tuple]
+tnth_behead [lemma, in mathcomp.ssreflect.tuple]
+tnth_map [lemma, in mathcomp.ssreflect.tuple]
+tnth_nth [lemma, in mathcomp.ssreflect.tuple]
+tnth_default [lemma, in mathcomp.ssreflect.tuple]
+tnth_fgraph [lemma, in mathcomp.ssreflect.finfun]
+tnth0 [lemma, in mathcomp.ssreflect.tuple]
+to [definition, in mathcomp.solvable.burnside_app]
+tofrac [abbreviation, in mathcomp.algebra.fraction]
+tofracB [lemma, in mathcomp.algebra.fraction]
+tofracD [lemma, in mathcomp.algebra.fraction]
+tofracM [lemma, in mathcomp.algebra.fraction]
+tofracMn [lemma, in mathcomp.algebra.fraction]
+tofracMNn [lemma, in mathcomp.algebra.fraction]
+tofracN [lemma, in mathcomp.algebra.fraction]
+tofracX [lemma, in mathcomp.algebra.fraction]
+tofrac_eq0 [lemma, in mathcomp.algebra.fraction]
+tofrac_eq [lemma, in mathcomp.algebra.fraction]
+tofrac_is_multiplicative [lemma, in mathcomp.algebra.fraction]
+tofrac_is_additive [lemma, in mathcomp.algebra.fraction]
+tofrac0 [lemma, in mathcomp.algebra.fraction]
+tofrac1 [lemma, in mathcomp.algebra.fraction]
+TotalAction [definition, in mathcomp.fingroup.action]
+TotalAction [section, in mathcomp.fingroup.action]
+TotalActions [section, in mathcomp.fingroup.action]
+TotalActions.aT [variable, in mathcomp.fingroup.action]
+TotalActions.rT [variable, in mathcomp.fingroup.action]
+TotalActions.to [variable, in mathcomp.fingroup.action]
+TotalAction.aT [variable, in mathcomp.fingroup.action]
+TotalAction.rT [variable, in mathcomp.fingroup.action]
+TotalAction.to [variable, in mathcomp.fingroup.action]
+TotalAction.toM [variable, in mathcomp.fingroup.action]
+TotalAction.to1 [variable, in mathcomp.fingroup.action]
+totient [definition, in mathcomp.ssreflect.prime]
+totientE [lemma, in mathcomp.ssreflect.prime]
+totient_count_coprime [lemma, in mathcomp.ssreflect.prime]
+totient_coprime [lemma, in mathcomp.ssreflect.prime]
+totient_pfactor [lemma, in mathcomp.ssreflect.prime]
+totient_gt0 [lemma, in mathcomp.ssreflect.prime]
+totient_gen [lemma, in mathcomp.solvable.cyclic]
+to_dirrK [lemma, in mathcomp.character.vcharacter]
+to_dirr [definition, in mathcomp.character.vcharacter]
+to_g [definition, in mathcomp.solvable.burnside_app]
+tperm [definition, in mathcomp.fingroup.perm]
+tpermC [lemma, in mathcomp.fingroup.perm]
+tpermD [lemma, in mathcomp.fingroup.perm]
+TpermFirst [constructor, in mathcomp.fingroup.perm]
+tpermJ [lemma, in mathcomp.fingroup.perm]
+tpermK [lemma, in mathcomp.fingroup.perm]
+tpermKg [lemma, in mathcomp.fingroup.perm]
+tpermL [lemma, in mathcomp.fingroup.perm]
+TpermNone [constructor, in mathcomp.fingroup.perm]
+tpermP [lemma, in mathcomp.fingroup.perm]
+tpermR [lemma, in mathcomp.fingroup.perm]
+TpermSecond [constructor, in mathcomp.fingroup.perm]
+tpermV [lemma, in mathcomp.fingroup.perm]
+tperm_spec [inductive, in mathcomp.fingroup.perm]
+tperm_proof [lemma, in mathcomp.fingroup.perm]
+tperm_mx [definition, in mathcomp.algebra.matrix]
+tperm1 [lemma, in mathcomp.fingroup.perm]
+tperm2 [lemma, in mathcomp.fingroup.perm]
+tprod [definition, in mathcomp.character.character]
+tprodE [lemma, in mathcomp.character.character]
+tprod1 [lemma, in mathcomp.character.character]
+trace_map_mx [lemma, in mathcomp.algebra.matrix]
+trace_mx11 [lemma, in mathcomp.algebra.matrix]
+traject [definition, in mathcomp.ssreflect.path]
+Trajectory [section, in mathcomp.ssreflect.path]
+Trajectory.f [variable, in mathcomp.ssreflect.path]
+Trajectory.T [variable, in mathcomp.ssreflect.path]
+trajectP [lemma, in mathcomp.ssreflect.path]
+trajectS [lemma, in mathcomp.ssreflect.path]
+trajectSr [lemma, in mathcomp.ssreflect.path]
+traject_iteri [lemma, in mathcomp.ssreflect.path]
+transfer [definition, in mathcomp.solvable.finmodule]
+Transfer [section, in mathcomp.solvable.finmodule]
+TransferEqType [section, in mathcomp.ssreflect.eqtype]
+TransferEqType.eT [variable, in mathcomp.ssreflect.eqtype]
+TransferEqType.f [variable, in mathcomp.ssreflect.eqtype]
+TransferEqType.T [variable, in mathcomp.ssreflect.eqtype]
+TransferFinType [section, in mathcomp.ssreflect.fintype]
+TransferFinType.eT [variable, in mathcomp.ssreflect.fintype]
+TransferFinType.f [variable, in mathcomp.ssreflect.fintype]
+TransferFinType.fT [variable, in mathcomp.ssreflect.fintype]
+transferM [lemma, in mathcomp.solvable.finmodule]
+transfer_cycle_expansion [lemma, in mathcomp.solvable.finmodule]
+transfer_indep [lemma, in mathcomp.solvable.finmodule]
+transfer_morph_subproof [lemma, in mathcomp.solvable.finmodule]
+Transfer.abelA [variable, in mathcomp.solvable.finmodule]
+Transfer.alpha [variable, in mathcomp.solvable.finmodule]
+Transfer.aT [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer [section, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.actsgHG [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.defHGg [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.g [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.Gg [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.HGg [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.H_g_rcosets [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.injHg [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.injHGg [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.n_ [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.partHG [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.partHGg [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.sgG [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.sXG [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.trX [variable, in mathcomp.solvable.finmodule]
+Transfer.FactorTransfer.X [variable, in mathcomp.solvable.finmodule]
+Transfer.fmalpha [variable, in mathcomp.solvable.finmodule]
+Transfer.G [variable, in mathcomp.solvable.finmodule]
+Transfer.gT [variable, in mathcomp.solvable.finmodule]
+Transfer.H [variable, in mathcomp.solvable.finmodule]
+Transfer.sHG [variable, in mathcomp.solvable.finmodule]
+Transfer.V [variable, in mathcomp.solvable.finmodule]
+transRs_rcosets [lemma, in mathcomp.fingroup.action]
+transversal [definition, in mathcomp.ssreflect.finset]
+transversalP [lemma, in mathcomp.ssreflect.finset]
+transversal_reprK [lemma, in mathcomp.ssreflect.finset]
+transversal_sub [lemma, in mathcomp.ssreflect.finset]
+transversal_repr [definition, in mathcomp.ssreflect.finset]
+trans_prim_astab [lemma, in mathcomp.solvable.primitive_action]
+trans_subnorm_fixP [lemma, in mathcomp.fingroup.action]
+tree_countMixin [definition, in mathcomp.ssreflect.choice]
+tree_choiceMixin [definition, in mathcomp.ssreflect.choice]
+tree_eqMixin [definition, in mathcomp.ssreflect.choice]
+triangular_sum [lemma, in mathcomp.ssreflect.binomial]
+trivGfun [definition, in mathcomp.solvable.gfunctor]
+trivGfun_cont [lemma, in mathcomp.solvable.gfunctor]
+trivGP [lemma, in mathcomp.fingroup.fingroup]
+trivgP [lemma, in mathcomp.fingroup.fingroup]
+trivgPn [lemma, in mathcomp.fingroup.fingroup]
+trivgVpdiv [lemma, in mathcomp.solvable.pgroup]
+trivg_pcore_quotient [lemma, in mathcomp.solvable.pgroup]
+trivg_quotient [lemma, in mathcomp.fingroup.quotient]
+trivg_acomps [lemma, in mathcomp.solvable.jordanholder]
+trivg_comps [lemma, in mathcomp.solvable.jordanholder]
+trivg_Mho [lemma, in mathcomp.solvable.abelian]
+trivg_exponent [lemma, in mathcomp.solvable.abelian]
+trivg_Fitting [lemma, in mathcomp.solvable.maximal]
+trivg_Phi [lemma, in mathcomp.solvable.maximal]
+trivg_rowg [lemma, in mathcomp.character.mxabelem]
+trivg_card1 [lemma, in mathcomp.fingroup.fingroup]
+trivg_card_le1 [lemma, in mathcomp.fingroup.fingroup]
+trivg_center_pgroup [lemma, in mathcomp.solvable.sylow]
+trivg0 [lemma, in mathcomp.fingroup.gproduct]
+TrivialMxsum [constructor, in mathcomp.algebra.mxalgebra]
+trivial_Alt_2 [lemma, in mathcomp.solvable.alt]
+trivial_fieldOver [lemma, in mathcomp.field.fieldext]
+trivial_isog [lemma, in mathcomp.fingroup.morphism]
+trivIimset [lemma, in mathcomp.ssreflect.finset]
+trivIset [definition, in mathcomp.ssreflect.finset]
+trivIsetI [lemma, in mathcomp.ssreflect.finset]
+trivIsetP [lemma, in mathcomp.ssreflect.finset]
+trivIsetS [lemma, in mathcomp.ssreflect.finset]
+trivIsetU1 [lemma, in mathcomp.ssreflect.finset]
+trivm [definition, in mathcomp.fingroup.morphism]
+trivMg [lemma, in mathcomp.fingroup.fingroup]
+TrivMorphism [section, in mathcomp.fingroup.morphism]
+TrivMorphism.aT [variable, in mathcomp.fingroup.morphism]
+TrivMorphism.rT [variable, in mathcomp.fingroup.morphism]
+trivm_morphM [lemma, in mathcomp.fingroup.morphism]
+triv_cprod [lemma, in mathcomp.fingroup.gproduct]
+triv_restr_perm [lemma, in mathcomp.fingroup.action]
+trmx [definition, in mathcomp.algebra.matrix]
+trmxK [lemma, in mathcomp.algebra.matrix]
+trmxV [lemma, in mathcomp.algebra.matrix]
+trmx_inv [lemma, in mathcomp.algebra.matrix]
+trmx_adj [lemma, in mathcomp.algebra.matrix]
+trmx_mul [lemma, in mathcomp.algebra.matrix]
+trmx_mul_rev [lemma, in mathcomp.algebra.matrix]
+trmx_delta [lemma, in mathcomp.algebra.matrix]
+trmx_drsub [lemma, in mathcomp.algebra.matrix]
+trmx_dlsub [lemma, in mathcomp.algebra.matrix]
+trmx_ursub [lemma, in mathcomp.algebra.matrix]
+trmx_ulsub [lemma, in mathcomp.algebra.matrix]
+trmx_dsub [lemma, in mathcomp.algebra.matrix]
+trmx_usub [lemma, in mathcomp.algebra.matrix]
+trmx_rsub [lemma, in mathcomp.algebra.matrix]
+trmx_lsub [lemma, in mathcomp.algebra.matrix]
+trmx_cast [lemma, in mathcomp.algebra.matrix]
+trmx_inj [lemma, in mathcomp.algebra.matrix]
+trmx_const [lemma, in mathcomp.algebra.matrix]
+trmx_key [lemma, in mathcomp.algebra.matrix]
+trmx0 [lemma, in mathcomp.algebra.matrix]
+trmx1 [lemma, in mathcomp.algebra.matrix]
+trow [definition, in mathcomp.character.character]
+trowb [definition, in mathcomp.character.character]
+trowbE [lemma, in mathcomp.character.character]
+trowb_is_linear [lemma, in mathcomp.character.character]
+trow_is_linear [lemma, in mathcomp.character.character]
+trow0 [lemma, in mathcomp.character.character]
+True [abbreviation, in mathcomp.character.mxrepresentation]
+truncCD [lemma, in mathcomp.field.algC]
+truncCK [lemma, in mathcomp.field.algC]
+truncCM [lemma, in mathcomp.field.algC]
+truncCX [lemma, in mathcomp.field.algC]
+truncC_gt0 [lemma, in mathcomp.field.algC]
+truncC_def [lemma, in mathcomp.field.algC]
+truncC_itv [lemma, in mathcomp.field.algC]
+truncC0 [lemma, in mathcomp.field.algC]
+truncC0Pn [lemma, in mathcomp.field.algC]
+truncC1 [lemma, in mathcomp.field.algC]
+trunc_log_max [lemma, in mathcomp.ssreflect.prime]
+trunc_logP [lemma, in mathcomp.ssreflect.prime]
+trunc_log_ltn [lemma, in mathcomp.ssreflect.prime]
+trunc_log_bounds [lemma, in mathcomp.ssreflect.prime]
+trunc_log [definition, in mathcomp.ssreflect.prime]
+tr_pid_mx [lemma, in mathcomp.algebra.matrix]
+tr_tperm_mx [lemma, in mathcomp.algebra.matrix]
+tr_perm_mx [lemma, in mathcomp.algebra.matrix]
+tr_scalar_mx [lemma, in mathcomp.algebra.matrix]
+tr_diag_mx [lemma, in mathcomp.algebra.matrix]
+tr_block_mx [lemma, in mathcomp.algebra.matrix]
+tr_col_mx [lemma, in mathcomp.algebra.matrix]
+tr_row_mx [lemma, in mathcomp.algebra.matrix]
+tr_col' [lemma, in mathcomp.algebra.matrix]
+tr_col [lemma, in mathcomp.algebra.matrix]
+tr_row' [lemma, in mathcomp.algebra.matrix]
+tr_row [lemma, in mathcomp.algebra.matrix]
+tr_xcol [lemma, in mathcomp.algebra.matrix]
+tr_xrow [lemma, in mathcomp.algebra.matrix]
+tr_col_perm [lemma, in mathcomp.algebra.matrix]
+tr_row_perm [lemma, in mathcomp.algebra.matrix]
+tsize [definition, in mathcomp.ssreflect.tuple]
+tuple [definition, in mathcomp.ssreflect.tuple]
+Tuple [constructor, in mathcomp.ssreflect.tuple]
+tuple [library]
+tupleE [lemma, in mathcomp.ssreflect.tuple]
+tupleP [lemma, in mathcomp.ssreflect.tuple]
+TupleQuantifiers [section, in mathcomp.ssreflect.tuple]
+TupleQuantifiers.n [variable, in mathcomp.ssreflect.tuple]
+TupleQuantifiers.T [variable, in mathcomp.ssreflect.tuple]
+tuple_perm_eqP [lemma, in mathcomp.fingroup.perm]
+tuple_map_ord [lemma, in mathcomp.ssreflect.tuple]
+tuple_countMixin [definition, in mathcomp.ssreflect.tuple]
+tuple_choiceMixin [definition, in mathcomp.ssreflect.tuple]
+tuple_eqMixin [definition, in mathcomp.ssreflect.tuple]
+tuple_eta [lemma, in mathcomp.ssreflect.tuple]
+tuple_of [record, in mathcomp.ssreflect.tuple]
+tuple0 [lemma, in mathcomp.ssreflect.tuple]
+Tuple1spec [constructor, in mathcomp.ssreflect.tuple]
+tuple1_spec [inductive, in mathcomp.ssreflect.tuple]
+tval [projection, in mathcomp.ssreflect.tuple]
+tvalK [lemma, in mathcomp.ssreflect.tuple]
+type [abbreviation, in mathcomp.field.finfield]
+T' [abbreviation, in mathcomp.solvable.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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +