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

(100113 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

(1864 entries)

Binder 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

(49278 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

(1631 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

(6978 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

(94 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

(14781 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

(222 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

(131 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

(2030 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

(2189 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

(1149 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

(19126 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

(565 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_take [abbreviation, 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]
tauS:264 [binder, in mathcomp.character.vcharacter]
tauS:575 [binder, in mathcomp.character.classfun]
tau:167 [binder, in mathcomp.character.classfun]
tau:171 [binder, in mathcomp.character.classfun]
tau:265 [binder, in mathcomp.character.vcharacter]
tau:266 [binder, in mathcomp.character.vcharacter]
tau:268 [binder, in mathcomp.character.vcharacter]
tau:269 [binder, in mathcomp.character.vcharacter]
tau:569 [binder, in mathcomp.character.classfun]
tau:572 [binder, in mathcomp.character.classfun]
tau:573 [binder, in mathcomp.character.classfun]
tau:576 [binder, in mathcomp.character.classfun]
tau:577 [binder, in mathcomp.character.classfun]
tau:579 [binder, in mathcomp.character.classfun]
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 [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 [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]
textbook_triangular_sum [lemma, in mathcomp.ssreflect.binomial]
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]
theta:440 [binder, in mathcomp.character.inertia]
theta:488 [binder, in mathcomp.character.inertia]
theta:499 [binder, in mathcomp.character.inertia]
theta:541 [binder, 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_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]
tofracX [abbreviation, 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]
toL:367 [binder, in mathcomp.field.fieldext]
toL:368 [binder, in mathcomp.field.fieldext]
toPF:366 [binder, in mathcomp.field.fieldext]
top:222 [binder, in mathcomp.ssreflect.order]
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_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]
to':31 [binder, in mathcomp.fingroup.action]
to:12 [binder, in mathcomp.fingroup.action]
to:158 [binder, in mathcomp.solvable.frobenius]
to:30 [binder, in mathcomp.fingroup.action]
to:37 [binder, in mathcomp.fingroup.action]
to:39 [binder, in mathcomp.fingroup.action]
to:39 [binder, in mathcomp.solvable.frobenius]
to:4 [binder, in mathcomp.fingroup.action]
to:43 [binder, in mathcomp.fingroup.action]
to:46 [binder, in mathcomp.fingroup.action]
to:463 [binder, in mathcomp.fingroup.action]
to:466 [binder, in mathcomp.fingroup.action]
to:5 [binder, in mathcomp.solvable.burnside_app]
to:53 [binder, in mathcomp.fingroup.action]
to:58 [binder, in mathcomp.fingroup.action]
to:588 [binder, in mathcomp.fingroup.gproduct]
to:592 [binder, in mathcomp.fingroup.gproduct]
to:62 [binder, in mathcomp.fingroup.action]
to:622 [binder, in mathcomp.fingroup.action]
to:626 [binder, in mathcomp.fingroup.action]
to:633 [binder, in mathcomp.fingroup.action]
to:637 [binder, in mathcomp.fingroup.action]
to:640 [binder, in mathcomp.fingroup.action]
to:643 [binder, in mathcomp.fingroup.action]
to:66 [binder, in mathcomp.fingroup.action]
to:71 [binder, in mathcomp.fingroup.action]
to:74 [binder, in mathcomp.fingroup.action]
to:8 [binder, in mathcomp.fingroup.action]
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]
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]
tP:158 [binder, in mathcomp.ssreflect.choice]
tP:161 [binder, in mathcomp.ssreflect.choice]
tP:164 [binder, in mathcomp.ssreflect.choice]
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_30.fK [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_30.g [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_30 [section, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_26.fK [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_26.g [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_26 [section, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_23.f_inj [variable, in mathcomp.ssreflect.eqtype]
TransferEqType.hb_instance_23 [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_31.fK [variable, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_31.g [variable, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_31 [section, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_28.fK [variable, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_28.g [variable, in mathcomp.ssreflect.fintype]
TransferFinType.hb_instance_28 [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]
triangular_sum [lemma, in mathcomp.ssreflect.binomial]
trigmx_ind [lemma, in mathcomp.algebra.matrix]
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]
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]
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]
truncC [abbreviation, in mathcomp.field.algC]
truncCD [abbreviation, in mathcomp.field.algC]
truncCK [abbreviation, in mathcomp.field.algC]
truncCM [abbreviation, in mathcomp.field.algC]
truncCX [abbreviation, in mathcomp.field.algC]
truncC_gt0 [abbreviation, in mathcomp.field.algC]
truncC_def [abbreviation, in mathcomp.field.algC]
truncC_itv [abbreviation, in mathcomp.field.algC]
truncC0 [abbreviation, in mathcomp.field.algC]
truncC0Pn [abbreviation, in mathcomp.field.algC]
truncC1 [abbreviation, in mathcomp.field.algC]
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]
trunc_subproof:47 [binder, in mathcomp.algebra.ssrnum]
trunc_subdef:43 [binder, in mathcomp.algebra.ssrnum]
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]
ts:219 [binder, in mathcomp.fingroup.perm]
ts:223 [binder, in mathcomp.fingroup.perm]
ts:228 [binder, in mathcomp.fingroup.perm]
ts:326 [binder, in mathcomp.field.closed_field]
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]
Tx:142 [binder, in mathcomp.character.inertia]
Tx:143 [binder, in mathcomp.character.inertia]
type [abbreviation, in mathcomp.field.finfield]
ty':2 [binder, in mathcomp.ssreflect.ssrAC]
ty:1 [binder, in mathcomp.ssreflect.ssrAC]
ty:5 [binder, in mathcomp.ssreflect.ssrAC]
ty:6 [binder, in mathcomp.ssreflect.ssrAC]
T' [abbreviation, in mathcomp.solvable.alt]
T':112 [binder, in mathcomp.fingroup.perm]
T':126 [binder, in mathcomp.ssreflect.ssrbool]
T':1280 [binder, in mathcomp.ssreflect.finset]
T':150 [binder, in mathcomp.ssreflect.fingraph]
T':155 [binder, in mathcomp.ssreflect.generic_quotient]
t':1638 [binder, in mathcomp.algebra.ssralg]
T':2036 [binder, in mathcomp.ssreflect.order]
T':214 [binder, in mathcomp.ssreflect.tuple]
T':2514 [binder, in mathcomp.ssreflect.seq]
T':2633 [binder, in mathcomp.ssreflect.seq]
T':2702 [binder, in mathcomp.ssreflect.order]
T':2733 [binder, in mathcomp.ssreflect.order]
T':2740 [binder, in mathcomp.ssreflect.order]
T':2756 [binder, in mathcomp.ssreflect.order]
T':2785 [binder, in mathcomp.ssreflect.order]
T':2804 [binder, in mathcomp.ssreflect.order]
T':2813 [binder, in mathcomp.ssreflect.order]
T':2824 [binder, in mathcomp.ssreflect.order]
T':2852 [binder, in mathcomp.ssreflect.order]
T':2861 [binder, in mathcomp.ssreflect.order]
T':2870 [binder, in mathcomp.ssreflect.order]
T':2881 [binder, in mathcomp.ssreflect.order]
T':2892 [binder, in mathcomp.ssreflect.order]
T':2899 [binder, in mathcomp.ssreflect.order]
T':2906 [binder, in mathcomp.ssreflect.order]
T':2913 [binder, in mathcomp.ssreflect.order]
T':2925 [binder, in mathcomp.ssreflect.order]
T':2959 [binder, in mathcomp.ssreflect.order]
T':2970 [binder, in mathcomp.ssreflect.order]
T':2981 [binder, in mathcomp.ssreflect.order]
T':2988 [binder, in mathcomp.ssreflect.order]
T':2995 [binder, in mathcomp.ssreflect.order]
T':358 [binder, in mathcomp.ssreflect.fintype]
T':4011 [binder, in mathcomp.ssreflect.order]
T':4016 [binder, in mathcomp.ssreflect.order]
T':4018 [binder, in mathcomp.ssreflect.order]
T':4020 [binder, in mathcomp.ssreflect.order]
T':4022 [binder, in mathcomp.ssreflect.order]
T':4064 [binder, in mathcomp.ssreflect.order]
T':4066 [binder, in mathcomp.ssreflect.order]
T':4083 [binder, in mathcomp.ssreflect.order]
T':4085 [binder, in mathcomp.ssreflect.order]
T':4087 [binder, in mathcomp.ssreflect.order]
T':4089 [binder, in mathcomp.ssreflect.order]
T':4093 [binder, in mathcomp.ssreflect.order]
T':4095 [binder, in mathcomp.ssreflect.order]
T':4097 [binder, in mathcomp.ssreflect.order]
T':4099 [binder, in mathcomp.ssreflect.order]
T':4101 [binder, in mathcomp.ssreflect.order]
T':4103 [binder, in mathcomp.ssreflect.order]
T':4105 [binder, in mathcomp.ssreflect.order]
T':4107 [binder, in mathcomp.ssreflect.order]
T':4109 [binder, in mathcomp.ssreflect.order]
T':4111 [binder, in mathcomp.ssreflect.order]
T':4113 [binder, in mathcomp.ssreflect.order]
T':4115 [binder, in mathcomp.ssreflect.order]
T':4117 [binder, in mathcomp.ssreflect.order]
T':4143 [binder, in mathcomp.ssreflect.order]
T':4160 [binder, in mathcomp.ssreflect.order]
T':4165 [binder, in mathcomp.ssreflect.order]
T':4167 [binder, in mathcomp.ssreflect.order]
T':4169 [binder, in mathcomp.ssreflect.order]
T':4171 [binder, in mathcomp.ssreflect.order]
T':4193 [binder, in mathcomp.ssreflect.order]
T':4202 [binder, in mathcomp.ssreflect.order]
T':4206 [binder, in mathcomp.ssreflect.order]
T':4208 [binder, in mathcomp.ssreflect.order]
T':4210 [binder, in mathcomp.ssreflect.order]
T':4621 [binder, in mathcomp.ssreflect.order]
T':4631 [binder, in mathcomp.ssreflect.order]
T':573 [binder, in mathcomp.ssreflect.fintype]
T':588 [binder, in mathcomp.ssreflect.fintype]
T':667 [binder, in mathcomp.ssreflect.path]
T':675 [binder, in mathcomp.ssreflect.fintype]
T':677 [binder, in mathcomp.ssreflect.path]
t':78 [binder, in mathcomp.solvable.primitive_action]
t':79 [binder, in mathcomp.solvable.primitive_action]
T':790 [binder, in mathcomp.ssreflect.path]
T':928 [binder, in mathcomp.ssreflect.fintype]
T':933 [binder, in mathcomp.ssreflect.fintype]
T':96 [binder, in mathcomp.ssreflect.generic_quotient]
T':996 [binder, in mathcomp.ssreflect.order]
t1:110 [binder, in mathcomp.solvable.burnside_app]
T1:1254 [binder, in mathcomp.algebra.mxalgebra]
T1:1293 [binder, in mathcomp.ssreflect.seq]
t1:13 [binder, in mathcomp.ssreflect.tuple]
t1:1588 [binder, in mathcomp.ssreflect.seq]
t1:1618 [binder, in mathcomp.algebra.ssralg]
t1:1636 [binder, in mathcomp.ssreflect.seq]
t1:1643 [binder, in mathcomp.ssreflect.seq]
t1:1651 [binder, in mathcomp.ssreflect.seq]
t1:167 [binder, in mathcomp.ssreflect.tuple]
T1:171 [binder, in mathcomp.ssreflect.choice]
T1:173 [binder, in mathcomp.ssreflect.choice]
T1:1969 [binder, in mathcomp.ssreflect.order]
t1:2070 [binder, in mathcomp.ssreflect.seq]
t1:2209 [binder, in mathcomp.ssreflect.seq]
t1:2223 [binder, in mathcomp.ssreflect.seq]
t1:2259 [binder, in mathcomp.ssreflect.seq]
t1:2395 [binder, in mathcomp.ssreflect.seq]
t1:2408 [binder, in mathcomp.ssreflect.seq]
T1:243 [binder, in mathcomp.ssreflect.choice]
T1:245 [binder, in mathcomp.ssreflect.choice]
T1:398 [binder, in mathcomp.ssreflect.eqtype]
T1:4 [binder, in mathcomp.field.closed_field]
T1:43 [binder, in mathcomp.field.closed_field]
t1:4358 [binder, in mathcomp.ssreflect.order]
t1:4365 [binder, in mathcomp.ssreflect.order]
t1:4375 [binder, in mathcomp.ssreflect.order]
t1:4379 [binder, in mathcomp.ssreflect.order]
t1:4383 [binder, in mathcomp.ssreflect.order]
t1:4386 [binder, in mathcomp.ssreflect.order]
t1:4390 [binder, in mathcomp.ssreflect.order]
t1:4393 [binder, in mathcomp.ssreflect.order]
t1:4395 [binder, in mathcomp.ssreflect.order]
t1:4399 [binder, in mathcomp.ssreflect.order]
t1:4417 [binder, in mathcomp.ssreflect.order]
t1:4421 [binder, in mathcomp.ssreflect.order]
t1:4424 [binder, in mathcomp.ssreflect.order]
t1:4426 [binder, in mathcomp.ssreflect.order]
t1:4428 [binder, in mathcomp.ssreflect.order]
t1:4492 [binder, in mathcomp.ssreflect.order]
t1:4498 [binder, in mathcomp.ssreflect.order]
t1:4504 [binder, in mathcomp.ssreflect.order]
T1:7 [binder, in mathcomp.field.closed_field]
t1:847 [binder, in mathcomp.ssreflect.seq]
t1:860 [binder, in mathcomp.ssreflect.seq]
T1:889 [binder, in mathcomp.ssreflect.order]
t2:111 [binder, in mathcomp.solvable.burnside_app]
T2:1255 [binder, in mathcomp.algebra.mxalgebra]
T2:1294 [binder, in mathcomp.ssreflect.seq]
t2:14 [binder, in mathcomp.ssreflect.tuple]
t2:1589 [binder, in mathcomp.ssreflect.seq]
t2:1637 [binder, in mathcomp.ssreflect.seq]
t2:1644 [binder, in mathcomp.ssreflect.seq]
t2:1652 [binder, in mathcomp.ssreflect.seq]
t2:168 [binder, in mathcomp.ssreflect.tuple]
T2:172 [binder, in mathcomp.ssreflect.choice]
T2:174 [binder, in mathcomp.ssreflect.choice]
T2:1970 [binder, in mathcomp.ssreflect.order]
t2:2071 [binder, in mathcomp.ssreflect.seq]
t2:2211 [binder, in mathcomp.ssreflect.seq]
t2:2225 [binder, in mathcomp.ssreflect.seq]
t2:2260 [binder, in mathcomp.ssreflect.seq]
t2:2397 [binder, in mathcomp.ssreflect.seq]
t2:2410 [binder, in mathcomp.ssreflect.seq]
T2:244 [binder, in mathcomp.ssreflect.choice]
T2:246 [binder, in mathcomp.ssreflect.choice]
T2:399 [binder, in mathcomp.ssreflect.eqtype]
t2:4359 [binder, in mathcomp.ssreflect.order]
t2:4366 [binder, in mathcomp.ssreflect.order]
t2:4376 [binder, in mathcomp.ssreflect.order]
t2:4380 [binder, in mathcomp.ssreflect.order]
t2:4384 [binder, in mathcomp.ssreflect.order]
t2:4387 [binder, in mathcomp.ssreflect.order]
t2:4389 [binder, in mathcomp.ssreflect.order]
t2:4394 [binder, in mathcomp.ssreflect.order]
t2:4396 [binder, in mathcomp.ssreflect.order]
t2:4400 [binder, in mathcomp.ssreflect.order]
t2:4418 [binder, in mathcomp.ssreflect.order]
t2:4422 [binder, in mathcomp.ssreflect.order]
t2:4425 [binder, in mathcomp.ssreflect.order]
t2:4427 [binder, in mathcomp.ssreflect.order]
t2:4429 [binder, in mathcomp.ssreflect.order]
t2:4493 [binder, in mathcomp.ssreflect.order]
t2:4499 [binder, in mathcomp.ssreflect.order]
T2:45 [binder, in mathcomp.field.closed_field]
t2:4505 [binder, in mathcomp.ssreflect.order]
T2:8 [binder, in mathcomp.field.closed_field]
t2:848 [binder, in mathcomp.ssreflect.seq]
t2:861 [binder, in mathcomp.ssreflect.seq]
T2:890 [binder, in mathcomp.ssreflect.order]
T:1 [binder, in mathcomp.ssreflect.generic_quotient]
T:1 [binder, in mathcomp.algebra.interval]
T:1 [binder, in mathcomp.algebra.ring_quotient]
T:1 [binder, in mathcomp.ssreflect.ssreflect]
T:1 [binder, in mathcomp.ssreflect.fingraph]
T:1 [binder, in mathcomp.ssreflect.fintype]
T:1 [binder, in mathcomp.ssreflect.bigop]
T:1 [binder, in mathcomp.ssreflect.eqtype]
t:10 [binder, in mathcomp.ssreflect.tuple]
T:10 [binder, in mathcomp.ssreflect.bigop]
T:100 [binder, in mathcomp.ssreflect.generic_quotient]
t:101 [binder, in mathcomp.ssreflect.tuple]
T:101 [binder, in mathcomp.ssreflect.bigop]
t:1025 [binder, in mathcomp.character.mxrepresentation]
T:103 [binder, in mathcomp.ssreflect.ssrbool]
t:104 [binder, in mathcomp.ssreflect.tuple]
t:107 [binder, in mathcomp.ssreflect.tuple]
t:108 [binder, in mathcomp.ssreflect.tuple]
t:108 [binder, in mathcomp.field.closed_field]
T:108 [binder, in mathcomp.ssreflect.ssrbool]
T:11 [binder, in mathcomp.fingroup.perm]
T:11 [binder, in mathcomp.field.algebraics_fundamentals]
T:11 [binder, in mathcomp.ssreflect.fintype]
t:110 [binder, in mathcomp.ssreflect.tuple]
T:110 [binder, in mathcomp.ssreflect.finfun]
T:111 [binder, in mathcomp.fingroup.perm]
T:111 [binder, in mathcomp.ssreflect.generic_quotient]
T:1112 [binder, in mathcomp.ssreflect.order]
T:1113 [binder, in mathcomp.ssreflect.order]
T:1114 [binder, in mathcomp.ssreflect.order]
T:1115 [binder, in mathcomp.ssreflect.order]
t:113 [binder, in mathcomp.ssreflect.tuple]
T:113 [binder, in mathcomp.algebra.ring_quotient]
T:113 [binder, in mathcomp.ssreflect.ssrbool]
T:1130 [binder, in mathcomp.ssreflect.order]
T:116 [binder, in mathcomp.ssreflect.generic_quotient]
t:116 [binder, in mathcomp.ssreflect.tuple]
T:117 [binder, in mathcomp.fingroup.perm]
T:118 [binder, in mathcomp.ssreflect.ssrbool]
T:118 [binder, in mathcomp.ssreflect.eqtype]
T:119 [binder, in mathcomp.ssreflect.generic_quotient]
t:119 [binder, in mathcomp.ssreflect.tuple]
t:12 [binder, in mathcomp.ssreflect.tuple]
T:12 [binder, in mathcomp.ssreflect.fintype]
T:1204 [binder, in mathcomp.ssreflect.seq]
T:1207 [binder, in mathcomp.ssreflect.seq]
T:121 [binder, in mathcomp.fingroup.perm]
T:121 [binder, in mathcomp.ssreflect.generic_quotient]
t:121 [binder, in mathcomp.ssreflect.tuple]
T:121 [binder, in mathcomp.ssreflect.bigop]
t:1210 [binder, in mathcomp.ssreflect.order]
T:1211 [binder, in mathcomp.ssreflect.seq]
T:123 [binder, in mathcomp.ssreflect.ssrbool]
t:124 [binder, in mathcomp.fingroup.perm]
t:124 [binder, in mathcomp.ssreflect.tuple]
T:124 [binder, in mathcomp.fingroup.action]
T:125 [binder, in mathcomp.ssreflect.order]
t:1257 [binder, in mathcomp.ssreflect.order]
t:126 [binder, in mathcomp.ssreflect.tuple]
T:126 [binder, in mathcomp.ssreflect.eqtype]
t:1269 [binder, in mathcomp.ssreflect.seq]
T:1269 [binder, in mathcomp.ssreflect.order]
T:127 [binder, in mathcomp.ssreflect.ssrbool]
t:1270 [binder, in mathcomp.ssreflect.seq]
t:1279 [binder, in mathcomp.ssreflect.seq]
T:129 [binder, in mathcomp.fingroup.perm]
t:129 [binder, in mathcomp.ssreflect.tuple]
t:1292 [binder, in mathcomp.ssreflect.seq]
T:1293 [binder, in mathcomp.algebra.mxalgebra]
t:13 [binder, in mathcomp.fingroup.presentation]
T:13 [binder, in mathcomp.ssreflect.eqtype]
T:1317 [binder, in mathcomp.ssreflect.seq]
T:132 [binder, in mathcomp.fingroup.perm]
T:1321 [binder, in mathcomp.ssreflect.seq]
t:1325 [binder, in mathcomp.ssreflect.order]
t:1329 [binder, in mathcomp.ssreflect.order]
t:133 [binder, in mathcomp.ssreflect.tuple]
t:1333 [binder, in mathcomp.ssreflect.order]
t:1337 [binder, in mathcomp.ssreflect.seq]
t:1337 [binder, in mathcomp.ssreflect.order]
T:135 [binder, in mathcomp.fingroup.perm]
T:136 [binder, in mathcomp.ssreflect.generic_quotient]
t:136 [binder, in mathcomp.ssreflect.tuple]
t:1361 [binder, in mathcomp.ssreflect.seq]
T:138 [binder, in mathcomp.ssreflect.generic_quotient]
T:14 [binder, in mathcomp.field.closed_field]
T:14 [binder, in mathcomp.ssreflect.order]
T:140 [binder, in mathcomp.ssreflect.generic_quotient]
T:141 [binder, in mathcomp.ssreflect.tuple]
T:141 [binder, in mathcomp.ssreflect.bigop]
t:142 [binder, in mathcomp.ssreflect.tuple]
T:142 [binder, in mathcomp.ssreflect.bigop]
T:144 [binder, in mathcomp.ssreflect.order]
T:144 [binder, in mathcomp.ssreflect.bigop]
t:1442 [binder, in mathcomp.ssreflect.seq]
T:145 [binder, in mathcomp.ssreflect.tuple]
t:146 [binder, in mathcomp.ssreflect.tuple]
T:146 [binder, in mathcomp.ssreflect.bigop]
t:147 [binder, in mathcomp.algebra.matrix]
t:147 [binder, in mathcomp.solvable.extremal]
T:1474 [binder, in mathcomp.ssreflect.seq]
T:148 [binder, in mathcomp.ssreflect.order]
t:15 [binder, in mathcomp.fingroup.perm]
t:15 [binder, in mathcomp.ssreflect.tuple]
T:15 [binder, in mathcomp.ssreflect.bigop]
t:150 [binder, in mathcomp.ssreflect.tuple]
t:150 [binder, in mathcomp.algebra.matrix]
T:1524 [binder, in mathcomp.ssreflect.finset]
t:153 [binder, in mathcomp.algebra.matrix]
T:153 [binder, in mathcomp.ssreflect.fintype]
T:1530 [binder, in mathcomp.ssreflect.finset]
t:155 [binder, in mathcomp.ssreflect.tuple]
T:156 [binder, in mathcomp.field.galois]
T:156 [binder, in mathcomp.ssreflect.fintype]
t:1561 [binder, in mathcomp.algebra.ssralg]
t:1566 [binder, in mathcomp.ssreflect.seq]
t:1571 [binder, in mathcomp.ssreflect.seq]
t:1571 [binder, in mathcomp.algebra.ssralg]
t:1577 [binder, in mathcomp.ssreflect.seq]
t:1578 [binder, in mathcomp.algebra.ssralg]
t:1579 [binder, in mathcomp.ssreflect.seq]
t:1580 [binder, in mathcomp.algebra.ssralg]
t:1581 [binder, in mathcomp.ssreflect.seq]
t:1583 [binder, in mathcomp.ssreflect.seq]
t:1585 [binder, in mathcomp.ssreflect.seq]
T:159 [binder, in mathcomp.ssreflect.fintype]
t:1593 [binder, in mathcomp.ssreflect.seq]
t:1597 [binder, in mathcomp.ssreflect.seq]
T:16 [binder, in mathcomp.solvable.alt]
t:16 [binder, in mathcomp.field.closed_field]
t:160 [binder, in mathcomp.ssreflect.tuple]
t:1600 [binder, in mathcomp.ssreflect.seq]
t:1601 [binder, in mathcomp.algebra.ssralg]
t:1604 [binder, in mathcomp.ssreflect.seq]
t:1606 [binder, in mathcomp.ssreflect.seq]
t:1606 [binder, in mathcomp.character.mxrepresentation]
t:1607 [binder, in mathcomp.algebra.ssralg]
t:1610 [binder, in mathcomp.algebra.ssralg]
t:1615 [binder, in mathcomp.algebra.ssralg]
t:1617 [binder, in mathcomp.ssreflect.seq]
t:1618 [binder, in mathcomp.character.mxrepresentation]
t:1626 [binder, in mathcomp.ssreflect.seq]
t:163 [binder, in mathcomp.ssreflect.tuple]
T:1633 [binder, in mathcomp.ssreflect.seq]
T:1642 [binder, in mathcomp.ssreflect.seq]
T:1648 [binder, in mathcomp.ssreflect.seq]
T:1653 [binder, in mathcomp.ssreflect.seq]
t:1655 [binder, in mathcomp.ssreflect.seq]
T:1657 [binder, in mathcomp.ssreflect.seq]
T:166 [binder, in mathcomp.ssreflect.order]
t:1676 [binder, in mathcomp.algebra.ssralg]
t:1678 [binder, in mathcomp.algebra.ssralg]
T:17 [binder, in mathcomp.ssreflect.eqtype]
T:170 [binder, in mathcomp.ssreflect.choice]
T:172 [binder, in mathcomp.ssreflect.binomial]
t:172 [binder, in mathcomp.ssreflect.tuple]
T:173 [binder, in mathcomp.ssreflect.order]
t:1733 [binder, in mathcomp.algebra.matrix]
t:174 [binder, in mathcomp.ssreflect.tuple]
t:174 [binder, in mathcomp.field.algebraics_fundamentals]
T:1742 [binder, in mathcomp.ssreflect.seq]
T:1746 [binder, in mathcomp.ssreflect.seq]
t:175 [binder, in mathcomp.ssreflect.binomial]
t:175 [binder, in mathcomp.fingroup.perm]
T:175 [binder, in mathcomp.ssreflect.choice]
T:1752 [binder, in mathcomp.ssreflect.seq]
T:1755 [binder, in mathcomp.ssreflect.seq]
t:176 [binder, in mathcomp.ssreflect.binomial]
t:176 [binder, in mathcomp.ssreflect.tuple]
T:176 [binder, in mathcomp.ssreflect.choice]
t:177 [binder, in mathcomp.ssreflect.binomial]
T:177 [binder, in mathcomp.ssreflect.order]
t:178 [binder, in mathcomp.ssreflect.binomial]
t:178 [binder, in mathcomp.ssreflect.tuple]
t:179 [binder, in mathcomp.ssreflect.binomial]
t:18 [binder, in mathcomp.ssreflect.tuple]
T:18 [binder, in mathcomp.ssreflect.order]
T:18 [binder, in mathcomp.ssreflect.ssrbool]
t:180 [binder, in mathcomp.fingroup.perm]
T:181 [binder, in mathcomp.ssreflect.binomial]
T:181 [binder, in mathcomp.ssreflect.choice]
t:181 [binder, in mathcomp.solvable.burnside_app]
t:184 [binder, in mathcomp.ssreflect.tuple]
T:185 [binder, in mathcomp.ssreflect.choice]
T:186 [binder, in mathcomp.ssreflect.tuple]
T:187 [binder, in mathcomp.ssreflect.binomial]
t:187 [binder, in mathcomp.solvable.burnside_app]
T:188 [binder, in mathcomp.ssreflect.tuple]
T:189 [binder, in mathcomp.ssreflect.binomial]
T:19 [binder, in mathcomp.ssreflect.bigop]
T:19 [binder, in mathcomp.ssreflect.eqtype]
T:190 [binder, in mathcomp.ssreflect.choice]
t:1912 [binder, in mathcomp.algebra.ssralg]
T:193 [binder, in mathcomp.ssreflect.choice]
t:197 [binder, in mathcomp.solvable.burnside_app]
t:1973 [binder, in mathcomp.ssreflect.order]
t:1976 [binder, in mathcomp.ssreflect.order]
t:1979 [binder, in mathcomp.ssreflect.order]
T:198 [binder, in mathcomp.ssreflect.choice]
t:1982 [binder, in mathcomp.ssreflect.order]
t:1985 [binder, in mathcomp.ssreflect.order]
t:1988 [binder, in mathcomp.ssreflect.order]
t:1991 [binder, in mathcomp.ssreflect.order]
t:1994 [binder, in mathcomp.ssreflect.order]
t:1995 [binder, in mathcomp.ssreflect.seq]
t:1997 [binder, in mathcomp.ssreflect.order]
T:2 [binder, in mathcomp.field.fieldext]
T:2 [binder, in mathcomp.ssreflect.order]
T:20 [binder, in mathcomp.ssreflect.prime]
t:2000 [binder, in mathcomp.ssreflect.order]
t:2002 [binder, in mathcomp.ssreflect.seq]
t:2004 [binder, in mathcomp.ssreflect.order]
t:2008 [binder, in mathcomp.ssreflect.order]
t:201 [binder, in mathcomp.fingroup.gproduct]
t:2010 [binder, in mathcomp.ssreflect.seq]
t:2012 [binder, in mathcomp.ssreflect.order]
t:2016 [binder, in mathcomp.ssreflect.order]
t:2020 [binder, in mathcomp.ssreflect.order]
t:2023 [binder, in mathcomp.ssreflect.seq]
t:2024 [binder, in mathcomp.ssreflect.order]
t:2028 [binder, in mathcomp.ssreflect.order]
t:2032 [binder, in mathcomp.ssreflect.order]
T:2035 [binder, in mathcomp.ssreflect.order]
t:204 [binder, in mathcomp.ssreflect.tuple]
t:2042 [binder, in mathcomp.ssreflect.seq]
T:2053 [binder, in mathcomp.algebra.ssralg]
t:2057 [binder, in mathcomp.ssreflect.seq]
t:207 [binder, in mathcomp.solvable.burnside_app]
T:2083 [binder, in mathcomp.ssreflect.order]
t:2084 [binder, in mathcomp.ssreflect.seq]
T:2091 [binder, in mathcomp.ssreflect.order]
T:21 [binder, in mathcomp.ssreflect.tuple]
t:2100 [binder, in mathcomp.ssreflect.seq]
t:2114 [binder, in mathcomp.ssreflect.seq]
T:212 [binder, in mathcomp.ssreflect.binomial]
T:2124 [binder, in mathcomp.ssreflect.order]
t:2127 [binder, in mathcomp.ssreflect.seq]
T:2137 [binder, in mathcomp.ssreflect.seq]
t:2143 [binder, in mathcomp.ssreflect.seq]
t:2157 [binder, in mathcomp.ssreflect.seq]
t:2163 [binder, in mathcomp.ssreflect.seq]
t:217 [binder, in mathcomp.ssreflect.binomial]
t:217 [binder, in mathcomp.fingroup.perm]
t:2175 [binder, in mathcomp.ssreflect.seq]
t:218 [binder, in mathcomp.ssreflect.binomial]
t:218 [binder, in mathcomp.solvable.burnside_app]
t:2187 [binder, in mathcomp.ssreflect.seq]
T:2188 [binder, in mathcomp.ssreflect.order]
T:2195 [binder, in mathcomp.ssreflect.order]
t:2197 [binder, in mathcomp.ssreflect.seq]
T:22 [binder, in mathcomp.algebra.ring_quotient]
T:22 [binder, in mathcomp.ssreflect.eqtype]
t:220 [binder, in mathcomp.fingroup.perm]
T:2203 [binder, in mathcomp.ssreflect.order]
t:221 [binder, in mathcomp.fingroup.perm]
T:221 [binder, in mathcomp.ssreflect.order]
t:222 [binder, in mathcomp.fingroup.perm]
T:2236 [binder, in mathcomp.ssreflect.order]
t:2237 [binder, in mathcomp.ssreflect.seq]
T:226 [binder, in mathcomp.ssreflect.choice]
t:227 [binder, in mathcomp.ssreflect.binomial]
t:2276 [binder, in mathcomp.ssreflect.seq]
T:228 [binder, in mathcomp.ssreflect.order]
t:229 [binder, in mathcomp.fingroup.perm]
T:229 [binder, in mathcomp.ssreflect.tuple]
t:2292 [binder, in mathcomp.ssreflect.seq]
T:23 [binder, in mathcomp.algebra.interval]
T:23 [binder, in mathcomp.ssreflect.tuple]
t:23 [binder, in mathcomp.solvable.primitive_action]
t:230 [binder, in mathcomp.ssreflect.binomial]
t:230 [binder, in mathcomp.fingroup.perm]
t:2302 [binder, in mathcomp.ssreflect.order]
t:2305 [binder, in mathcomp.ssreflect.seq]
t:2306 [binder, in mathcomp.ssreflect.order]
t:231 [binder, in mathcomp.fingroup.perm]
T:231 [binder, in mathcomp.ssreflect.tuple]
t:2318 [binder, in mathcomp.ssreflect.order]
t:232 [binder, in mathcomp.ssreflect.binomial]
T:232 [binder, in mathcomp.ssreflect.order]
t:2320 [binder, in mathcomp.ssreflect.seq]
t:233 [binder, in mathcomp.ssreflect.tuple]
t:2331 [binder, in mathcomp.algebra.ssrnum]
t:2332 [binder, in mathcomp.algebra.ssrnum]
t:2333 [binder, in mathcomp.ssreflect.seq]
T:2333 [binder, in mathcomp.ssreflect.order]
t:2337 [binder, in mathcomp.ssreflect.order]
t:2341 [binder, in mathcomp.ssreflect.order]
t:2344 [binder, in mathcomp.algebra.ssrnum]
t:2345 [binder, in mathcomp.algebra.ssrnum]
T:2346 [binder, in mathcomp.ssreflect.seq]
t:235 [binder, in mathcomp.ssreflect.binomial]
t:2353 [binder, in mathcomp.ssreflect.seq]
t:2353 [binder, in mathcomp.ssreflect.order]
t:236 [binder, in mathcomp.ssreflect.binomial]
T:236 [binder, in mathcomp.ssreflect.tuple]
T:236 [binder, in mathcomp.ssreflect.path]
T:236 [binder, in mathcomp.ssreflect.order]
t:2365 [binder, in mathcomp.ssreflect.seq]
t:2368 [binder, in mathcomp.algebra.ssrnum]
t:2369 [binder, in mathcomp.algebra.ssrnum]
t:237 [binder, in mathcomp.ssreflect.tuple]
t:2374 [binder, in mathcomp.ssreflect.seq]
t:238 [binder, in mathcomp.ssreflect.binomial]
T:238 [binder, in mathcomp.ssreflect.choice]
t:2384 [binder, in mathcomp.ssreflect.seq]
T:239 [binder, in mathcomp.ssreflect.tuple]
T:239 [binder, in mathcomp.ssreflect.choice]
T:239 [binder, in mathcomp.ssreflect.path]
T:24 [binder, in mathcomp.algebra.interval]
T:24 [binder, in mathcomp.ssreflect.finset]
t:240 [binder, in mathcomp.ssreflect.binomial]
T:240 [binder, in mathcomp.ssreflect.order]
t:2408 [binder, in mathcomp.algebra.ssrnum]
t:2409 [binder, in mathcomp.algebra.ssrnum]
t:241 [binder, in mathcomp.ssreflect.binomial]
T:241 [binder, in mathcomp.ssreflect.eqtype]
t:2416 [binder, in mathcomp.ssreflect.order]
T:242 [binder, in mathcomp.ssreflect.tuple]
t:2421 [binder, in mathcomp.ssreflect.seq]
t:244 [binder, in mathcomp.ssreflect.binomial]
T:244 [binder, in mathcomp.ssreflect.eqtype]
T:247 [binder, in mathcomp.ssreflect.choice]
T:2477 [binder, in mathcomp.ssreflect.seq]
T:2487 [binder, in mathcomp.ssreflect.seq]
T:2495 [binder, in mathcomp.ssreflect.seq]
t:25 [binder, in mathcomp.fingroup.perm]
T:25 [binder, in mathcomp.algebra.interval]
t:25 [binder, in mathcomp.ssreflect.tuple]
T:25 [binder, in mathcomp.ssreflect.prime]
T:25 [binder, in mathcomp.ssreflect.bigop]
T:2503 [binder, in mathcomp.ssreflect.seq]
T:2507 [binder, in mathcomp.ssreflect.seq]
T:2510 [binder, in mathcomp.ssreflect.order]
T:2513 [binder, in mathcomp.ssreflect.seq]
t:252 [binder, in mathcomp.ssreflect.binomial]
T:2521 [binder, in mathcomp.ssreflect.seq]
T:2530 [binder, in mathcomp.ssreflect.seq]
T:2530 [binder, in mathcomp.ssreflect.order]
T:2534 [binder, in mathcomp.ssreflect.order]
T:2537 [binder, in mathcomp.ssreflect.seq]
T:2539 [binder, in mathcomp.ssreflect.order]
T:2541 [binder, in mathcomp.ssreflect.seq]
T:2547 [binder, in mathcomp.ssreflect.order]
T:2549 [binder, in mathcomp.ssreflect.seq]
T:2552 [binder, in mathcomp.ssreflect.order]
T:2554 [binder, in mathcomp.ssreflect.seq]
T:2559 [binder, in mathcomp.ssreflect.seq]
T:2564 [binder, in mathcomp.ssreflect.seq]
T:2568 [binder, in mathcomp.ssreflect.order]
T:2570 [binder, in mathcomp.ssreflect.seq]
T:2576 [binder, in mathcomp.ssreflect.seq]
T:2594 [binder, in mathcomp.ssreflect.order]
T:2598 [binder, in mathcomp.ssreflect.order]
T:26 [binder, in mathcomp.algebra.interval]
T:26 [binder, in mathcomp.ssreflect.order]
T:26 [binder, in mathcomp.ssreflect.fintype]
T:261 [binder, in mathcomp.ssreflect.eqtype]
T:2612 [binder, in mathcomp.ssreflect.order]
T:2614 [binder, in mathcomp.algebra.matrix]
T:2615 [binder, in mathcomp.ssreflect.seq]
T:2620 [binder, in mathcomp.ssreflect.seq]
T:2624 [binder, in mathcomp.ssreflect.seq]
T:2629 [binder, in mathcomp.ssreflect.seq]
T:2632 [binder, in mathcomp.ssreflect.seq]
T:2634 [binder, in mathcomp.ssreflect.order]
T:2636 [binder, in mathcomp.algebra.matrix]
T:2637 [binder, in mathcomp.ssreflect.seq]
t:264 [binder, in mathcomp.ssreflect.binomial]
t:264 [binder, in mathcomp.fingroup.perm]
T:2640 [binder, in mathcomp.algebra.matrix]
t:265 [binder, in mathcomp.ssreflect.binomial]
T:2654 [binder, in mathcomp.ssreflect.order]
T:266 [binder, in mathcomp.ssreflect.eqtype]
T:2668 [binder, in mathcomp.ssreflect.order]
T:2676 [binder, in mathcomp.algebra.matrix]
t:268 [binder, in mathcomp.ssreflect.binomial]
T:2690 [binder, in mathcomp.ssreflect.order]
T:27 [binder, in mathcomp.ssreflect.generic_quotient]
T:27 [binder, in mathcomp.algebra.interval]
T:27 [binder, in mathcomp.ssreflect.eqtype]
T:2700 [binder, in mathcomp.ssreflect.order]
T:2712 [binder, in mathcomp.ssreflect.order]
t:2715 [binder, in mathcomp.ssreflect.seq]
t:2716 [binder, in mathcomp.ssreflect.seq]
t:272 [binder, in mathcomp.ssreflect.binomial]
t:2724 [binder, in mathcomp.ssreflect.seq]
t:2725 [binder, in mathcomp.ssreflect.seq]
t:2730 [binder, in mathcomp.ssreflect.seq]
T:2731 [binder, in mathcomp.ssreflect.order]
t:2736 [binder, in mathcomp.ssreflect.seq]
t:2737 [binder, in mathcomp.ssreflect.seq]
T:2738 [binder, in mathcomp.ssreflect.order]
t:2740 [binder, in mathcomp.ssreflect.seq]
t:2742 [binder, in mathcomp.ssreflect.seq]
t:2743 [binder, in mathcomp.ssreflect.seq]
t:2748 [binder, in mathcomp.ssreflect.seq]
t:2750 [binder, in mathcomp.ssreflect.seq]
T:2754 [binder, in mathcomp.ssreflect.order]
t:2757 [binder, in mathcomp.ssreflect.seq]
t:276 [binder, in mathcomp.ssreflect.binomial]
T:2769 [binder, in mathcomp.ssreflect.order]
t:277 [binder, in mathcomp.ssreflect.binomial]
T:277 [binder, in mathcomp.fingroup.action]
t:277 [binder, in mathcomp.solvable.extremal]
T:278 [binder, in mathcomp.fingroup.action]
T:2783 [binder, in mathcomp.ssreflect.order]
T:279 [binder, in mathcomp.fingroup.action]
t:279 [binder, in mathcomp.solvable.extremal]
T:2798 [binder, in mathcomp.ssreflect.order]
t:28 [binder, in mathcomp.fingroup.perm]
T:28 [binder, in mathcomp.algebra.interval]
T:28 [binder, in mathcomp.ssreflect.fintype]
T:280 [binder, in mathcomp.fingroup.action]
T:2802 [binder, in mathcomp.ssreflect.order]
T:281 [binder, in mathcomp.fingroup.action]
T:2811 [binder, in mathcomp.ssreflect.order]
T:2822 [binder, in mathcomp.ssreflect.order]
T:284 [binder, in mathcomp.ssreflect.order]
t:284 [binder, in mathcomp.solvable.extremal]
T:2843 [binder, in mathcomp.ssreflect.bigop]
t:285 [binder, in mathcomp.solvable.extremal]
T:2850 [binder, in mathcomp.ssreflect.order]
T:2859 [binder, in mathcomp.ssreflect.order]
T:2861 [binder, in mathcomp.algebra.matrix]
T:2868 [binder, in mathcomp.ssreflect.order]
t:287 [binder, in mathcomp.field.algebraics_fundamentals]
t:287 [binder, in mathcomp.solvable.extremal]
T:2873 [binder, in mathcomp.algebra.matrix]
T:2879 [binder, in mathcomp.ssreflect.order]
T:289 [binder, in mathcomp.ssreflect.order]
t:289 [binder, in mathcomp.solvable.extremal]
T:2890 [binder, in mathcomp.ssreflect.order]
T:2897 [binder, in mathcomp.ssreflect.order]
T:2898 [binder, in mathcomp.algebra.matrix]
T:29 [binder, in mathcomp.algebra.interval]
T:29 [binder, in mathcomp.field.closed_field]
T:2904 [binder, in mathcomp.ssreflect.order]
T:2911 [binder, in mathcomp.ssreflect.order]
T:2915 [binder, in mathcomp.algebra.matrix]
t:292 [binder, in mathcomp.solvable.extremal]
T:2923 [binder, in mathcomp.algebra.matrix]
T:2923 [binder, in mathcomp.ssreflect.order]
T:293 [binder, in mathcomp.ssreflect.order]
t:294 [binder, in mathcomp.solvable.extremal]
t:295 [binder, in mathcomp.solvable.extremal]
T:2957 [binder, in mathcomp.ssreflect.order]
t:296 [binder, in mathcomp.solvable.extremal]
T:2968 [binder, in mathcomp.ssreflect.order]
T:297 [binder, in mathcomp.ssreflect.order]
t:297 [binder, in mathcomp.solvable.extremal]
T:2979 [binder, in mathcomp.ssreflect.order]
t:298 [binder, in mathcomp.solvable.extremal]
T:2986 [binder, in mathcomp.ssreflect.order]
t:299 [binder, in mathcomp.solvable.extremal]
T:2993 [binder, in mathcomp.ssreflect.order]
T:30 [binder, in mathcomp.algebra.interval]
T:30 [binder, in mathcomp.ssreflect.order]
T:30 [binder, in mathcomp.ssreflect.fintype]
t:300 [binder, in mathcomp.solvable.extremal]
T:301 [binder, in mathcomp.ssreflect.order]
t:302 [binder, in mathcomp.solvable.extremal]
t:303 [binder, in mathcomp.field.closed_field]
T:3033 [binder, in mathcomp.ssreflect.order]
T:3040 [binder, in mathcomp.ssreflect.order]
T:3047 [binder, in mathcomp.ssreflect.order]
T:3054 [binder, in mathcomp.ssreflect.order]
T:3061 [binder, in mathcomp.ssreflect.order]
T:3066 [binder, in mathcomp.ssreflect.order]
T:3071 [binder, in mathcomp.ssreflect.order]
T:3076 [binder, in mathcomp.ssreflect.order]
t:308 [binder, in mathcomp.field.closed_field]
t:308 [binder, in mathcomp.solvable.extremal]
T:3081 [binder, in mathcomp.ssreflect.order]
T:3086 [binder, in mathcomp.ssreflect.order]
t:309 [binder, in mathcomp.fingroup.perm]
t:309 [binder, in mathcomp.solvable.extremal]
T:3091 [binder, in mathcomp.ssreflect.order]
T:3096 [binder, in mathcomp.ssreflect.order]
T:31 [binder, in mathcomp.ssreflect.generic_quotient]
t:31 [binder, in mathcomp.ssreflect.tuple]
t:31 [binder, in mathcomp.ssreflect.choice]
t:31 [binder, in mathcomp.solvable.primitive_action]
T:31 [binder, in mathcomp.ssreflect.prime]
t:310 [binder, in mathcomp.solvable.extremal]
T:3101 [binder, in mathcomp.ssreflect.order]
T:3109 [binder, in mathcomp.ssreflect.order]
T:3115 [binder, in mathcomp.ssreflect.order]
t:312 [binder, in mathcomp.field.closed_field]
T:312 [binder, in mathcomp.ssreflect.order]
t:312 [binder, in mathcomp.solvable.extremal]
T:3125 [binder, in mathcomp.ssreflect.order]
t:315 [binder, in mathcomp.solvable.extremal]
T:316 [binder, in mathcomp.ssreflect.order]
T:316 [binder, in mathcomp.ssreflect.eqtype]
T:3163 [binder, in mathcomp.ssreflect.order]
T:3178 [binder, in mathcomp.ssreflect.order]
t:318 [binder, in mathcomp.solvable.extremal]
T:3185 [binder, in mathcomp.ssreflect.order]
T:3194 [binder, in mathcomp.ssreflect.order]
t:32 [binder, in mathcomp.solvable.primitive_action]
T:32 [binder, in mathcomp.ssreflect.bigop]
t:320 [binder, in mathcomp.solvable.extremal]
T:3204 [binder, in mathcomp.ssreflect.order]
t:321 [binder, in mathcomp.solvable.extremal]
T:3214 [binder, in mathcomp.ssreflect.order]
T:3219 [binder, in mathcomp.ssreflect.order]
t:322 [binder, in mathcomp.solvable.extremal]
T:323 [binder, in mathcomp.ssreflect.order]
t:323 [binder, in mathcomp.solvable.extremal]
T:3234 [binder, in mathcomp.ssreflect.order]
t:324 [binder, in mathcomp.solvable.extremal]
T:3249 [binder, in mathcomp.ssreflect.order]
T:3256 [binder, in mathcomp.ssreflect.order]
T:3263 [binder, in mathcomp.ssreflect.order]
T:327 [binder, in mathcomp.ssreflect.order]
t:327 [binder, in mathcomp.solvable.extremal]
T:327 [binder, in mathcomp.ssreflect.eqtype]
T:3270 [binder, in mathcomp.ssreflect.order]
T:3277 [binder, in mathcomp.ssreflect.order]
T:3284 [binder, in mathcomp.ssreflect.order]
T:3291 [binder, in mathcomp.ssreflect.order]
T:3298 [binder, in mathcomp.ssreflect.order]
t:33 [binder, in mathcomp.fingroup.perm]
T:330 [binder, in mathcomp.ssreflect.eqtype]
T:3305 [binder, in mathcomp.ssreflect.order]
T:3312 [binder, in mathcomp.ssreflect.order]
T:3319 [binder, in mathcomp.ssreflect.order]
T:332 [binder, in mathcomp.ssreflect.order]
t:332 [binder, in mathcomp.solvable.extremal]
T:332 [binder, in mathcomp.ssreflect.eqtype]
T:3326 [binder, in mathcomp.ssreflect.order]
T:3333 [binder, in mathcomp.ssreflect.order]
T:3340 [binder, in mathcomp.ssreflect.order]
T:3347 [binder, in mathcomp.ssreflect.order]
T:3354 [binder, in mathcomp.ssreflect.order]
T:336 [binder, in mathcomp.ssreflect.order]
T:3361 [binder, in mathcomp.ssreflect.order]
T:3366 [binder, in mathcomp.ssreflect.order]
t:337 [binder, in mathcomp.solvable.extremal]
T:3371 [binder, in mathcomp.ssreflect.order]
t:338 [binder, in mathcomp.field.closed_field]
T:3383 [binder, in mathcomp.ssreflect.order]
T:34 [binder, in mathcomp.ssreflect.generic_quotient]
t:34 [binder, in mathcomp.solvable.primitive_action]
T:34 [binder, in mathcomp.ssreflect.fintype]
T:340 [binder, in mathcomp.ssreflect.order]
T:340 [binder, in mathcomp.ssreflect.eqtype]
T:3405 [binder, in mathcomp.ssreflect.order]
T:3417 [binder, in mathcomp.ssreflect.order]
t:342 [binder, in mathcomp.solvable.extremal]
T:3427 [binder, in mathcomp.ssreflect.order]
t:343 [binder, in mathcomp.field.closed_field]
T:3438 [binder, in mathcomp.ssreflect.order]
T:344 [binder, in mathcomp.ssreflect.order]
t:344 [binder, in mathcomp.solvable.extremal]
T:3445 [binder, in mathcomp.ssreflect.order]
t:345 [binder, in mathcomp.solvable.extremal]
T:3452 [binder, in mathcomp.ssreflect.order]
T:3459 [binder, in mathcomp.ssreflect.order]
t:346 [binder, in mathcomp.solvable.extremal]
T:3466 [binder, in mathcomp.ssreflect.order]
t:347 [binder, in mathcomp.solvable.extremal]
T:3471 [binder, in mathcomp.ssreflect.order]
T:348 [binder, in mathcomp.ssreflect.order]
t:348 [binder, in mathcomp.solvable.extremal]
T:3482 [binder, in mathcomp.ssreflect.order]
t:349 [binder, in mathcomp.solvable.extremal]
T:3495 [binder, in mathcomp.ssreflect.order]
t:35 [binder, in mathcomp.ssreflect.choice]
T:35 [binder, in mathcomp.field.closed_field]
T:3508 [binder, in mathcomp.ssreflect.order]
T:3518 [binder, in mathcomp.ssreflect.order]
T:352 [binder, in mathcomp.ssreflect.order]
T:3529 [binder, in mathcomp.ssreflect.order]
T:3536 [binder, in mathcomp.ssreflect.order]
T:3543 [binder, in mathcomp.ssreflect.order]
T:355 [binder, in mathcomp.ssreflect.tuple]
T:355 [binder, in mathcomp.ssreflect.order]
T:3550 [binder, in mathcomp.ssreflect.order]
T:3557 [binder, in mathcomp.ssreflect.order]
T:3562 [binder, in mathcomp.ssreflect.order]
T:357 [binder, in mathcomp.ssreflect.tuple]
T:357 [binder, in mathcomp.ssreflect.fintype]
T:3573 [binder, in mathcomp.ssreflect.order]
t:358 [binder, in mathcomp.ssreflect.tuple]
T:3586 [binder, in mathcomp.ssreflect.order]
T:3599 [binder, in mathcomp.ssreflect.order]
T:360 [binder, in mathcomp.ssreflect.tuple]
T:3609 [binder, in mathcomp.ssreflect.order]
T:3616 [binder, in mathcomp.ssreflect.order]
T:3621 [binder, in mathcomp.ssreflect.order]
T:363 [binder, in mathcomp.ssreflect.tuple]
T:3633 [binder, in mathcomp.ssreflect.order]
T:364 [binder, in mathcomp.ssreflect.eqtype]
T:3643 [binder, in mathcomp.ssreflect.order]
T:365 [binder, in mathcomp.ssreflect.tuple]
T:3657 [binder, in mathcomp.ssreflect.order]
T:3667 [binder, in mathcomp.ssreflect.order]
T:367 [binder, in mathcomp.ssreflect.tuple]
T:367 [binder, in mathcomp.ssreflect.eqtype]
T:3674 [binder, in mathcomp.ssreflect.order]
T:3684 [binder, in mathcomp.ssreflect.order]
T:3694 [binder, in mathcomp.ssreflect.order]
t:37 [binder, in mathcomp.ssreflect.tuple]
T:3704 [binder, in mathcomp.ssreflect.order]
T:371 [binder, in mathcomp.ssreflect.tuple]
T:3714 [binder, in mathcomp.ssreflect.order]
T:3724 [binder, in mathcomp.ssreflect.order]
t:373 [binder, in mathcomp.ssreflect.tuple]
T:373 [binder, in mathcomp.ssreflect.eqtype]
T:3734 [binder, in mathcomp.ssreflect.order]
T:3740 [binder, in mathcomp.ssreflect.order]
T:375 [binder, in mathcomp.ssreflect.tuple]
T:377 [binder, in mathcomp.ssreflect.tuple]
T:377 [binder, in mathcomp.ssreflect.eqtype]
T:38 [binder, in mathcomp.ssreflect.finset]
T:381 [binder, in mathcomp.ssreflect.tuple]
T:382 [binder, in mathcomp.ssreflect.eqtype]
T:383 [binder, in mathcomp.ssreflect.tuple]
T:385 [binder, in mathcomp.ssreflect.tuple]
t:388 [binder, in mathcomp.solvable.extremal]
t:393 [binder, in mathcomp.ssreflect.seq]
t:396 [binder, in mathcomp.ssreflect.seq]
t:399 [binder, in mathcomp.ssreflect.seq]
T:4 [binder, in mathcomp.algebra.interval]
T:4 [binder, in mathcomp.ssreflect.fintype]
T:40 [binder, in mathcomp.field.closed_field]
T:40 [binder, in mathcomp.ssreflect.bigop]
T:4010 [binder, in mathcomp.ssreflect.order]
T:4015 [binder, in mathcomp.ssreflect.order]
T:4017 [binder, in mathcomp.ssreflect.order]
T:4019 [binder, in mathcomp.ssreflect.order]
T:4021 [binder, in mathcomp.ssreflect.order]
t:405 [binder, in mathcomp.ssreflect.seq]
T:4063 [binder, in mathcomp.ssreflect.order]
T:4065 [binder, in mathcomp.ssreflect.order]
T:4082 [binder, in mathcomp.ssreflect.order]
T:4084 [binder, in mathcomp.ssreflect.order]
T:4086 [binder, in mathcomp.ssreflect.order]
T:4088 [binder, in mathcomp.ssreflect.order]
T:4092 [binder, in mathcomp.ssreflect.order]
T:4094 [binder, in mathcomp.ssreflect.order]
T:4096 [binder, in mathcomp.ssreflect.order]
T:4098 [binder, in mathcomp.ssreflect.order]
t:41 [binder, in mathcomp.ssreflect.tuple]
T:41 [binder, in mathcomp.ssreflect.order]
T:4100 [binder, in mathcomp.ssreflect.order]
T:4102 [binder, in mathcomp.ssreflect.order]
T:4104 [binder, in mathcomp.ssreflect.order]
T:4106 [binder, in mathcomp.ssreflect.order]
T:4108 [binder, in mathcomp.ssreflect.order]
T:4110 [binder, in mathcomp.ssreflect.order]
T:4112 [binder, in mathcomp.ssreflect.order]
T:4114 [binder, in mathcomp.ssreflect.order]
T:4116 [binder, in mathcomp.ssreflect.order]
t:4122 [binder, in mathcomp.ssreflect.order]
t:4129 [binder, in mathcomp.ssreflect.order]
T:4142 [binder, in mathcomp.ssreflect.order]
t:4144 [binder, in mathcomp.ssreflect.order]
t:4147 [binder, in mathcomp.ssreflect.order]
t:4148 [binder, in mathcomp.ssreflect.order]
t:4149 [binder, in mathcomp.ssreflect.order]
t:4152 [binder, in mathcomp.ssreflect.order]
t:4154 [binder, in mathcomp.ssreflect.order]
t:4155 [binder, in mathcomp.ssreflect.order]
t:4157 [binder, in mathcomp.ssreflect.order]
T:4159 [binder, in mathcomp.ssreflect.order]
T:4164 [binder, in mathcomp.ssreflect.order]
T:4166 [binder, in mathcomp.ssreflect.order]
T:4168 [binder, in mathcomp.ssreflect.order]
T:4170 [binder, in mathcomp.ssreflect.order]
T:4192 [binder, in mathcomp.ssreflect.order]
t:42 [binder, in mathcomp.solvable.primitive_action]
T:42 [binder, in mathcomp.algebra.ring_quotient]
T:42 [binder, in mathcomp.fingroup.fingroup]
T:4201 [binder, in mathcomp.ssreflect.order]
T:4205 [binder, in mathcomp.ssreflect.order]
T:4207 [binder, in mathcomp.ssreflect.order]
T:4209 [binder, in mathcomp.ssreflect.order]
T:4212 [binder, in mathcomp.ssreflect.order]
T:4215 [binder, in mathcomp.ssreflect.order]
T:4216 [binder, in mathcomp.ssreflect.order]
T:4217 [binder, in mathcomp.ssreflect.order]
T:427 [binder, in mathcomp.ssreflect.seq]
T:4270 [binder, in mathcomp.ssreflect.order]
T:4271 [binder, in mathcomp.ssreflect.order]
T:4272 [binder, in mathcomp.ssreflect.order]
T:4274 [binder, in mathcomp.ssreflect.order]
T:4277 [binder, in mathcomp.ssreflect.order]
T:4278 [binder, in mathcomp.ssreflect.order]
T:4279 [binder, in mathcomp.ssreflect.order]
t:43 [binder, in mathcomp.ssreflect.choice]
t:43 [binder, in mathcomp.solvable.primitive_action]
T:43 [binder, in mathcomp.fingroup.fingroup]
t:432 [binder, in mathcomp.ssreflect.seq]
T:4337 [binder, in mathcomp.ssreflect.order]
T:4339 [binder, in mathcomp.ssreflect.order]
t:434 [binder, in mathcomp.ssreflect.seq]
T:4340 [binder, in mathcomp.ssreflect.order]
T:4341 [binder, in mathcomp.ssreflect.order]
T:4344 [binder, in mathcomp.ssreflect.order]
T:4348 [binder, in mathcomp.ssreflect.order]
T:4349 [binder, in mathcomp.ssreflect.order]
T:4350 [binder, in mathcomp.ssreflect.order]
T:4351 [binder, in mathcomp.ssreflect.order]
T:4353 [binder, in mathcomp.ssreflect.order]
T:4355 [binder, in mathcomp.ssreflect.order]
T:4357 [binder, in mathcomp.ssreflect.order]
T:4364 [binder, in mathcomp.ssreflect.order]
T:439 [binder, in mathcomp.ssreflect.ssrnat]
T:440 [binder, in mathcomp.ssreflect.order]
t:4405 [binder, in mathcomp.ssreflect.order]
t:4408 [binder, in mathcomp.ssreflect.order]
t:441 [binder, in mathcomp.character.inertia]
T:4412 [binder, in mathcomp.ssreflect.order]
T:4414 [binder, in mathcomp.ssreflect.order]
t:4434 [binder, in mathcomp.ssreflect.order]
t:4435 [binder, in mathcomp.ssreflect.order]
t:4437 [binder, in mathcomp.ssreflect.order]
t:4438 [binder, in mathcomp.ssreflect.order]
T:4442 [binder, in mathcomp.ssreflect.order]
T:4444 [binder, in mathcomp.ssreflect.order]
T:4446 [binder, in mathcomp.ssreflect.order]
T:4448 [binder, in mathcomp.ssreflect.order]
T:4451 [binder, in mathcomp.ssreflect.order]
T:4453 [binder, in mathcomp.ssreflect.order]
T:4455 [binder, in mathcomp.ssreflect.order]
T:4457 [binder, in mathcomp.ssreflect.order]
T:4459 [binder, in mathcomp.ssreflect.order]
T:4461 [binder, in mathcomp.ssreflect.order]
T:4463 [binder, in mathcomp.ssreflect.order]
T:4465 [binder, in mathcomp.ssreflect.order]
T:4467 [binder, in mathcomp.ssreflect.order]
T:4469 [binder, in mathcomp.ssreflect.order]
T:4471 [binder, in mathcomp.ssreflect.order]
T:4473 [binder, in mathcomp.ssreflect.order]
T:4475 [binder, in mathcomp.ssreflect.order]
T:4478 [binder, in mathcomp.ssreflect.order]
T:4482 [binder, in mathcomp.ssreflect.order]
T:4483 [binder, in mathcomp.ssreflect.order]
T:4484 [binder, in mathcomp.ssreflect.order]
T:4485 [binder, in mathcomp.ssreflect.order]
T:4487 [binder, in mathcomp.ssreflect.order]
T:4489 [binder, in mathcomp.ssreflect.order]
t:449 [binder, in mathcomp.ssreflect.order]
t:449 [binder, in mathcomp.algebra.ssrnum]
T:4491 [binder, in mathcomp.ssreflect.order]
T:4497 [binder, in mathcomp.ssreflect.order]
T:45 [binder, in mathcomp.ssreflect.bigop]
T:4503 [binder, in mathcomp.ssreflect.order]
T:451 [binder, in mathcomp.fingroup.action]
T:4510 [binder, in mathcomp.ssreflect.order]
T:4512 [binder, in mathcomp.ssreflect.order]
T:4514 [binder, in mathcomp.ssreflect.order]
t:4517 [binder, in mathcomp.ssreflect.order]
t:4520 [binder, in mathcomp.ssreflect.order]
T:4523 [binder, in mathcomp.ssreflect.order]
T:4526 [binder, in mathcomp.ssreflect.order]
T:4528 [binder, in mathcomp.ssreflect.order]
t:453 [binder, in mathcomp.algebra.ssrnum]
T:4530 [binder, in mathcomp.ssreflect.order]
T:4532 [binder, in mathcomp.ssreflect.order]
T:4534 [binder, in mathcomp.ssreflect.order]
T:4536 [binder, in mathcomp.ssreflect.order]
T:4538 [binder, in mathcomp.ssreflect.order]
T:4540 [binder, in mathcomp.ssreflect.order]
T:4544 [binder, in mathcomp.ssreflect.order]
T:4546 [binder, in mathcomp.ssreflect.order]
T:4566 [binder, in mathcomp.ssreflect.order]
T:4568 [binder, in mathcomp.ssreflect.order]
t:457 [binder, in mathcomp.algebra.ssrnum]
T:4570 [binder, in mathcomp.ssreflect.order]
T:4590 [binder, in mathcomp.ssreflect.order]
T:46 [binder, in mathcomp.fingroup.fingroup]
t:461 [binder, in mathcomp.algebra.ssrnum]
T:4620 [binder, in mathcomp.ssreflect.order]
T:4630 [binder, in mathcomp.ssreflect.order]
t:465 [binder, in mathcomp.algebra.ssrnum]
t:469 [binder, in mathcomp.algebra.ssrnum]
t:47 [binder, in mathcomp.ssreflect.choice]
t:47 [binder, in mathcomp.solvable.primitive_action]
T:47 [binder, in mathcomp.ssreflect.order]
t:472 [binder, in mathcomp.fingroup.gproduct]
t:473 [binder, in mathcomp.algebra.ssrnum]
t:477 [binder, in mathcomp.algebra.ssrnum]
t:480 [binder, in mathcomp.character.inertia]
t:494 [binder, in mathcomp.ssreflect.path]
t:5 [binder, in mathcomp.ssreflect.tuple]
t:5 [binder, in mathcomp.fingroup.presentation]
T:5 [binder, in mathcomp.ssreflect.eqtype]
t:50 [binder, in mathcomp.solvable.primitive_action]
T:50 [binder, in mathcomp.field.closed_field]
t:505 [binder, in mathcomp.ssreflect.seq]
t:509 [binder, in mathcomp.ssreflect.seq]
t:51 [binder, in mathcomp.ssreflect.choice]
T:516 [binder, in mathcomp.ssreflect.path]
t:52 [binder, in mathcomp.solvable.extremal]
T:53 [binder, in mathcomp.solvable.alt]
t:53 [binder, in mathcomp.ssreflect.tuple]
t:53 [binder, in mathcomp.field.closed_field]
T:53 [binder, in mathcomp.ssreflect.fintype]
T:539 [binder, in mathcomp.ssreflect.path]
t:54 [binder, in mathcomp.fingroup.perm]
t:54 [binder, in mathcomp.solvable.primitive_action]
t:54 [binder, in mathcomp.field.separable]
T:54 [binder, in mathcomp.ssreflect.order]
T:54 [binder, in mathcomp.ssreflect.bigop]
t:540 [binder, in mathcomp.character.inertia]
t:542 [binder, in mathcomp.character.character]
T:545 [binder, in mathcomp.ssreflect.path]
t:55 [binder, in mathcomp.ssreflect.tuple]
t:55 [binder, in mathcomp.solvable.burnside_app]
T:55 [binder, in mathcomp.ssreflect.fintype]
T:550 [binder, in mathcomp.ssreflect.path]
t:553 [binder, in mathcomp.character.character]
T:554 [binder, in mathcomp.ssreflect.path]
t:559 [binder, in mathcomp.character.character]
t:57 [binder, in mathcomp.solvable.primitive_action]
T:572 [binder, in mathcomp.ssreflect.fintype]
T:574 [binder, in mathcomp.ssreflect.path]
T:58 [binder, in mathcomp.ssreflect.choice]
T:580 [binder, in mathcomp.ssreflect.path]
T:586 [binder, in mathcomp.ssreflect.path]
T:587 [binder, in mathcomp.ssreflect.fintype]
t:59 [binder, in mathcomp.ssreflect.tuple]
T:59 [binder, in mathcomp.ssreflect.choice]
T:593 [binder, in mathcomp.ssreflect.path]
T:599 [binder, in mathcomp.ssreflect.path]
T:6 [binder, in mathcomp.solvable.alt]
t:6 [binder, in mathcomp.ssreflect.tuple]
T:6 [binder, in mathcomp.ssreflect.finset]
T:6 [binder, in mathcomp.ssreflect.bigop]
T:60 [binder, in mathcomp.ssreflect.bigop]
T:619 [binder, in mathcomp.ssreflect.ssrnat]
t:633 [binder, in mathcomp.ssreflect.path]
t:635 [binder, in mathcomp.ssreflect.path]
t:637 [binder, in mathcomp.ssreflect.path]
t:638 [binder, in mathcomp.ssreflect.seq]
T:639 [binder, in mathcomp.algebra.ssralg]
T:64 [binder, in mathcomp.algebra.ring_quotient]
T:64 [binder, in mathcomp.ssreflect.prime]
T:640 [binder, in mathcomp.algebra.ssralg]
t:644 [binder, in mathcomp.ssreflect.path]
t:646 [binder, in mathcomp.ssreflect.path]
T:65 [binder, in mathcomp.ssreflect.ssrfun]
T:65 [binder, in mathcomp.ssreflect.bigop]
T:651 [binder, in mathcomp.ssreflect.path]
T:654 [binder, in mathcomp.ssreflect.path]
T:658 [binder, in mathcomp.ssreflect.path]
t:66 [binder, in mathcomp.ssreflect.tuple]
T:662 [binder, in mathcomp.ssreflect.path]
T:666 [binder, in mathcomp.ssreflect.path]
t:67 [binder, in mathcomp.ssreflect.ssrAC]
T:674 [binder, in mathcomp.ssreflect.fintype]
T:676 [binder, in mathcomp.ssreflect.path]
t:68 [binder, in mathcomp.ssreflect.tuple]
T:682 [binder, in mathcomp.ssreflect.ssrnat]
T:7 [binder, in mathcomp.solvable.alt]
T:7 [binder, in mathcomp.algebra.interval]
t:7 [binder, in mathcomp.ssreflect.tuple]
T:70 [binder, in mathcomp.ssreflect.ssrAC]
T:71 [binder, in mathcomp.ssreflect.ssrbool]
T:718 [binder, in mathcomp.ssreflect.fintype]
t:72 [binder, in mathcomp.ssreflect.tuple]
T:727 [binder, in mathcomp.ssreflect.fintype]
t:73 [binder, in mathcomp.ssreflect.tuple]
T:73 [binder, in mathcomp.ssreflect.choice]
T:733 [binder, in mathcomp.ssreflect.fintype]
T:738 [binder, in mathcomp.ssreflect.seq]
T:74 [binder, in mathcomp.ssreflect.bigop]
T:740 [binder, in mathcomp.ssreflect.seq]
T:741 [binder, in mathcomp.ssreflect.fintype]
t:75 [binder, in mathcomp.ssreflect.tuple]
t:77 [binder, in mathcomp.ssreflect.tuple]
T:770 [binder, in mathcomp.ssreflect.fintype]
T:778 [binder, in mathcomp.ssreflect.seq]
T:779 [binder, in mathcomp.ssreflect.fintype]
t:78 [binder, in mathcomp.ssreflect.tuple]
T:783 [binder, in mathcomp.ssreflect.seq]
t:786 [binder, in mathcomp.ssreflect.order]
T:788 [binder, in mathcomp.ssreflect.fintype]
T:789 [binder, in mathcomp.ssreflect.path]
T:79 [binder, in mathcomp.ssreflect.ssrAC]
t:790 [binder, in mathcomp.ssreflect.order]
T:8 [binder, in mathcomp.solvable.alt]
T:8 [binder, in mathcomp.fingroup.perm]
T:8 [binder, in mathcomp.ssreflect.generic_quotient]
T:8 [binder, in mathcomp.ssreflect.finset]
T:8 [binder, in mathcomp.ssreflect.fintype]
t:80 [binder, in mathcomp.ssreflect.tuple]
T:80 [binder, in mathcomp.solvable.sylow]
T:80 [binder, in mathcomp.ssreflect.bigop]
T:800 [binder, in mathcomp.ssreflect.fintype]
t:82 [binder, in mathcomp.ssreflect.tuple]
t:83 [binder, in mathcomp.ssreflect.tuple]
t:84 [binder, in mathcomp.ssreflect.tuple]
t:85 [binder, in mathcomp.ssreflect.tuple]
t:857 [binder, in mathcomp.ssreflect.seq]
t:86 [binder, in mathcomp.ssreflect.tuple]
t:86 [binder, in mathcomp.solvable.extremal]
T:863 [binder, in mathcomp.algebra.matrix]
t:87 [binder, in mathcomp.ssreflect.tuple]
T:87 [binder, in mathcomp.ssreflect.finfun]
T:87 [binder, in mathcomp.algebra.ring_quotient]
t:87 [binder, in mathcomp.solvable.extremal]
t:88 [binder, in mathcomp.ssreflect.tuple]
T:88 [binder, in mathcomp.ssreflect.bigop]
T:885 [binder, in mathcomp.algebra.matrix]
t:89 [binder, in mathcomp.ssreflect.tuple]
t:891 [binder, in mathcomp.ssreflect.seq]
T:9 [binder, in mathcomp.ssreflect.eqtype]
t:90 [binder, in mathcomp.ssreflect.tuple]
t:900 [binder, in mathcomp.ssreflect.bigop]
t:91 [binder, in mathcomp.ssreflect.tuple]
t:91 [binder, in mathcomp.ssreflect.finfun]
T:910 [binder, in mathcomp.ssreflect.fintype]
T:913 [binder, in mathcomp.ssreflect.fintype]
t:93 [binder, in mathcomp.ssreflect.tuple]
T:93 [binder, in mathcomp.ssreflect.bigop]
T:942 [binder, in mathcomp.algebra.matrix]
t:943 [binder, in mathcomp.ssreflect.bigop]
T:95 [binder, in mathcomp.ssreflect.generic_quotient]
t:95 [binder, in mathcomp.ssreflect.tuple]
T:953 [binder, in mathcomp.ssreflect.finset]
T:957 [binder, in mathcomp.ssreflect.finset]
T:960 [binder, in mathcomp.ssreflect.finset]
T:965 [binder, in mathcomp.ssreflect.finset]
T:97 [binder, in mathcomp.ssreflect.ssrAC]
T:971 [binder, in mathcomp.algebra.matrix]
t:98 [binder, in mathcomp.ssreflect.tuple]
t:980 [binder, in mathcomp.ssreflect.order]
t:984 [binder, in mathcomp.ssreflect.order]
t:988 [binder, in mathcomp.ssreflect.order]
t:992 [binder, in mathcomp.ssreflect.order]
T:995 [binder, in mathcomp.ssreflect.order]

---

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

(100113 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

(1864 entries)

Binder 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

(49278 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

(1631 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

(6978 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

(94 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

(14781 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

(222 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

(131 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

(2030 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

(2189 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

(1149 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

(19126 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

(565 entries)

---

Index

---

This page has been generated by coqdoc