| 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 | (54001 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 | (1931 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 | (1658 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 | (7199 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 | (97 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 | (15214 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 | (75 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 | (224 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 | (132 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 | (2371 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 | (2266 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 | (732 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 | (21455 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 | (647 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_tuple_bseq_bij [lemma, in mathcomp.ssreflect.tuple]
tagged_tuple_bseqK [lemma, in mathcomp.ssreflect.tuple]
tagged_tuple_bseq [definition, in mathcomp.ssreflect.tuple]
tagged_hasChoice [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]
tagnat [module, in mathcomp.ssreflect.order]
tagnat.card [lemma, in mathcomp.ssreflect.order]
tagnat.eqRank [lemma, in mathcomp.ssreflect.order]
tagnat.eq_Rank [lemma, in mathcomp.ssreflect.order]
tagnat.le_Rank [lemma, in mathcomp.ssreflect.order]
tagnat.le_rank [lemma, in mathcomp.ssreflect.order]
tagnat.le_sig1 [lemma, in mathcomp.ssreflect.order]
tagnat.le_sig [lemma, in mathcomp.ssreflect.order]
tagnat.lt_Rank [lemma, in mathcomp.ssreflect.order]
tagnat.lt_rank [lemma, in mathcomp.ssreflect.order]
tagnat.lt_sig [lemma, in mathcomp.ssreflect.order]
tagnat.ordsum [abbreviation, in mathcomp.ssreflect.order]
tagnat.Rank [definition, in mathcomp.ssreflect.order]
tagnat.rank [definition, in mathcomp.ssreflect.order]
tagnat.rankE [lemma, in mathcomp.ssreflect.order]
tagnat.RankEsum [lemma, in mathcomp.ssreflect.order]
tagnat.rankEsum [lemma, in mathcomp.ssreflect.order]
tagnat.rankK [lemma, in mathcomp.ssreflect.order]
tagnat.rank_bij_on [lemma, in mathcomp.ssreflect.order]
tagnat.rank_bij [lemma, in mathcomp.ssreflect.order]
tagnat.rank_inj [lemma, in mathcomp.ssreflect.order]
tagnat.Rank1K [lemma, in mathcomp.ssreflect.order]
tagnat.Rank2K [lemma, in mathcomp.ssreflect.order]
tagnat.rect [lemma, in mathcomp.ssreflect.order]
tagnat.sig [definition, in mathcomp.ssreflect.order]
tagnat.sigE12 [lemma, in mathcomp.ssreflect.order]
tagnat.sigK [lemma, in mathcomp.ssreflect.order]
tagnat.sig_bij_on [lemma, in mathcomp.ssreflect.order]
tagnat.sig_bij [lemma, in mathcomp.ssreflect.order]
tagnat.sig_inj [lemma, in mathcomp.ssreflect.order]
tagnat.sig1 [definition, in mathcomp.ssreflect.order]
tagnat.sig2 [definition, in mathcomp.ssreflect.order]
tagnat.sig2K [lemma, in mathcomp.ssreflect.order]
tagnat.T [abbreviation, in mathcomp.ssreflect.order]
tagnat.tagnat [section, in mathcomp.ssreflect.order]
tag_of_pairK [lemma, in mathcomp.ssreflect.choice]
tag_of_pair [definition, in mathcomp.ssreflect.choice]
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]
takeC [lemma, in mathcomp.ssreflect.seq]
takeD [lemma, in mathcomp.ssreflect.seq]
takeEmask [lemma, in mathcomp.ssreflect.seq]
takel_cat [lemma, in mathcomp.ssreflect.seq]
take_bseq [definition, in mathcomp.ssreflect.tuple]
take_bseqP [lemma, in mathcomp.ssreflect.tuple]
take_tuple [definition, in mathcomp.ssreflect.tuple]
take_tupleP [lemma, in mathcomp.ssreflect.tuple]
take_iota [lemma, in mathcomp.ssreflect.seq]
take_uniq [lemma, in mathcomp.ssreflect.seq]
take_subseq [lemma, in mathcomp.ssreflect.seq]
take_rev [lemma, in mathcomp.ssreflect.seq]
take_pivot [lemma, in mathcomp.ssreflect.seq]
take_nth [lemma, in mathcomp.ssreflect.seq]
take_nseq [lemma, in mathcomp.ssreflect.seq]
take_drop [lemma, in mathcomp.ssreflect.seq]
take_taker [lemma, in mathcomp.ssreflect.seq]
take_takel [lemma, in mathcomp.ssreflect.seq]
take_min [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]
take_traject [lemma, in mathcomp.ssreflect.path]
take_sorted [lemma, in mathcomp.ssreflect.path]
take_path [lemma, in mathcomp.ssreflect.path]
take_polyDMXn [lemma, in mathcomp.algebra.poly]
take_polyMXn_0 [lemma, in mathcomp.algebra.poly]
take_polyMXn [lemma, in mathcomp.algebra.poly]
take_poly0r [lemma, in mathcomp.algebra.poly]
take_poly0l [lemma, in mathcomp.algebra.poly]
take_poly_sum [lemma, in mathcomp.algebra.poly]
take_poly_is_linear [lemma, in mathcomp.algebra.poly]
take_polyZ [lemma, in mathcomp.algebra.poly]
take_polyD [lemma, in mathcomp.algebra.poly]
take_poly_id [lemma, in mathcomp.algebra.poly]
take_poly [definition, in mathcomp.algebra.poly]
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]
telescope_sumn [lemma, in mathcomp.ssreflect.bigop]
telescope_sumn_in [lemma, in mathcomp.ssreflect.bigop]
telescope_big [lemma, in mathcomp.ssreflect.bigop]
Tensor [section, in mathcomp.character.character]
Tensor.F [variable, in mathcomp.character.character]
Tensor.hb_instance_7.A [variable, in mathcomp.character.character]
Tensor.hb_instance_7.n2 [variable, in mathcomp.character.character]
Tensor.hb_instance_7.m2 [variable, in mathcomp.character.character]
Tensor.hb_instance_7.n1 [variable, in mathcomp.character.character]
Tensor.hb_instance_7.hb_instance_7 [section, in mathcomp.character.character]
Tensor.hb_instance_1.B [variable, in mathcomp.character.character]
Tensor.hb_instance_1.n2 [variable, in mathcomp.character.character]
Tensor.hb_instance_1.m2 [variable, in mathcomp.character.character]
Tensor.hb_instance_1.n1 [variable, in mathcomp.character.character]
Tensor.hb_instance_1.hb_instance_1 [section, 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]
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]
thinmxOver [lemma, in mathcomp.algebra.matrix]
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_cardMg [lemma, in mathcomp.fingroup.fingroup]
TI_pcoreC [lemma, in mathcomp.solvable.pgroup]
TI_Ohm1 [lemma, in mathcomp.solvable.abelian]
TI_cfker_irr [lemma, in mathcomp.character.character]
TI_center_nil [lemma, in mathcomp.solvable.nilpotent]
tnth [definition, in mathcomp.ssreflect.tuple]
tnthP [lemma, in mathcomp.ssreflect.tuple]
tnthS [lemma, in mathcomp.ssreflect.tuple]
tnth_mktuple [lemma, in mathcomp.ssreflect.tuple]
tnth_ord_tuple [lemma, in mathcomp.ssreflect.tuple]
tnth_rshift [lemma, in mathcomp.ssreflect.tuple]
tnth_lshift [lemma, in mathcomp.ssreflect.tuple]
tnth_shift [section, in mathcomp.ssreflect.tuple]
tnth_behead [lemma, in mathcomp.ssreflect.tuple]
tnth_nseq [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]
tofracXn [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_gt1 [lemma, in mathcomp.ssreflect.prime]
totient_count_coprime [lemma, in mathcomp.ssreflect.prime]
totient_coprime [lemma, in mathcomp.ssreflect.prime]
totient_prime [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]
tpermJ [section, in mathcomp.fingroup.perm]
tpermJ_tperm [lemma, in mathcomp.fingroup.perm]
tpermJ.T [variable, 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_on [lemma, in mathcomp.fingroup.perm]
tperm_spec [inductive, in mathcomp.fingroup.perm]
tperm_proof [lemma, in mathcomp.fingroup.perm]
tperm_mxEsub [lemma, in mathcomp.algebra.matrix]
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]
trajectD [lemma, 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.hb_instance_15.fK [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_15.g [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_15.hb_instance_15 [section, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_11.fK [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_11.g [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_11.hb_instance_11 [section, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_8.f_inj [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_8.hb_instance_8 [section, in mathcomp.ssreflect.eqtype]
TransferEqType.T [variable, in mathcomp.ssreflect.eqtype]
TransferFinType [section, in mathcomp.ssreflect.fintype]
TransferFinTypeFromCount [section, in mathcomp.ssreflect.fintype]
TransferFinTypeFromCount.eT [variable, in mathcomp.ssreflect.fintype]
TransferFinTypeFromCount.f [variable, in mathcomp.ssreflect.fintype]
TransferFinTypeFromCount.fT [variable, 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]
TransferFinType.hb_instance_23.fK [variable, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_23.g [variable, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_23.hb_instance_23 [section, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_20.fK [variable, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_20.g [variable, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_20.hb_instance_20 [section, in mathcomp.ssreflect.fintype]
transferM [lemma, in mathcomp.solvable.finmodule]
TransferType [section, in mathcomp.ssreflect.eqtype]
TransferType.f [variable, in mathcomp.ssreflect.eqtype]
TransferType.T [variable, in mathcomp.ssreflect.eqtype]
TransferType.T' [variable, in mathcomp.ssreflect.eqtype]
transfer_cycle_expansion [lemma, in mathcomp.solvable.finmodule]
transfer_indep [lemma, in mathcomp.solvable.finmodule]
transfer_morphism [definition, 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]
triangle_lerif [lemma, in mathcomp.algebra.sesquilinear]
triangular_sum [abbreviation, in mathcomp.ssreflect.binomial]
trigmx_ind [lemma, in mathcomp.algebra.matrix]
trigonalizable [abbreviation, in mathcomp.algebra.mxred]
trigonalizable_in [abbreviation, in mathcomp.algebra.mxred]
trigsqmx_ind [lemma, in mathcomp.algebra.matrix]
trivGfun [definition, in mathcomp.solvable.gfunctor]
trivGfun_pgFun [definition, in mathcomp.solvable.gfunctor]
trivGfun_gFun [definition, in mathcomp.solvable.gfunctor]
trivGfun_igFun [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_quotient [lemma, in mathcomp.fingroup.quotient]
trivg_acomps [lemma, in mathcomp.solvable.jordanholder]
trivg_comps [lemma, in mathcomp.solvable.jordanholder]
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]
trivg_pcore_quotient [lemma, in mathcomp.solvable.pgroup]
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]
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]
trivial_addv [definition, in mathcomp.algebra.vector]
trivial_mxsum [definition, in mathcomp.algebra.mxalgebra]
trivIimset [lemma, in mathcomp.ssreflect.finset]
trivIset [definition, in mathcomp.ssreflect.finset]
trivIsetD [lemma, in mathcomp.ssreflect.finset]
trivIsetI [lemma, in mathcomp.ssreflect.finset]
trivIsetP [lemma, in mathcomp.ssreflect.finset]
trivIsetS [lemma, in mathcomp.ssreflect.finset]
trivIsetU [lemma, in mathcomp.ssreflect.finset]
trivIsetU1 [lemma, in mathcomp.ssreflect.finset]
trivIset1 [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_restr_perm [lemma, in mathcomp.fingroup.action]
triv_cprod [lemma, in mathcomp.fingroup.gproduct]
triv_morph [definition, in mathcomp.fingroup.morphism]
trmx [definition, in mathcomp.algebra.matrix]
trmxCK [lemma, in mathcomp.algebra.spectral]
trmxC_unitary [lemma, in mathcomp.algebra.spectral]
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_eq0 [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_mxsub [lemma, in mathcomp.algebra.matrix]
trmx_conform [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]
trmx_unitary [lemma, in mathcomp.algebra.spectral]
trmx_hermitian [lemma, in mathcomp.algebra.sesquilinear]
trmx_sesqui [lemma, in mathcomp.algebra.sesquilinear]
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]
trunc_log_up_log [lemma, in mathcomp.ssreflect.prime]
trunc_log2S [lemma, in mathcomp.ssreflect.prime]
trunc_log2_double [lemma, in mathcomp.ssreflect.prime]
trunc_logMp [lemma, in mathcomp.ssreflect.prime]
trunc_expnK [lemma, in mathcomp.ssreflect.prime]
trunc_lognn [lemma, in mathcomp.ssreflect.prime]
trunc_log_eq [lemma, in mathcomp.ssreflect.prime]
trunc_log1n [lemma, in mathcomp.ssreflect.prime]
trunc_log0n [lemma, in mathcomp.ssreflect.prime]
trunc_log_gt0 [lemma, in mathcomp.ssreflect.prime]
trunc_log_eq0 [lemma, in mathcomp.ssreflect.prime]
trunc_log_max [lemma, in mathcomp.ssreflect.prime]
trunc_log_ltn [lemma, in mathcomp.ssreflect.prime]
trunc_logP [lemma, in mathcomp.ssreflect.prime]
trunc_log_bounds [lemma, in mathcomp.ssreflect.prime]
trunc_log1 [lemma, in mathcomp.ssreflect.prime]
trunc_log0 [lemma, in mathcomp.ssreflect.prime]
trunc_log [definition, in mathcomp.ssreflect.prime]
tr_mxdiag [lemma, in mathcomp.algebra.matrix]
tr_submxcol [lemma, in mathcomp.algebra.matrix]
tr_submxrow [lemma, in mathcomp.algebra.matrix]
tr_submxblock [lemma, in mathcomp.algebra.matrix]
tr_mxcol [lemma, in mathcomp.algebra.matrix]
tr_mxrow [lemma, in mathcomp.algebra.matrix]
tr_mxblock [lemma, in mathcomp.algebra.matrix]
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 [library]
TupleDef [section, in mathcomp.ssreflect.tuple]
TupleDef.n [variable, in mathcomp.ssreflect.tuple]
TupleDef.T [variable, in mathcomp.ssreflect.tuple]
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_permP [lemma, in mathcomp.fingroup.perm]
tuple_bseq_of__canonical__fintype_SubFinite [definition, in mathcomp.ssreflect.tuple]
tuple_bseq_of__canonical__fintype_Finite [definition, in mathcomp.ssreflect.tuple]
tuple_bseq_of__canonical__choice_SubCountable [definition, in mathcomp.ssreflect.tuple]
tuple_bseq_of__canonical__choice_Countable [definition, in mathcomp.ssreflect.tuple]
tuple_bseq_of__canonical__choice_SubChoice [definition, in mathcomp.ssreflect.tuple]
tuple_bseq_of__canonical__choice_Choice [definition, in mathcomp.ssreflect.tuple]
tuple_bseq_of__canonical__eqtype_SubEquality [definition, in mathcomp.ssreflect.tuple]
tuple_bseq_of__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.tuple]
tuple_bseq_of__canonical__eqtype_SubType [definition, in mathcomp.ssreflect.tuple]
tuple_map_ord [lemma, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__fintype_SubFinite [definition, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__fintype_Finite [definition, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__choice_SubCountable [definition, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__choice_Countable [definition, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__choice_SubChoice [definition, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__choice_Choice [definition, in mathcomp.ssreflect.tuple]
tuple_uniqP [lemma, in mathcomp.ssreflect.tuple]
tuple_predType [definition, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__eqtype_SubEquality [definition, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.tuple]
tuple_eta [lemma, in mathcomp.ssreflect.tuple]
tuple_tuple_of__canonical__eqtype_SubType [definition, in mathcomp.ssreflect.tuple]
tuple_of [record, in mathcomp.ssreflect.tuple]
tuple_of_finfunK [lemma, in mathcomp.ssreflect.finfun]
tuple_of_finfun [definition, in mathcomp.ssreflect.finfun]
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 | (54001 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 | (1931 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 | (1658 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 | (7199 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 | (97 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 | (15214 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 | (75 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 | (224 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 | (132 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 | (2371 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 | (2266 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 | (732 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 | (21455 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 | (647 entries) |