| 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 (lemma)
-tagged_choiceMixin [in mathcomp.ssreflect.choice]-tagged_tfgraph [in mathcomp.ssreflect.finfun]
-tagged_asE [in mathcomp.ssreflect.eqtype]
-tag_of_pairK [in mathcomp.ssreflect.choice]
-tag_enumP [in mathcomp.ssreflect.fintype]
-tag_eqE [in mathcomp.ssreflect.eqtype]
-tag_eqP [in mathcomp.ssreflect.eqtype]
-takel_cat [in mathcomp.ssreflect.seq]
-take_tupleP [in mathcomp.ssreflect.tuple]
-take_subseq [in mathcomp.ssreflect.seq]
-take_rev [in mathcomp.ssreflect.seq]
-take_nth [in mathcomp.ssreflect.seq]
-take_size_cat [in mathcomp.ssreflect.seq]
-take_cat [in mathcomp.ssreflect.seq]
-take_cons [in mathcomp.ssreflect.seq]
-take_size [in mathcomp.ssreflect.seq]
-take_oversize [in mathcomp.ssreflect.seq]
-take0 [in mathcomp.ssreflect.seq]
-tallyE [in mathcomp.ssreflect.seq]
-tallyEl [in mathcomp.ssreflect.seq]
-tallyK [in mathcomp.ssreflect.seq]
-tallyP [in mathcomp.ssreflect.seq]
-tally_seqK [in mathcomp.ssreflect.seq]
-tcastE [in mathcomp.ssreflect.tuple]
-tcastK [in mathcomp.ssreflect.tuple]
-tcastKV [in mathcomp.ssreflect.tuple]
-tcast_trans [in mathcomp.ssreflect.tuple]
-tcast_id [in mathcomp.ssreflect.tuple]
-textbook_triangular_sum [in mathcomp.ssreflect.binomial]
-tfgraphK [in mathcomp.ssreflect.finfun]
-tfgraph_inj [in mathcomp.ssreflect.finfun]
-theadE [in mathcomp.ssreflect.tuple]
-thinmx0 [in mathcomp.algebra.matrix]
-third_isog [in mathcomp.fingroup.quotient]
-third_isom [in mathcomp.fingroup.quotient]
-Thompson_critical [in mathcomp.solvable.maximal]
-three_subgroup [in mathcomp.solvable.commutator]
-TIp1ElemP [in mathcomp.solvable.abelian]
-TI_pcoreC [in mathcomp.solvable.pgroup]
-TI_cfker_irr [in mathcomp.character.character]
-TI_Ohm1 [in mathcomp.solvable.abelian]
-TI_center_nil [in mathcomp.solvable.nilpotent]
-TI_cardMg [in mathcomp.fingroup.fingroup]
-tnthP [in mathcomp.ssreflect.tuple]
-tnth_mktuple [in mathcomp.ssreflect.tuple]
-tnth_ord_tuple [in mathcomp.ssreflect.tuple]
-tnth_behead [in mathcomp.ssreflect.tuple]
-tnth_map [in mathcomp.ssreflect.tuple]
-tnth_nth [in mathcomp.ssreflect.tuple]
-tnth_default [in mathcomp.ssreflect.tuple]
-tnth_fgraph [in mathcomp.ssreflect.finfun]
-tnth0 [in mathcomp.ssreflect.tuple]
-tofracB [in mathcomp.algebra.fraction]
-tofracD [in mathcomp.algebra.fraction]
-tofracM [in mathcomp.algebra.fraction]
-tofracMn [in mathcomp.algebra.fraction]
-tofracMNn [in mathcomp.algebra.fraction]
-tofracN [in mathcomp.algebra.fraction]
-tofracX [in mathcomp.algebra.fraction]
-tofrac_eq0 [in mathcomp.algebra.fraction]
-tofrac_eq [in mathcomp.algebra.fraction]
-tofrac_is_multiplicative [in mathcomp.algebra.fraction]
-tofrac_is_additive [in mathcomp.algebra.fraction]
-tofrac0 [in mathcomp.algebra.fraction]
-tofrac1 [in mathcomp.algebra.fraction]
-total_homo_mono [in mathcomp.ssreflect.eqtype]
-total_homo_mono_in [in mathcomp.ssreflect.eqtype]
-totientE [in mathcomp.ssreflect.prime]
-totient_count_coprime [in mathcomp.ssreflect.prime]
-totient_coprime [in mathcomp.ssreflect.prime]
-totient_pfactor [in mathcomp.ssreflect.prime]
-totient_gt0 [in mathcomp.ssreflect.prime]
-totient_gen [in mathcomp.solvable.cyclic]
-to_dirrK [in mathcomp.character.vcharacter]
-tpermC [in mathcomp.fingroup.perm]
-tpermD [in mathcomp.fingroup.perm]
-tpermJ [in mathcomp.fingroup.perm]
-tpermK [in mathcomp.fingroup.perm]
-tpermKg [in mathcomp.fingroup.perm]
-tpermL [in mathcomp.fingroup.perm]
-tpermP [in mathcomp.fingroup.perm]
-tpermR [in mathcomp.fingroup.perm]
-tpermV [in mathcomp.fingroup.perm]
-tperm_proof [in mathcomp.fingroup.perm]
-tperm1 [in mathcomp.fingroup.perm]
-tperm2 [in mathcomp.fingroup.perm]
-tprodE [in mathcomp.character.character]
-tprod1 [in mathcomp.character.character]
-trace_map_mx [in mathcomp.algebra.matrix]
-trace_mx11 [in mathcomp.algebra.matrix]
-trajectP [in mathcomp.ssreflect.path]
-trajectS [in mathcomp.ssreflect.path]
-trajectSr [in mathcomp.ssreflect.path]
-traject_iteri [in mathcomp.ssreflect.path]
-transferM [in mathcomp.solvable.finmodule]
-transfer_cycle_expansion [in mathcomp.solvable.finmodule]
-transfer_indep [in mathcomp.solvable.finmodule]
-transfer_morph_subproof [in mathcomp.solvable.finmodule]
-transRs_rcosets [in mathcomp.fingroup.action]
-transversalP [in mathcomp.ssreflect.finset]
-transversal_reprK [in mathcomp.ssreflect.finset]
-transversal_sub [in mathcomp.ssreflect.finset]
-trans_prim_astab [in mathcomp.solvable.primitive_action]
-trans_subnorm_fixP [in mathcomp.fingroup.action]
-triangular_sum [in mathcomp.ssreflect.binomial]
-trivGfun_cont [in mathcomp.solvable.gfunctor]
-trivGP [in mathcomp.fingroup.fingroup]
-trivgP [in mathcomp.fingroup.fingroup]
-trivgPn [in mathcomp.fingroup.fingroup]
-trivgVpdiv [in mathcomp.solvable.pgroup]
-trivg_pcore_quotient [in mathcomp.solvable.pgroup]
-trivg_quotient [in mathcomp.fingroup.quotient]
-trivg_acomps [in mathcomp.solvable.jordanholder]
-trivg_comps [in mathcomp.solvable.jordanholder]
-trivg_Mho [in mathcomp.solvable.abelian]
-trivg_exponent [in mathcomp.solvable.abelian]
-trivg_Fitting [in mathcomp.solvable.maximal]
-trivg_Phi [in mathcomp.solvable.maximal]
-trivg_rowg [in mathcomp.character.mxabelem]
-trivg_card1 [in mathcomp.fingroup.fingroup]
-trivg_card_le1 [in mathcomp.fingroup.fingroup]
-trivg_center_pgroup [in mathcomp.solvable.sylow]
-trivg0 [in mathcomp.fingroup.gproduct]
-trivial_Alt_2 [in mathcomp.solvable.alt]
-trivial_fieldOver [in mathcomp.field.fieldext]
-trivial_isog [in mathcomp.fingroup.morphism]
-trivIimset [in mathcomp.ssreflect.finset]
-trivIsetI [in mathcomp.ssreflect.finset]
-trivIsetP [in mathcomp.ssreflect.finset]
-trivIsetS [in mathcomp.ssreflect.finset]
-trivIsetU1 [in mathcomp.ssreflect.finset]
-trivMg [in mathcomp.fingroup.fingroup]
-trivm_morphM [in mathcomp.fingroup.morphism]
-triv_cprod [in mathcomp.fingroup.gproduct]
-triv_restr_perm [in mathcomp.fingroup.action]
-trmxK [in mathcomp.algebra.matrix]
-trmxV [in mathcomp.algebra.matrix]
-trmx_inv [in mathcomp.algebra.matrix]
-trmx_adj [in mathcomp.algebra.matrix]
-trmx_mul [in mathcomp.algebra.matrix]
-trmx_mul_rev [in mathcomp.algebra.matrix]
-trmx_delta [in mathcomp.algebra.matrix]
-trmx_drsub [in mathcomp.algebra.matrix]
-trmx_dlsub [in mathcomp.algebra.matrix]
-trmx_ursub [in mathcomp.algebra.matrix]
-trmx_ulsub [in mathcomp.algebra.matrix]
-trmx_dsub [in mathcomp.algebra.matrix]
-trmx_usub [in mathcomp.algebra.matrix]
-trmx_rsub [in mathcomp.algebra.matrix]
-trmx_lsub [in mathcomp.algebra.matrix]
-trmx_cast [in mathcomp.algebra.matrix]
-trmx_inj [in mathcomp.algebra.matrix]
-trmx_const [in mathcomp.algebra.matrix]
-trmx_key [in mathcomp.algebra.matrix]
-trmx0 [in mathcomp.algebra.matrix]
-trmx1 [in mathcomp.algebra.matrix]
-trowbE [in mathcomp.character.character]
-trowb_is_linear [in mathcomp.character.character]
-trow_is_linear [in mathcomp.character.character]
-trow0 [in mathcomp.character.character]
-truncCD [in mathcomp.field.algC]
-truncCK [in mathcomp.field.algC]
-truncCM [in mathcomp.field.algC]
-truncCX [in mathcomp.field.algC]
-truncC_gt0 [in mathcomp.field.algC]
-truncC_def [in mathcomp.field.algC]
-truncC_itv [in mathcomp.field.algC]
-truncC0 [in mathcomp.field.algC]
-truncC0Pn [in mathcomp.field.algC]
-truncC1 [in mathcomp.field.algC]
-trunc_log_max [in mathcomp.ssreflect.prime]
-trunc_logP [in mathcomp.ssreflect.prime]
-trunc_log_ltn [in mathcomp.ssreflect.prime]
-trunc_log_bounds [in mathcomp.ssreflect.prime]
-tr_pid_mx [in mathcomp.algebra.matrix]
-tr_tperm_mx [in mathcomp.algebra.matrix]
-tr_perm_mx [in mathcomp.algebra.matrix]
-tr_scalar_mx [in mathcomp.algebra.matrix]
-tr_diag_mx [in mathcomp.algebra.matrix]
-tr_block_mx [in mathcomp.algebra.matrix]
-tr_col_mx [in mathcomp.algebra.matrix]
-tr_row_mx [in mathcomp.algebra.matrix]
-tr_col' [in mathcomp.algebra.matrix]
-tr_col [in mathcomp.algebra.matrix]
-tr_row' [in mathcomp.algebra.matrix]
-tr_row [in mathcomp.algebra.matrix]
-tr_xcol [in mathcomp.algebra.matrix]
-tr_xrow [in mathcomp.algebra.matrix]
-tr_col_perm [in mathcomp.algebra.matrix]
-tr_row_perm [in mathcomp.algebra.matrix]
-tupleE [in mathcomp.ssreflect.tuple]
-tupleP [in mathcomp.ssreflect.tuple]
-tuple_permP [in mathcomp.fingroup.perm]
-tuple_map_ord [in mathcomp.ssreflect.tuple]
-tuple_eta [in mathcomp.ssreflect.tuple]
-tuple0 [in mathcomp.ssreflect.tuple]
-tvalK [in mathcomp.ssreflect.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 | -(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) | -