mathcomp.ssreflect.tuple

Global Index

_

(80254 entries)

Notation Index

H

J

T

W

X

Y

_

(1852 entries)

Binder Index

_

other

(48996 entries)

Module Index

H

J

K

L

W

X

Y

Z

_

other

(383 entries)

Variable Index

J

W

X

Y

_

other

(4219 entries)

Library Index

K

L

U

W

X

Y

_

other

(93 entries)

Lemma Index

Y

_

other

(14738 entries)

Constructor Index

J

K

W

Y

_

other

(223 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

D

H

J

K

L

W

X

Y

_

other

(452 entries)

Section Index

J

W

X

Y

_

other

(1431 entries)

Abbreviation Index

Y

_

other

(1169 entries)

Definition Index

Y

_

other

(6273 entries)

Record Index

D

H

J

K

L

W

X

Y

_

other

(248 entries)

T (lemma)

tagged_tuple_bseq_bij [in mathcomp.ssreflect.tuple]
tagged_tuple_bseqK [in mathcomp.ssreflect.tuple]
tagged_choiceMixin [in mathcomp.ssreflect.choice]
tagged_tfgraph [in mathcomp.ssreflect.finfun]
tagged_asE [in mathcomp.ssreflect.eqtype]
tagnat.card [in mathcomp.ssreflect.order]
tagnat.eqRank [in mathcomp.ssreflect.order]
tagnat.eq_Rank [in mathcomp.ssreflect.order]
tagnat.le_Rank [in mathcomp.ssreflect.order]
tagnat.le_rank [in mathcomp.ssreflect.order]
tagnat.le_sig1 [in mathcomp.ssreflect.order]
tagnat.le_sig [in mathcomp.ssreflect.order]
tagnat.lt_Rank [in mathcomp.ssreflect.order]
tagnat.lt_rank [in mathcomp.ssreflect.order]
tagnat.lt_sig [in mathcomp.ssreflect.order]
tagnat.rankE [in mathcomp.ssreflect.order]
tagnat.RankEsum [in mathcomp.ssreflect.order]
tagnat.rankEsum [in mathcomp.ssreflect.order]
tagnat.rankK [in mathcomp.ssreflect.order]
tagnat.rank_bij_on [in mathcomp.ssreflect.order]
tagnat.rank_bij [in mathcomp.ssreflect.order]
tagnat.rank_inj [in mathcomp.ssreflect.order]
tagnat.Rank1K [in mathcomp.ssreflect.order]
tagnat.Rank2K [in mathcomp.ssreflect.order]
tagnat.rect [in mathcomp.ssreflect.order]
tagnat.sigE12 [in mathcomp.ssreflect.order]
tagnat.sigK [in mathcomp.ssreflect.order]
tagnat.sig_bij_on [in mathcomp.ssreflect.order]
tagnat.sig_bij [in mathcomp.ssreflect.order]
tagnat.sig_inj [in mathcomp.ssreflect.order]
tagnat.sig2K [in mathcomp.ssreflect.order]
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]
takeC [in mathcomp.ssreflect.seq]
takeD [in mathcomp.ssreflect.seq]
takeEmask [in mathcomp.ssreflect.seq]
takel_cat [in mathcomp.ssreflect.seq]
take_bseqP [in mathcomp.ssreflect.tuple]
take_tupleP [in mathcomp.ssreflect.tuple]
take_iota [in mathcomp.ssreflect.seq]
take_uniq [in mathcomp.ssreflect.seq]
take_subseq [in mathcomp.ssreflect.seq]
take_rev [in mathcomp.ssreflect.seq]
take_pivot [in mathcomp.ssreflect.seq]
take_nth [in mathcomp.ssreflect.seq]
take_nseq [in mathcomp.ssreflect.seq]
take_drop [in mathcomp.ssreflect.seq]
take_taker [in mathcomp.ssreflect.seq]
take_takel [in mathcomp.ssreflect.seq]
take_min [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]
take_traject [in mathcomp.ssreflect.path]
take_sorted [in mathcomp.ssreflect.path]
take_path [in mathcomp.ssreflect.path]
take_polyDMXn [in mathcomp.algebra.poly]
take_polyMXn_0 [in mathcomp.algebra.poly]
take_polyMXn [in mathcomp.algebra.poly]
take_poly0r [in mathcomp.algebra.poly]
take_poly0l [in mathcomp.algebra.poly]
take_poly_sum [in mathcomp.algebra.poly]
take_poly_is_linear [in mathcomp.algebra.poly]
take_polyZ [in mathcomp.algebra.poly]
take_polyD [in mathcomp.algebra.poly]
take_poly_id [in mathcomp.algebra.poly]
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]
telescope_sumn [in mathcomp.ssreflect.bigop]
telescope_sumn_in [in mathcomp.ssreflect.bigop]
telescope_big [in mathcomp.ssreflect.bigop]
textbook_triangular_sum [in mathcomp.ssreflect.binomial]
tfgraphK [in mathcomp.ssreflect.finfun]
tfgraph_inj [in mathcomp.ssreflect.finfun]
theadE [in mathcomp.ssreflect.tuple]
thinmxOver [in mathcomp.algebra.matrix]
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_cardMg [in mathcomp.fingroup.fingroup]
TI_pcoreC [in mathcomp.solvable.pgroup]
TI_Ohm1 [in mathcomp.solvable.abelian]
TI_cfker_irr [in mathcomp.character.character]
TI_center_nil [in mathcomp.solvable.nilpotent]
tnthP [in mathcomp.ssreflect.tuple]
tnthS [in mathcomp.ssreflect.tuple]
tnth_mktuple [in mathcomp.ssreflect.tuple]
tnth_ord_tuple [in mathcomp.ssreflect.tuple]
tnth_behead [in mathcomp.ssreflect.tuple]
tnth_nseq [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]
tofracXn [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_prime [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_on [in mathcomp.fingroup.perm]
tperm_proof [in mathcomp.fingroup.perm]
tperm_mxEsub [in mathcomp.algebra.matrix]
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]
trajectD [in mathcomp.ssreflect.path]
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]
trigmx_ind [in mathcomp.algebra.matrix]
trigsqmx_ind [in mathcomp.algebra.matrix]
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_quotient [in mathcomp.fingroup.quotient]
trivg_acomps [in mathcomp.solvable.jordanholder]
trivg_comps [in mathcomp.solvable.jordanholder]
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]
trivg_pcore_quotient [in mathcomp.solvable.pgroup]
trivg_Mho [in mathcomp.solvable.abelian]
trivg_exponent [in mathcomp.solvable.abelian]
trivg_Fitting [in mathcomp.solvable.maximal]
trivg_Phi [in mathcomp.solvable.maximal]
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]
trivIsetD [in mathcomp.ssreflect.finset]
trivIsetI [in mathcomp.ssreflect.finset]
trivIsetP [in mathcomp.ssreflect.finset]
trivIsetS [in mathcomp.ssreflect.finset]
trivIsetU [in mathcomp.ssreflect.finset]
trivIsetU1 [in mathcomp.ssreflect.finset]
trivIset1 [in mathcomp.ssreflect.finset]
trivMg [in mathcomp.fingroup.fingroup]
trivm_morphM [in mathcomp.fingroup.morphism]
triv_restr_perm [in mathcomp.fingroup.action]
triv_cprod [in mathcomp.fingroup.gproduct]
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_eq0 [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_mxsub [in mathcomp.algebra.matrix]
trmx_conform [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_up_log [in mathcomp.ssreflect.prime]
trunc_log2S [in mathcomp.ssreflect.prime]
trunc_log2_double [in mathcomp.ssreflect.prime]
trunc_logMp [in mathcomp.ssreflect.prime]
trunc_expnK [in mathcomp.ssreflect.prime]
trunc_lognn [in mathcomp.ssreflect.prime]
trunc_log_eq [in mathcomp.ssreflect.prime]
trunc_log1n [in mathcomp.ssreflect.prime]
trunc_log0n [in mathcomp.ssreflect.prime]
trunc_log_gt0 [in mathcomp.ssreflect.prime]
trunc_log_eq0 [in mathcomp.ssreflect.prime]
trunc_log_max [in mathcomp.ssreflect.prime]
trunc_log_ltn [in mathcomp.ssreflect.prime]
trunc_logP [in mathcomp.ssreflect.prime]
trunc_log_bounds [in mathcomp.ssreflect.prime]
trunc_log1 [in mathcomp.ssreflect.prime]
trunc_log0 [in mathcomp.ssreflect.prime]
tr_mxdiag [in mathcomp.algebra.matrix]
tr_submxcol [in mathcomp.algebra.matrix]
tr_submxrow [in mathcomp.algebra.matrix]
tr_submxblock [in mathcomp.algebra.matrix]
tr_mxcol [in mathcomp.algebra.matrix]
tr_mxrow [in mathcomp.algebra.matrix]
tr_mxblock [in mathcomp.algebra.matrix]
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_uniqP [in mathcomp.ssreflect.tuple]
tuple_eta [in mathcomp.ssreflect.tuple]
tuple_of_finfunK [in mathcomp.ssreflect.finfun]
tuple0 [in mathcomp.ssreflect.tuple]
tvalK [in mathcomp.ssreflect.tuple]

Global Index

_

(80254 entries)

Notation Index

H

J

T

W

X

Y

_

(1852 entries)

Binder Index

_

other

(48996 entries)

Module Index

H

J

K

L

W

X

Y

Z

_

other

(383 entries)

Variable Index

J

W

X

Y

_

other

(4219 entries)

Library Index

K

L

U

W

X

Y

_

other

(93 entries)

Lemma Index

Y

_

other

(14738 entries)

Constructor Index

J

K

W

Y

_

other

(223 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

D

H

J

K

L

W

X

Y

_

other

(452 entries)

Section Index

J

W

X

Y

_

other

(1431 entries)

Abbreviation Index

Y

_

other

(1169 entries)

Definition Index

Y

_

other

(6273 entries)

Record Index

D

H

J

K

L

W

X

Y

_

other

(248 entries)