| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -
T
-T [abbreviation, in mathcomp.character.inertia]-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]
-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_tfgraph [lemma, in mathcomp.ssreflect.finfun]
-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_subseq [lemma, in mathcomp.ssreflect.seq]
-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]
-tally [definition, in mathcomp.ssreflect.seq]
-tallyE [lemma, in mathcomp.ssreflect.seq]
-tallyEl [lemma, in mathcomp.ssreflect.seq]
-tallyK [lemma, in mathcomp.ssreflect.seq]
-tallyP [lemma, in mathcomp.ssreflect.seq]
-tally_seqK [lemma, in mathcomp.ssreflect.seq]
-tally_seq [definition, 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]
-tfgraph [definition, in mathcomp.ssreflect.finfun]
-tfgraphK [lemma, in mathcomp.ssreflect.finfun]
-tfgraph_inj [lemma, in mathcomp.ssreflect.finfun]
-tfgraph_inv [definition, in mathcomp.ssreflect.finfun]
-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]
-total_fun [definition, in mathcomp.ssreflect.finfun]
-total_homo_mono [lemma, in mathcomp.ssreflect.eqtype]
-total_homo_mono_in [lemma, in mathcomp.ssreflect.eqtype]
-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]
-tseq [abbreviation, in mathcomp.ssreflect.seq]
-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 [abbreviation, in mathcomp.fingroup.perm]
-tuple_permP [lemma, in mathcomp.fingroup.perm]
-tuple_map_ord [lemma, in mathcomp.ssreflect.tuple]
-tuple_finMixin [definition, 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -