T (Global Index)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
T
T [abbrev, in mathcomp.group_representation.inertia]T [abbrev, in mathcomp.boot.eqtype]
T' [abbrev, in mathcomp.solvable.alt]
tact [def, in mathcomp.finite_group.perm]
tact1 [prf, in mathcomp.finite_group.perm]
tact_lift0 [prf, in mathcomp.finite_group.perm]
tactE [prf, in mathcomp.finite_group.perm]
tactK [prf, in mathcomp.finite_group.perm]
tactM [prf, in mathcomp.finite_group.perm]
tactP [prf, in mathcomp.finite_group.perm]
tag_enum [def, in mathcomp.boot.fintype]
tag_enumP [prf, in mathcomp.boot.fintype]
tag_eq [def, in mathcomp.boot.eqtype]
tag_eqE [prf, in mathcomp.boot.eqtype]
tag_eqP [prf, in mathcomp.boot.eqtype]
tag_fprod_fun [prf, in mathcomp.boot.finfun]
tag_of_pair [def, in mathcomp.boot.choice]
tag_of_pairK [prf, in mathcomp.boot.choice]
tag_with [def, in mathcomp.boot.eqtype]
tag_with_bij [prf, in mathcomp.boot.eqtype]
tag_withK [prf, in mathcomp.boot.eqtype]
tagged_as [def, in mathcomp.boot.eqtype]
tagged_asE [prf, in mathcomp.boot.eqtype]
tagged_hasChoice [prf, in mathcomp.boot.choice]
tagged_tfgraph [prf, in mathcomp.boot.finfun]
tagged_tuple_bseq [def, in mathcomp.boot.tuple]
tagged_tuple_bseq_bij [prf, in mathcomp.boot.tuple]
tagged_tuple_bseqK [prf, in mathcomp.boot.tuple]
tagged_with [def, in mathcomp.boot.eqtype]
taggedK [prf, in mathcomp.boot.ssrfun]
tagnat [mod, in mathcomp.order.order]
tagnat.card [prf, in mathcomp.order.order]
tagnat.eq_Rank [prf, in mathcomp.order.order]
tagnat.eqRank [prf, in mathcomp.order.order]
tagnat.le_Rank [prf, in mathcomp.order.order]
tagnat.le_rank [prf, in mathcomp.order.order]
tagnat.le_sig [prf, in mathcomp.order.order]
tagnat.le_sig1 [prf, in mathcomp.order.order]
tagnat.lt_Rank [prf, in mathcomp.order.order]
tagnat.lt_rank [prf, in mathcomp.order.order]
tagnat.lt_sig [prf, in mathcomp.order.order]
tagnat.ordsum [abbrev, in mathcomp.order.order]
tagnat.Rank [def, in mathcomp.order.order]
tagnat.rank [def, in mathcomp.order.order]
tagnat.Rank1K [prf, in mathcomp.order.order]
tagnat.Rank2K [prf, in mathcomp.order.order]
tagnat.rank_bij [prf, in mathcomp.order.order]
tagnat.rank_bij_on [prf, in mathcomp.order.order]
tagnat.rank_inj [prf, in mathcomp.order.order]
tagnat.rankE [prf, in mathcomp.order.order]
tagnat.RankEsum [prf, in mathcomp.order.order]
tagnat.rankEsum [prf, in mathcomp.order.order]
tagnat.rankK [prf, in mathcomp.order.order]
tagnat.rect [prf, in mathcomp.order.order]
tagnat.sig [def, in mathcomp.order.order]
tagnat.sig1 [def, in mathcomp.order.order]
tagnat.sig2 [def, in mathcomp.order.order]
tagnat.sig2K [prf, in mathcomp.order.order]
tagnat.sig_bij [prf, in mathcomp.order.order]
tagnat.sig_bij_on [prf, in mathcomp.order.order]
tagnat.sig_inj [prf, in mathcomp.order.order]
tagnat.sigE12 [prf, in mathcomp.order.order]
tagnat.sigK [prf, in mathcomp.order.order]
tagnat.T [abbrev, in mathcomp.order.order]
take [def, in mathcomp.boot.seq]
take0 [prf, in mathcomp.boot.seq]
take_bseq [def, in mathcomp.boot.tuple]
take_bseqP [prf, in mathcomp.boot.tuple]
take_cat [prf, in mathcomp.boot.seq]
take_cons [prf, in mathcomp.boot.seq]
take_drop [prf, in mathcomp.boot.seq]
take_iota [prf, in mathcomp.boot.seq]
take_min [prf, in mathcomp.boot.seq]
take_mkseq [prf, in mathcomp.boot.seq]
take_nseq [prf, in mathcomp.boot.seq]
take_nth [prf, in mathcomp.boot.seq]
take_oversize [prf, in mathcomp.boot.seq]
take_path [prf, in mathcomp.boot.path]
take_pivot [prf, in mathcomp.boot.seq]
take_poly [def, in mathcomp.algebra.poly]
take_poly0l [prf, in mathcomp.algebra.poly]
take_poly0r [prf, in mathcomp.algebra.poly]
take_poly_id [prf, in mathcomp.algebra.poly]
take_poly_is_linear [prf, in mathcomp.algebra.poly]
take_poly_sum [prf, in mathcomp.algebra.poly]
take_polyD [prf, in mathcomp.algebra.poly]
take_polyDMXn [prf, in mathcomp.algebra.poly]
take_polyMXn [prf, in mathcomp.algebra.poly]
take_polyMXn_0 [prf, in mathcomp.algebra.poly]
take_polyZ [prf, in mathcomp.algebra.poly]
take_rev [prf, in mathcomp.boot.seq]
take_size [prf, in mathcomp.boot.seq]
take_size_cat [prf, in mathcomp.boot.seq]
take_sorted [prf, in mathcomp.boot.path]
take_subseq [prf, in mathcomp.boot.seq]
take_takel [prf, in mathcomp.boot.seq]
take_taker [prf, in mathcomp.boot.seq]
take_traject [prf, in mathcomp.boot.path]
take_tuple [def, in mathcomp.boot.tuple]
take_tupleP [prf, in mathcomp.boot.tuple]
take_uniq [prf, in mathcomp.boot.seq]
takeC [prf, in mathcomp.boot.seq]
takeD [prf, in mathcomp.boot.seq]
takeEmask [prf, in mathcomp.boot.seq]
takel_cat [prf, in mathcomp.boot.seq]
tally [def, in mathcomp.boot.seq]
tally_seq [def, in mathcomp.boot.seq]
tally_seqK [prf, in mathcomp.boot.seq]
tallyE [prf, in mathcomp.boot.seq]
tallyEl [prf, in mathcomp.boot.seq]
tallyK [prf, in mathcomp.boot.seq]
tallyP [prf, in mathcomp.boot.seq]
tcast [def, in mathcomp.boot.tuple]
tcast_id [prf, in mathcomp.boot.tuple]
tcast_trans [prf, in mathcomp.boot.tuple]
tcastE [prf, in mathcomp.boot.tuple]
tcastK [prf, in mathcomp.boot.tuple]
tcastKV [prf, in mathcomp.boot.tuple]
telescope_big [prf, in mathcomp.boot.bigop]
telescope_sumn [prf, in mathcomp.boot.bigop]
telescope_sumn_in [prf, in mathcomp.boot.bigop]
tensor [file, in mathcomp.algebra.tensor]
Tensor [constr, in mathcomp.algebra.tensor]
tensor [ind, in mathcomp.algebra.tensor]
tensor1 [def, in mathcomp.algebra.tensor]
tensor_dffun_index [def, in mathcomp.algebra.tensor]
tensor_dffun_index_bij [prf, in mathcomp.algebra.tensor]
tensor_dffun_indexK [prf, in mathcomp.algebra.tensor]
tensor_dffun_unindex [def, in mathcomp.algebra.tensor]
tensor_dffun_unindexK [prf, in mathcomp.algebra.tensor]
tensor_index [def, in mathcomp.algebra.tensor]
tensor_index_bij [prf, in mathcomp.algebra.tensor]
tensor_indexK [prf, in mathcomp.algebra.tensor]
tensor_nil [def, in mathcomp.algebra.tensor]
tensor_nil_eqP [prf, in mathcomp.algebra.tensor]
tensor_nil_is_monoid_morphism [prf, in mathcomp.algebra.tensor]
tensor_nil_is_nmod_morphism [prf, in mathcomp.algebra.tensor]
tensor_nilK [prf, in mathcomp.algebra.tensor]
tensor_nilV [prf, in mathcomp.algebra.tensor]
tensor_of_matrix [def, in mathcomp.algebra.tensor]
tensor_of_matrixK [prf, in mathcomp.algebra.tensor]
tensor_unindex [def, in mathcomp.algebra.tensor]
tensor_unindexK [prf, in mathcomp.algebra.tensor]
tensor_val [def, in mathcomp.algebra.tensor]
tensormx_cast [prf, in mathcomp.algebra.tensor]
tensormx_index [def, in mathcomp.algebra.tensor]
tensormx_indexK [prf, in mathcomp.algebra.tensor]
tensormx_unindex [def, in mathcomp.algebra.tensor]
tensormx_unindexK [prf, in mathcomp.algebra.tensor]
term [abbrev, in mathcomp.group_representation.mxrepresentation]
tfgraph [def, in mathcomp.boot.finfun]
tfgraph_inj [prf, in mathcomp.boot.finfun]
tfgraph_inv [def, in mathcomp.boot.finfun]
tfgraphK [prf, in mathcomp.boot.finfun]
tG [abbrev, in mathcomp.group_representation.mxrepresentation]
thead [def, in mathcomp.boot.tuple]
theadE [prf, in mathcomp.boot.tuple]
theta [abbrev, in mathcomp.group_representation.inertia]
thinmx0 [prf, in mathcomp.algebra.matrix]
thinmxOver [prf, in mathcomp.algebra.matrix]
third_isog [prf, in mathcomp.finite_group.quotient]
third_isom [prf, in mathcomp.finite_group.quotient]
Thompson_critical [prf, in mathcomp.solvable.maximal]
three_subgroup [prf, in mathcomp.solvable.commutator]
TI_cardMg [prf, in mathcomp.finite_group.fingroup]
TI_center_nil [prf, in mathcomp.solvable.nilpotent]
TI_cfker_irr [prf, in mathcomp.group_representation.character]
TI_Ohm1 [prf, in mathcomp.solvable.abelian]
TI_pcoreC [prf, in mathcomp.solvable.pgroup]
TIp1ElemP [prf, in mathcomp.solvable.abelian]
tnth [def, in mathcomp.boot.tuple]
tnth0 [prf, in mathcomp.boot.tuple]
tnth_behead [prf, in mathcomp.boot.tuple]
tnth_default [prf, in mathcomp.boot.tuple]
tnth_fgraph [prf, in mathcomp.boot.finfun]
tnth_in_tuple [prf, in mathcomp.boot.tuple]
tnth_lshift [prf, in mathcomp.boot.tuple]
tnth_map [prf, in mathcomp.boot.tuple]
tnth_mktuple [prf, in mathcomp.boot.tuple]
tnth_nseq [prf, in mathcomp.boot.tuple]
tnth_nth [prf, in mathcomp.boot.tuple]
tnth_onth [prf, in mathcomp.boot.tuple]
tnth_ord_tuple [prf, in mathcomp.boot.tuple]
tnth_rshift [prf, in mathcomp.boot.tuple]
tnth_tact [prf, in mathcomp.finite_group.perm]
tnthP [prf, in mathcomp.boot.tuple]
tnthS [prf, in mathcomp.boot.tuple]
to [def, in mathcomp.solvable.burnside_app]
to_dirr [def, in mathcomp.group_representation.vcharacter]
to_dirrK [prf, in mathcomp.group_representation.vcharacter]
to_family_tagged_with [def, in mathcomp.boot.finfun]
to_family_tagged_with_bij [prf, in mathcomp.boot.finfun]
to_family_tagged_withK [prf, in mathcomp.boot.finfun]
to_g [def, in mathcomp.solvable.burnside_app]
tofrac [abbrev, in mathcomp.algebra.fraction]
tofrac0 [prf, in mathcomp.algebra.fraction]
tofrac1 [prf, in mathcomp.algebra.fraction]
tofrac_eq [prf, in mathcomp.algebra.fraction]
tofrac_eq0 [prf, in mathcomp.algebra.fraction]
tofrac_is_additive [def, in mathcomp.algebra.fraction]
tofrac_is_monoid_morphism [prf, in mathcomp.algebra.fraction]
tofrac_is_multiplicative [def, in mathcomp.algebra.fraction]
tofrac_is_zmod_morphism [prf, in mathcomp.algebra.fraction]
tofracB [prf, in mathcomp.algebra.fraction]
tofracD [prf, in mathcomp.algebra.fraction]
tofracM [prf, in mathcomp.algebra.fraction]
tofracMn [prf, in mathcomp.algebra.fraction]
tofracMNn [prf, in mathcomp.algebra.fraction]
tofracN [prf, in mathcomp.algebra.fraction]
tofracXn [prf, in mathcomp.algebra.fraction]
top_wider_anything [inst, in mathcomp.algebra.interval_inference]
total_algR [prf, in mathcomp.field.algC]
total_fun [def, in mathcomp.boot.finfun]
total_homo_mono [prf, in mathcomp.boot.eqtype]
total_homo_mono_in [prf, in mathcomp.boot.eqtype]
TotalAction [def, in mathcomp.finite_group.action]
totient [def, in mathcomp.boot.prime]
totient_coprime [prf, in mathcomp.boot.prime]
totient_count_coprime [prf, in mathcomp.boot.prime]
totient_gen [prf, in mathcomp.solvable.cyclic]
totient_gt0 [prf, in mathcomp.boot.prime]
totient_gt1 [prf, in mathcomp.boot.prime]
totient_pfactor [prf, in mathcomp.boot.prime]
totient_prime [prf, in mathcomp.boot.prime]
totientE [prf, in mathcomp.boot.prime]
tperm [def, in mathcomp.finite_group.perm]
tperm1 [prf, in mathcomp.finite_group.perm]
tperm2 [prf, in mathcomp.finite_group.perm]
tperm_mx [def, in mathcomp.algebra.matrix]
tperm_mxEsub [prf, in mathcomp.algebra.matrix]
tperm_on [prf, in mathcomp.finite_group.perm]
tperm_proof [prf, in mathcomp.finite_group.perm]
tperm_spec [ind, in mathcomp.finite_group.perm]
tpermC [prf, in mathcomp.finite_group.perm]
tpermD [prf, in mathcomp.finite_group.perm]
TpermFirst [constr, in mathcomp.finite_group.perm]
tpermJ [prf, in mathcomp.finite_group.perm]
tpermJ_tperm [prf, in mathcomp.finite_group.perm]
tpermK [prf, in mathcomp.finite_group.perm]
tpermKg [prf, in mathcomp.finite_group.perm]
tpermL [prf, in mathcomp.finite_group.perm]
TpermNone [constr, in mathcomp.finite_group.perm]
tpermP [prf, in mathcomp.finite_group.perm]
tpermR [prf, in mathcomp.finite_group.perm]
TpermSecond [constr, in mathcomp.finite_group.perm]
tpermV [prf, in mathcomp.finite_group.perm]
tprod [def, in mathcomp.group_representation.character]
tprod1 [prf, in mathcomp.group_representation.character]
tprodE [prf, in mathcomp.group_representation.character]
tr_block_mx [prf, in mathcomp.algebra.matrix]
tr_col [prf, in mathcomp.algebra.matrix]
tr_col' [prf, in mathcomp.algebra.matrix]
tr_col_mx [prf, in mathcomp.algebra.matrix]
tr_col_perm [prf, in mathcomp.algebra.matrix]
tr_diag_mx [prf, in mathcomp.algebra.matrix]
tr_mxblock [prf, in mathcomp.algebra.matrix]
tr_mxcol [prf, in mathcomp.algebra.matrix]
tr_mxdiag [prf, in mathcomp.algebra.matrix]
tr_mxrow [prf, in mathcomp.algebra.matrix]
tr_perm_mx [prf, in mathcomp.algebra.matrix]
tr_pid_mx [prf, in mathcomp.algebra.matrix]
tr_row [prf, in mathcomp.algebra.matrix]
tr_row' [prf, in mathcomp.algebra.matrix]
tr_row_mx [prf, in mathcomp.algebra.matrix]
tr_row_perm [prf, in mathcomp.algebra.matrix]
tr_scalar_mx [prf, in mathcomp.algebra.matrix]
tr_submxblock [prf, in mathcomp.algebra.matrix]
tr_submxcol [prf, in mathcomp.algebra.matrix]
tr_submxrow [prf, in mathcomp.algebra.matrix]
tr_tperm_mx [prf, in mathcomp.algebra.matrix]
tr_xcol [prf, in mathcomp.algebra.matrix]
tr_xrow [prf, in mathcomp.algebra.matrix]
trace_map_mx [prf, in mathcomp.algebra.matrix]
trace_mx11 [prf, in mathcomp.algebra.matrix]
traject [def, in mathcomp.boot.path]
traject_iteri [prf, in mathcomp.boot.path]
trajectD [prf, in mathcomp.boot.path]
trajectP [prf, in mathcomp.boot.path]
trajectS [prf, in mathcomp.boot.path]
trajectSr [prf, in mathcomp.boot.path]
trans_prim_astab [prf, in mathcomp.solvable.primitive_action]
trans_subnorm_fixP [prf, in mathcomp.finite_group.action]
transfer [def, in mathcomp.solvable.finmodule]
transfer_cycle_expansion [prf, in mathcomp.solvable.finmodule]
transfer_indep [prf, in mathcomp.solvable.finmodule]
transfer_morphism [def, in mathcomp.solvable.finmodule]
transferM [prf, in mathcomp.solvable.finmodule]
transRs_rcosets [prf, in mathcomp.finite_group.action]
transversal [def, in mathcomp.boot.finset]
transversal_repr [def, in mathcomp.boot.finset]
transversal_reprK [prf, in mathcomp.boot.finset]
transversal_sub [prf, in mathcomp.boot.finset]
transversalP [prf, in mathcomp.boot.finset]
triangle_lerif [prf, in mathcomp.algebra.sesquilinear]
triangular_sum [abbrev, in mathcomp.boot.binomial]
trigmx_ind [prf, in mathcomp.algebra.matrix]
trigonalizable [abbrev, in mathcomp.algebra.mxred]
trigonalizable_in [abbrev, in mathcomp.algebra.mxred]
trigsqmx_ind [prf, in mathcomp.algebra.matrix]
triv_cprod [prf, in mathcomp.finite_group.gproduct]
triv_morph [def, in mathcomp.finite_group.morphism]
triv_restr_perm [prf, in mathcomp.finite_group.action]
trivg0 [prf, in mathcomp.finite_group.gproduct]
trivg_acomps [prf, in mathcomp.solvable.jordanholder]
trivg_card1 [prf, in mathcomp.finite_group.fingroup]
trivg_card_le1 [prf, in mathcomp.finite_group.fingroup]
trivg_center_pgroup [prf, in mathcomp.solvable.sylow]
trivg_comps [prf, in mathcomp.solvable.jordanholder]
trivg_exponent [prf, in mathcomp.solvable.abelian]
trivg_Fitting [prf, in mathcomp.solvable.maximal]
trivg_Mho [prf, in mathcomp.solvable.abelian]
trivg_pcore_quotient [prf, in mathcomp.solvable.pgroup]
trivg_Phi [prf, in mathcomp.solvable.maximal]
trivg_quotient [prf, in mathcomp.finite_group.quotient]
trivg_rowg [prf, in mathcomp.group_representation.mxabelem]
trivGfun [def, in mathcomp.solvable.gfunctor]
trivGfun_cont [prf, in mathcomp.solvable.gfunctor]
trivGfun_gFun [def, in mathcomp.solvable.gfunctor]
trivGfun_igFun [def, in mathcomp.solvable.gfunctor]
trivGfun_pgFun [def, in mathcomp.solvable.gfunctor]
trivGP [prf, in mathcomp.finite_group.fingroup]
trivgP [prf, in mathcomp.finite_group.fingroup]
trivgPn [prf, in mathcomp.finite_group.fingroup]
trivgVpdiv [prf, in mathcomp.solvable.pgroup]
trivial_addv [def, in mathcomp.algebra.vector]
trivial_Alt_2 [prf, in mathcomp.solvable.alt]
trivial_fieldOver [prf, in mathcomp.field.fieldext]
trivial_isog [prf, in mathcomp.finite_group.morphism]
trivial_mxsum [def, in mathcomp.algebra.mxalgebra]
TrivialMxsum [constr, in mathcomp.algebra.mxalgebra]
trivIimset [prf, in mathcomp.boot.finset]
trivIset [def, in mathcomp.boot.finset]
trivIset1 [prf, in mathcomp.boot.finset]
trivIsetD [prf, in mathcomp.boot.finset]
trivIsetI [prf, in mathcomp.boot.finset]
trivIsetP [prf, in mathcomp.boot.finset]
trivIsetS [prf, in mathcomp.boot.finset]
trivIsetU [prf, in mathcomp.boot.finset]
trivIsetU1 [prf, in mathcomp.boot.finset]
trivm [def, in mathcomp.finite_group.morphism]
trivm_morphM [prf, in mathcomp.finite_group.morphism]
trivMg [prf, in mathcomp.finite_group.fingroup]
trmx [def, in mathcomp.algebra.matrix]
trmx0 [prf, in mathcomp.algebra.matrix]
trmx1 [prf, in mathcomp.algebra.matrix]
trmx_adj [prf, in mathcomp.algebra.matrix]
trmx_cast [prf, in mathcomp.algebra.matrix]
trmx_conform [prf, in mathcomp.algebra.matrix]
trmx_const [prf, in mathcomp.algebra.matrix]
trmx_delta [prf, in mathcomp.algebra.matrix]
trmx_dlsub [prf, in mathcomp.algebra.matrix]
trmx_drsub [prf, in mathcomp.algebra.matrix]
trmx_dsub [prf, in mathcomp.algebra.matrix]
trmx_eq0 [prf, in mathcomp.algebra.matrix]
trmx_hermitian [prf, in mathcomp.algebra.sesquilinear]
trmx_inj [prf, in mathcomp.algebra.matrix]
trmx_inv [prf, in mathcomp.algebra.matrix]
trmx_key [prf, in mathcomp.algebra.matrix]
trmx_lsub [prf, in mathcomp.algebra.matrix]
trmx_mul [prf, in mathcomp.algebra.matrix]
trmx_mul_rev [prf, in mathcomp.algebra.matrix]
trmx_mxsub [prf, in mathcomp.algebra.matrix]
trmx_rsub [prf, in mathcomp.algebra.matrix]
trmx_sesqui [prf, in mathcomp.algebra.sesquilinear]
trmx_ulsub [prf, in mathcomp.algebra.matrix]
trmx_unitary [prf, in mathcomp.algebra.spectral]
trmx_ursub [prf, in mathcomp.algebra.matrix]
trmx_usub [prf, in mathcomp.algebra.matrix]
trmxC_unitary [prf, in mathcomp.algebra.spectral]
trmxCK [prf, in mathcomp.algebra.spectral]
trmxK [prf, in mathcomp.algebra.matrix]
trmxV [prf, in mathcomp.algebra.matrix]
trow [def, in mathcomp.group_representation.character]
trow0 [prf, in mathcomp.group_representation.character]
trow_is_linear [prf, in mathcomp.group_representation.character]
trowb [def, in mathcomp.group_representation.character]
trowb_is_linear [prf, in mathcomp.group_representation.character]
trowbE [prf, in mathcomp.group_representation.character]
True [abbrev, in mathcomp.group_representation.mxrepresentation]
trunc_expnK [prf, in mathcomp.boot.prime]
trunc_log [def, in mathcomp.boot.prime]
trunc_log0 [prf, in mathcomp.boot.prime]
trunc_log0n [prf, in mathcomp.boot.prime]
trunc_log1 [prf, in mathcomp.boot.prime]
trunc_log1n [prf, in mathcomp.boot.prime]
trunc_log2_double [prf, in mathcomp.boot.prime]
trunc_log2S [prf, in mathcomp.boot.prime]
trunc_log_bounds [prf, in mathcomp.boot.prime]
trunc_log_eq [prf, in mathcomp.boot.prime]
trunc_log_eq0 [prf, in mathcomp.boot.prime]
trunc_log_gt0 [prf, in mathcomp.boot.prime]
trunc_log_ltn [prf, in mathcomp.boot.prime]
trunc_log_max [prf, in mathcomp.boot.prime]
trunc_log_up_log [prf, in mathcomp.boot.prime]
trunc_logMp [prf, in mathcomp.boot.prime]
trunc_lognn [prf, in mathcomp.boot.prime]
trunc_logP [prf, in mathcomp.boot.prime]
tseq [abbrev, in mathcomp.boot.seq]
tsize [def, in mathcomp.boot.tuple]
tuple [file, in mathcomp.boot.tuple]
tuple [def, in mathcomp.boot.tuple]
tuple0 [prf, in mathcomp.boot.tuple]
tuple1_spec [ind, in mathcomp.boot.tuple]
Tuple1spec [constr, in mathcomp.boot.tuple]
tuple_eta [prf, in mathcomp.boot.tuple]
tuple_map_ord [prf, in mathcomp.boot.tuple]
tuple_of [rec, in mathcomp.boot.tuple]
tuple_of_finfun [def, in mathcomp.boot.finfun]
tuple_of_finfunK [prf, in mathcomp.boot.finfun]
tuple_of_ntensor [def, in mathcomp.algebra.tensor]
tuple_of_ntensorK [prf, in mathcomp.algebra.tensor]
tuple_of_otensor [def, in mathcomp.algebra.tensor]
tuple_of_otensorK [prf, in mathcomp.algebra.tensor]
tuple_permP [prf, in mathcomp.finite_group.perm]
tuple_predType [def, in mathcomp.boot.tuple]
tuple_uniqP [prf, in mathcomp.boot.tuple]
tupleE [prf, in mathcomp.boot.tuple]
tupleP [prf, in mathcomp.boot.tuple]
tval [proj, in mathcomp.boot.tuple]
tval_tact_lift0 [prf, in mathcomp.finite_group.perm]
tvalK [prf, in mathcomp.boot.tuple]
type [abbrev, in mathcomp.field.finfield]
TypInstances [mod, in mathcomp.algebra.interval_inference]
TypInstances.nat_typ [def, in mathcomp.algebra.interval_inference]
TypInstances.nat_typ_spec [prf, in mathcomp.algebra.interval_inference]
TypInstances.real_domain_typ [def, in mathcomp.algebra.interval_inference]
TypInstances.real_domain_typ_spec [prf, in mathcomp.algebra.interval_inference]
TypInstances.real_field_typ [def, in mathcomp.algebra.interval_inference]
TypInstances.real_field_typ_spec [prf, in mathcomp.algebra.interval_inference]
TypInstances.top_typ [def, in mathcomp.algebra.interval_inference]
TypInstances.top_typ_spec [prf, in mathcomp.algebra.interval_inference]
TypInstances.typ_inum [def, in mathcomp.algebra.interval_inference]
TypInstances.typ_inum_spec [prf, in mathcomp.algebra.interval_inference]