T (Lemmas)
| 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 (Lemmas)
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_enumP [prf, in mathcomp.boot.fintype]
tag_eqE [prf, in mathcomp.boot.eqtype]
tag_eqP [prf, in mathcomp.boot.eqtype]
tag_fprod_fun [prf, in mathcomp.boot.finfun]
tag_of_pairK [prf, in mathcomp.boot.choice]
tag_with_bij [prf, in mathcomp.boot.eqtype]
tag_withK [prf, 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_bij [prf, in mathcomp.boot.tuple]
tagged_tuple_bseqK [prf, in mathcomp.boot.tuple]
taggedK [prf, in mathcomp.boot.ssrfun]
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.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.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]
take0 [prf, in mathcomp.boot.seq]
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_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_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_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_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_dffun_index_bij [prf, in mathcomp.algebra.tensor]
tensor_dffun_indexK [prf, in mathcomp.algebra.tensor]
tensor_dffun_unindexK [prf, in mathcomp.algebra.tensor]
tensor_index_bij [prf, in mathcomp.algebra.tensor]
tensor_indexK [prf, 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_matrixK [prf, in mathcomp.algebra.tensor]
tensor_unindexK [prf, in mathcomp.algebra.tensor]
tensormx_cast [prf, in mathcomp.algebra.tensor]
tensormx_indexK [prf, in mathcomp.algebra.tensor]
tensormx_unindexK [prf, in mathcomp.algebra.tensor]
tfgraph_inj [prf, in mathcomp.boot.finfun]
tfgraphK [prf, in mathcomp.boot.finfun]
theadE [prf, in mathcomp.boot.tuple]
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]
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_dirrK [prf, in mathcomp.group_representation.vcharacter]
to_family_tagged_with_bij [prf, in mathcomp.boot.finfun]
to_family_tagged_withK [prf, in mathcomp.boot.finfun]
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_monoid_morphism [prf, 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]
total_algR [prf, in mathcomp.field.algC]
total_homo_mono [prf, in mathcomp.boot.eqtype]
total_homo_mono_in [prf, in mathcomp.boot.eqtype]
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]
tperm1 [prf, in mathcomp.finite_group.perm]
tperm2 [prf, in mathcomp.finite_group.perm]
tperm_mxEsub [prf, in mathcomp.algebra.matrix]
tperm_on [prf, in mathcomp.finite_group.perm]
tperm_proof [prf, in mathcomp.finite_group.perm]
tpermC [prf, in mathcomp.finite_group.perm]
tpermD [prf, 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]
tpermP [prf, in mathcomp.finite_group.perm]
tpermR [prf, in mathcomp.finite_group.perm]
tpermV [prf, in mathcomp.finite_group.perm]
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_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_cycle_expansion [prf, in mathcomp.solvable.finmodule]
transfer_indep [prf, in mathcomp.solvable.finmodule]
transferM [prf, in mathcomp.solvable.finmodule]
transRs_rcosets [prf, in mathcomp.finite_group.action]
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]
trigmx_ind [prf, in mathcomp.algebra.matrix]
trigsqmx_ind [prf, in mathcomp.algebra.matrix]
triv_cprod [prf, in mathcomp.finite_group.gproduct]
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_cont [prf, 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_Alt_2 [prf, in mathcomp.solvable.alt]
trivial_fieldOver [prf, in mathcomp.field.fieldext]
trivial_isog [prf, in mathcomp.finite_group.morphism]
trivIimset [prf, 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_morphM [prf, in mathcomp.finite_group.morphism]
trivMg [prf, in mathcomp.finite_group.fingroup]
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]
trow0 [prf, in mathcomp.group_representation.character]
trow_is_linear [prf, in mathcomp.group_representation.character]
trowb_is_linear [prf, in mathcomp.group_representation.character]
trowbE [prf, in mathcomp.group_representation.character]
trunc_expnK [prf, 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]
tuple0 [prf, in mathcomp.boot.tuple]
tuple_eta [prf, in mathcomp.boot.tuple]
tuple_map_ord [prf, in mathcomp.boot.tuple]
tuple_of_finfunK [prf, in mathcomp.boot.finfun]
tuple_of_ntensorK [prf, in mathcomp.algebra.tensor]
tuple_of_otensorK [prf, in mathcomp.algebra.tensor]
tuple_permP [prf, in mathcomp.finite_group.perm]
tuple_uniqP [prf, in mathcomp.boot.tuple]
tupleE [prf, in mathcomp.boot.tuple]
tupleP [prf, in mathcomp.boot.tuple]
tval_tact_lift0 [prf, in mathcomp.finite_group.perm]
tvalK [prf, in mathcomp.boot.tuple]
TypInstances.nat_typ_spec [prf, in mathcomp.algebra.interval_inference]
TypInstances.real_domain_typ_spec [prf, in mathcomp.algebra.interval_inference]
TypInstances.real_field_typ_spec [prf, in mathcomp.algebra.interval_inference]
TypInstances.top_typ_spec [prf, in mathcomp.algebra.interval_inference]
TypInstances.typ_inum_spec [prf, in mathcomp.algebra.interval_inference]