mathcomp.ssreflect.tuple

Global Index

_

(69505 entries)

Notation Index

H

J

T

W

X

Y

_

(1943 entries)

Binder Index

_

other

(39748 entries)

Module Index

H

J

K

L

T

W

X

Y

Z

_

other

(379 entries)

Variable Index

J

W

X

Y

_

other

(3958 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(13542 entries)

Constructor Index

J

K

W

Y

_

other

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

(134 entries)

Projection Index

H

J

K

L

W

X

Y

_

other

(452 entries)

Section Index

J

W

X

Y

_

other

(1344 entries)

Abbreviation Index

Y

_

other

(1014 entries)

Definition Index

Y

_

other

(6127 entries)

Record Index

B

H

J

K

L

W

X

Y

_

other

(248 entries)

R (binder)

rc:108 [in mathcomp.algebra.ring_quotient]
rc:114 [in mathcomp.algebra.ring_quotient]
rc:145 [in mathcomp.algebra.ring_quotient]
rc:180 [in mathcomp.algebra.ring_quotient]
rc:186 [in mathcomp.algebra.ring_quotient]
rc:77 [in mathcomp.algebra.ring_quotient]
rdivpDl:160 [in mathcomp.algebra.polydiv]
rdivpDr:162 [in mathcomp.algebra.polydiv]
rdivp_addr:161 [in mathcomp.algebra.polydiv]
rdivp_addl:159 [in mathcomp.algebra.polydiv]
real_lteif_normr:461 [in mathcomp.algebra.interval]
real_lersif_normr:460 [in mathcomp.algebra.interval]
real_lteif_norml:458 [in mathcomp.algebra.interval]
real_lersif_norml:457 [in mathcomp.algebra.interval]
real_lteifNE:456 [in mathcomp.algebra.interval]
real_lersifN:455 [in mathcomp.algebra.interval]
real_leif_AGM2:3082 [in mathcomp.algebra.ssrnum]
real_lerif_AGM2:3081 [in mathcomp.algebra.ssrnum]
real_leif_mean_square:3080 [in mathcomp.algebra.ssrnum]
real_lerif_mean_square:3079 [in mathcomp.algebra.ssrnum]
real_leif_AGM2_scaled:3076 [in mathcomp.algebra.ssrnum]
real_lerif_AGM2_scaled:3075 [in mathcomp.algebra.ssrnum]
real_leif_mean_square_scaled:3074 [in mathcomp.algebra.ssrnum]
real_lerif_mean_square_scaled:3073 [in mathcomp.algebra.ssrnum]
real_leif_norm:3066 [in mathcomp.algebra.ssrnum]
real_lerif_norm:3065 [in mathcomp.algebra.ssrnum]
real_ltgt0P:3052 [in mathcomp.algebra.ssrnum]
real_ltrgt0P:3051 [in mathcomp.algebra.ssrnum]
real_ge0P:3050 [in mathcomp.algebra.ssrnum]
real_ger0P:3049 [in mathcomp.algebra.ssrnum]
real_ltgtP:3048 [in mathcomp.algebra.ssrnum]
real_ltrgtP:3047 [in mathcomp.algebra.ssrnum]
real_leNgt:3046 [in mathcomp.algebra.ssrnum]
real_lerNgt:3045 [in mathcomp.algebra.ssrnum]
real_ltNge:3044 [in mathcomp.algebra.ssrnum]
real_ltrNge:3043 [in mathcomp.algebra.ssrnum]
real_ltP:3042 [in mathcomp.algebra.ssrnum]
real_ltrP:3041 [in mathcomp.algebra.ssrnum]
real_leP:3040 [in mathcomp.algebra.ssrnum]
real_lerP:3039 [in mathcomp.algebra.ssrnum]
recf:492 [in mathcomp.algebra.mxpoly]
redg:1786 [in mathcomp.algebra.ssralg]
result:15 [in mathcomp.ssreflect.ssreflect]
result:2 [in mathcomp.ssreflect.ssreflect]
result:7 [in mathcomp.ssreflect.ssreflect]
rfG:570 [in mathcomp.character.character]
rGf:1254 [in mathcomp.character.mxrepresentation]
rG0:150 [in mathcomp.character.mxrepresentation]
rG1:109 [in mathcomp.character.character]
rG1:1117 [in mathcomp.character.mxrepresentation]
rG1:112 [in mathcomp.character.character]
rG1:1250 [in mathcomp.character.mxrepresentation]
rG1:154 [in mathcomp.character.character]
rG1:169 [in mathcomp.character.character]
rG1:171 [in mathcomp.character.character]
rG1:278 [in mathcomp.character.character]
rG1:284 [in mathcomp.character.character]
rG1:319 [in mathcomp.character.character]
rG1:739 [in mathcomp.character.mxrepresentation]
rG1:748 [in mathcomp.character.mxrepresentation]
rG1:754 [in mathcomp.character.mxrepresentation]
rG1:759 [in mathcomp.character.mxrepresentation]
rG1:764 [in mathcomp.character.mxrepresentation]
rG1:778 [in mathcomp.character.mxrepresentation]
rG1:782 [in mathcomp.character.mxrepresentation]
rG1:787 [in mathcomp.character.mxrepresentation]
rG1:791 [in mathcomp.character.mxrepresentation]
rG1:801 [in mathcomp.character.mxrepresentation]
rG1:806 [in mathcomp.character.mxrepresentation]
rG2:110 [in mathcomp.character.character]
rG2:1118 [in mathcomp.character.mxrepresentation]
rG2:113 [in mathcomp.character.character]
rG2:1251 [in mathcomp.character.mxrepresentation]
rG2:155 [in mathcomp.character.character]
rG2:170 [in mathcomp.character.character]
rG2:172 [in mathcomp.character.character]
rG2:279 [in mathcomp.character.character]
rG2:285 [in mathcomp.character.character]
rG2:320 [in mathcomp.character.character]
rG2:741 [in mathcomp.character.mxrepresentation]
rG2:749 [in mathcomp.character.mxrepresentation]
rG2:755 [in mathcomp.character.mxrepresentation]
rG2:760 [in mathcomp.character.mxrepresentation]
rG2:765 [in mathcomp.character.mxrepresentation]
rG2:779 [in mathcomp.character.mxrepresentation]
rG2:783 [in mathcomp.character.mxrepresentation]
rG2:788 [in mathcomp.character.mxrepresentation]
rG2:792 [in mathcomp.character.mxrepresentation]
rG2:802 [in mathcomp.character.mxrepresentation]
rG2:807 [in mathcomp.character.mxrepresentation]
rG3:761 [in mathcomp.character.mxrepresentation]
rG:1253 [in mathcomp.character.mxrepresentation]
rG:1272 [in mathcomp.character.mxrepresentation]
rG:161 [in mathcomp.character.character]
rG:164 [in mathcomp.character.character]
rG:166 [in mathcomp.character.character]
rG:176 [in mathcomp.character.character]
rG:179 [in mathcomp.character.character]
rG:207 [in mathcomp.character.mxabelem]
rG:217 [in mathcomp.character.character]
rG:274 [in mathcomp.character.character]
rG:287 [in mathcomp.character.character]
rG:288 [in mathcomp.character.character]
rG:310 [in mathcomp.character.character]
rG:316 [in mathcomp.character.character]
rG:325 [in mathcomp.character.character]
rG:376 [in mathcomp.character.character]
rG:490 [in mathcomp.character.character]
rG:496 [in mathcomp.character.character]
rG:524 [in mathcomp.character.character]
rG:542 [in mathcomp.character.character]
rG:61 [in mathcomp.character.integral_char]
rG:65 [in mathcomp.character.integral_char]
rG:709 [in mathcomp.character.mxrepresentation]
rG:720 [in mathcomp.character.mxrepresentation]
rG:722 [in mathcomp.character.mxrepresentation]
rG:725 [in mathcomp.character.mxrepresentation]
rG:727 [in mathcomp.character.mxrepresentation]
rG:730 [in mathcomp.character.mxrepresentation]
rG:751 [in mathcomp.character.mxrepresentation]
rG:771 [in mathcomp.character.mxrepresentation]
rG:794 [in mathcomp.character.mxrepresentation]
rG:888 [in mathcomp.character.character]
rG:923 [in mathcomp.character.character]
rho:112 [in mathcomp.solvable.pgroup]
rho:116 [in mathcomp.solvable.pgroup]
rho:120 [in mathcomp.solvable.pgroup]
rho:127 [in mathcomp.solvable.pgroup]
rho:31 [in mathcomp.solvable.pgroup]
rho:34 [in mathcomp.solvable.pgroup]
rho:37 [in mathcomp.solvable.pgroup]
rho:373 [in mathcomp.ssreflect.prime]
rho:376 [in mathcomp.ssreflect.prime]
rho:379 [in mathcomp.ssreflect.prime]
rho:384 [in mathcomp.ssreflect.prime]
rho:429 [in mathcomp.ssreflect.prime]
rho:459 [in mathcomp.ssreflect.prime]
rho:462 [in mathcomp.ssreflect.prime]
rho:543 [in mathcomp.solvable.pgroup]
rho:546 [in mathcomp.solvable.pgroup]
rho:549 [in mathcomp.solvable.pgroup]
rho:552 [in mathcomp.solvable.pgroup]
rho:557 [in mathcomp.solvable.pgroup]
rho:566 [in mathcomp.solvable.pgroup]
rhs:117 [in mathcomp.ssreflect.choice]
rhs:124 [in mathcomp.ssreflect.choice]
rid:99 [in mathcomp.ssreflect.ssrAC]
ringS:1378 [in mathcomp.algebra.ssralg]
ringS:1384 [in mathcomp.algebra.ssralg]
ringS:1387 [in mathcomp.algebra.ssralg]
ringS:1397 [in mathcomp.algebra.ssralg]
ringS:160 [in mathcomp.field.algC]
ringS:170 [in mathcomp.algebra.rat]
ringS:186 [in mathcomp.field.algC]
ringS:2331 [in mathcomp.algebra.matrix]
ringS:325 [in mathcomp.field.algC]
ringS:513 [in mathcomp.algebra.poly]
ringS:553 [in mathcomp.algebra.poly]
ringS:599 [in mathcomp.algebra.poly]
ringS:738 [in mathcomp.algebra.poly]
ringS:827 [in mathcomp.algebra.ssrint]
rI:1042 [in mathcomp.ssreflect.bigop]
rI:1057 [in mathcomp.ssreflect.bigop]
rI:1113 [in mathcomp.ssreflect.bigop]
rI:292 [in mathcomp.algebra.poly]
rI:299 [in mathcomp.algebra.poly]
rI:304 [in mathcomp.algebra.poly]
rJ:1043 [in mathcomp.ssreflect.bigop]
rJ:1058 [in mathcomp.ssreflect.bigop]
rJ:1114 [in mathcomp.ssreflect.bigop]
rk:135 [in mathcomp.algebra.vector]
rmodpD:164 [in mathcomp.algebra.polydiv]
rmodp_add:163 [in mathcomp.algebra.polydiv]
rngS:1605 [in mathcomp.algebra.ssralg]
Rorder:14 [in mathcomp.algebra.ssrnum]
Rorder:3 [in mathcomp.algebra.ssrnum]
rotD:2087 [in mathcomp.ssreflect.seq]
rot_addn:2086 [in mathcomp.ssreflect.seq]
RoverFp:157 [in mathcomp.field.finfield]
row1:711 [in mathcomp.algebra.matrix]
row3:713 [in mathcomp.algebra.matrix]
rqc:162 [in mathcomp.algebra.ring_quotient]
rqc:164 [in mathcomp.algebra.ring_quotient]
rqc:166 [in mathcomp.algebra.ring_quotient]
rqc:94 [in mathcomp.algebra.ring_quotient]
rqc:96 [in mathcomp.algebra.ring_quotient]
rqT:100 [in mathcomp.algebra.ring_quotient]
rqT:101 [in mathcomp.algebra.ring_quotient]
rqT:102 [in mathcomp.algebra.ring_quotient]
rqT:103 [in mathcomp.algebra.ring_quotient]
rqT:121 [in mathcomp.algebra.ring_quotient]
rqT:122 [in mathcomp.algebra.ring_quotient]
rqT:123 [in mathcomp.algebra.ring_quotient]
rqT:128 [in mathcomp.algebra.ring_quotient]
rqT:129 [in mathcomp.algebra.ring_quotient]
rqT:159 [in mathcomp.algebra.ring_quotient]
rqT:161 [in mathcomp.algebra.ring_quotient]
rqT:163 [in mathcomp.algebra.ring_quotient]
rqT:165 [in mathcomp.algebra.ring_quotient]
rqT:167 [in mathcomp.algebra.ring_quotient]
rqT:168 [in mathcomp.algebra.ring_quotient]
rqT:169 [in mathcomp.algebra.ring_quotient]
rqT:170 [in mathcomp.algebra.ring_quotient]
rqT:171 [in mathcomp.algebra.ring_quotient]
rqT:172 [in mathcomp.algebra.ring_quotient]
rqT:173 [in mathcomp.algebra.ring_quotient]
rqT:174 [in mathcomp.algebra.ring_quotient]
rqT:175 [in mathcomp.algebra.ring_quotient]
rqT:193 [in mathcomp.algebra.ring_quotient]
rqT:194 [in mathcomp.algebra.ring_quotient]
rqT:197 [in mathcomp.algebra.ring_quotient]
rqT:200 [in mathcomp.algebra.ring_quotient]
rqT:201 [in mathcomp.algebra.ring_quotient]
rqT:91 [in mathcomp.algebra.ring_quotient]
rqT:93 [in mathcomp.algebra.ring_quotient]
rqT:95 [in mathcomp.algebra.ring_quotient]
rqT:97 [in mathcomp.algebra.ring_quotient]
rqT:98 [in mathcomp.algebra.ring_quotient]
rqT:99 [in mathcomp.algebra.ring_quotient]
rQ:2199 [in mathcomp.algebra.ssralg]
rR:174 [in mathcomp.algebra.rat]
rR:177 [in mathcomp.algebra.rat]
rr:206 [in mathcomp.field.closed_field]
rR:207 [in mathcomp.algebra.mxpoly]
rr:212 [in mathcomp.field.closed_field]
rr:470 [in mathcomp.algebra.polydiv]
rr:479 [in mathcomp.algebra.polydiv]
rR:62 [in mathcomp.field.algnum]
rr:69 [in mathcomp.algebra.polydiv]
rR:770 [in mathcomp.algebra.poly]
rr:78 [in mathcomp.algebra.polydiv]
rr:789 [in mathcomp.ssreflect.bigop]
rs1:293 [in mathcomp.field.falgebra]
rs2:294 [in mathcomp.field.falgebra]
rs:194 [in mathcomp.algebra.polydiv]
rs:205 [in mathcomp.solvable.cyclic]
rs:254 [in mathcomp.field.separable]
rs:277 [in mathcomp.field.falgebra]
rs:279 [in mathcomp.field.falgebra]
rs:291 [in mathcomp.field.falgebra]
rs:392 [in mathcomp.algebra.polydiv]
rs:57 [in mathcomp.field.fieldext]
rs:6 [in mathcomp.field.galois]
rs:8 [in mathcomp.field.galois]
rs:884 [in mathcomp.algebra.poly]
rs:903 [in mathcomp.algebra.poly]
rs:905 [in mathcomp.algebra.poly]
rs:930 [in mathcomp.algebra.poly]
rs:934 [in mathcomp.algebra.poly]
rs:938 [in mathcomp.algebra.poly]
rs:940 [in mathcomp.algebra.poly]
rs:945 [in mathcomp.algebra.poly]
rs:947 [in mathcomp.algebra.poly]
rs:948 [in mathcomp.algebra.poly]
RtoK:324 [in mathcomp.algebra.mxpoly]
RtoK:330 [in mathcomp.algebra.mxpoly]
rT':29 [in mathcomp.fingroup.action]
rT:102 [in mathcomp.solvable.gfunctor]
rT:107 [in mathcomp.solvable.gfunctor]
rt:109 [in mathcomp.field.closed_field]
rT:11 [in mathcomp.ssreflect.ssrfun]
rT:112 [in mathcomp.solvable.gfunctor]
rT:113 [in mathcomp.algebra.ring_quotient]
rT:115 [in mathcomp.solvable.maximal]
rT:117 [in mathcomp.solvable.cyclic]
rT:118 [in mathcomp.solvable.gfunctor]
rT:1181 [in mathcomp.ssreflect.finset]
rT:1190 [in mathcomp.ssreflect.finset]
rT:120 [in mathcomp.solvable.maximal]
rT:123 [in mathcomp.solvable.gfunctor]
rT:136 [in mathcomp.solvable.center]
rT:151 [in mathcomp.solvable.commutator]
rT:152 [in mathcomp.solvable.gseries]
rT:17 [in mathcomp.fingroup.action]
rT:171 [in mathcomp.solvable.commutator]
rT:178 [in mathcomp.algebra.ring_quotient]
rT:185 [in mathcomp.algebra.ring_quotient]
rT:213 [in mathcomp.ssreflect.eqtype]
rT:221 [in mathcomp.solvable.nilpotent]
rT:224 [in mathcomp.solvable.nilpotent]
rT:258 [in mathcomp.fingroup.quotient]
rT:28 [in mathcomp.fingroup.action]
rT:28 [in mathcomp.ssreflect.ssrbool]
rT:31 [in mathcomp.ssreflect.finfun]
rT:33 [in mathcomp.solvable.maximal]
rT:34 [in mathcomp.ssreflect.finfun]
rT:39 [in mathcomp.solvable.maximal]
rT:40 [in mathcomp.field.fieldext]
rT:401 [in mathcomp.solvable.abelian]
rT:402 [in mathcomp.fingroup.morphism]
rT:407 [in mathcomp.fingroup.morphism]
rT:413 [in mathcomp.fingroup.morphism]
rT:416 [in mathcomp.solvable.abelian]
rT:417 [in mathcomp.fingroup.morphism]
rT:420 [in mathcomp.solvable.abelian]
rT:425 [in mathcomp.fingroup.morphism]
rT:429 [in mathcomp.fingroup.morphism]
rT:43 [in mathcomp.field.fieldext]
rT:43 [in mathcomp.solvable.maximal]
rT:433 [in mathcomp.fingroup.morphism]
rT:437 [in mathcomp.fingroup.morphism]
rT:440 [in mathcomp.solvable.pgroup]
rT:443 [in mathcomp.fingroup.morphism]
rT:447 [in mathcomp.solvable.pgroup]
rT:448 [in mathcomp.fingroup.morphism]
rT:46 [in mathcomp.field.fieldext]
rT:471 [in mathcomp.algebra.vector]
rT:498 [in mathcomp.ssreflect.fintype]
rT:507 [in mathcomp.ssreflect.finset]
rT:513 [in mathcomp.ssreflect.finset]
rT:520 [in mathcomp.ssreflect.finset]
rT:524 [in mathcomp.ssreflect.finset]
rT:529 [in mathcomp.ssreflect.finset]
rT:529 [in mathcomp.algebra.vector]
rT:532 [in mathcomp.algebra.vector]
rT:537 [in mathcomp.algebra.vector]
rT:542 [in mathcomp.algebra.vector]
rT:545 [in mathcomp.algebra.vector]
rT:548 [in mathcomp.algebra.vector]
rT:55 [in mathcomp.solvable.center]
rT:55 [in mathcomp.fingroup.presentation]
rT:552 [in mathcomp.algebra.vector]
rT:571 [in mathcomp.solvable.pgroup]
rT:61 [in mathcomp.solvable.maximal]
rT:67 [in mathcomp.fingroup.presentation]
rT:69 [in mathcomp.fingroup.presentation]
rT:70 [in mathcomp.solvable.gseries]
rT:730 [in mathcomp.algebra.vector]
rT:732 [in mathcomp.algebra.vector]
rT:750 [in mathcomp.character.classfun]
rT:754 [in mathcomp.character.classfun]
rT:763 [in mathcomp.ssreflect.finset]
rT:78 [in mathcomp.ssreflect.finfun]
rT:79 [in mathcomp.ssreflect.finfun]
rT:80 [in mathcomp.ssreflect.finfun]
rT:81 [in mathcomp.ssreflect.finfun]
rT:82 [in mathcomp.ssreflect.finfun]
rT:83 [in mathcomp.ssreflect.finfun]
rT:84 [in mathcomp.ssreflect.finfun]
rT:85 [in mathcomp.ssreflect.finfun]
rT:85 [in mathcomp.fingroup.presentation]
rT:86 [in mathcomp.ssreflect.finfun]
rT:87 [in mathcomp.ssreflect.finfun]
rT:88 [in mathcomp.ssreflect.finfun]
rT:89 [in mathcomp.ssreflect.finfun]
rT:90 [in mathcomp.fingroup.presentation]
rT:900 [in mathcomp.character.character]
rT:906 [in mathcomp.character.character]
rT:97 [in mathcomp.fingroup.presentation]
rU:119 [in mathcomp.character.character]
rU:127 [in mathcomp.character.character]
rV:120 [in mathcomp.character.character]
rv:122 [in mathcomp.algebra.vector]
rv:17 [in mathcomp.field.finfield]
rV:269 [in mathcomp.algebra.ssrint]
rW:139 [in mathcomp.character.character]
rW:144 [in mathcomp.character.character]
rw:871 [in mathcomp.algebra.vector]
rw:873 [in mathcomp.algebra.vector]
rxx:227 [in mathcomp.ssreflect.generic_quotient]
Rx:145 [in mathcomp.field.algebraics_fundamentals]
rX:155 [in mathcomp.solvable.finmodule]
rX:164 [in mathcomp.solvable.finmodule]
rz:198 [in mathcomp.field.galois]
r_a:463 [in mathcomp.field.galois]
r_:537 [in mathcomp.ssreflect.bigop]
r_:530 [in mathcomp.ssreflect.bigop]
R_:1583 [in mathcomp.algebra.mxalgebra]
R_:1400 [in mathcomp.algebra.mxalgebra]
R':1694 [in mathcomp.ssreflect.seq]
r':1922 [in mathcomp.ssreflect.seq]
r':1928 [in mathcomp.ssreflect.seq]
R':530 [in mathcomp.algebra.ssrint]
R':732 [in mathcomp.algebra.ssrint]
r1:1157 [in mathcomp.algebra.mxalgebra]
r1:12 [in mathcomp.algebra.polydiv]
r1:131 [in mathcomp.field.closed_field]
R1:1380 [in mathcomp.algebra.mxalgebra]
R1:1386 [in mathcomp.algebra.mxalgebra]
R1:1393 [in mathcomp.algebra.mxalgebra]
R1:1418 [in mathcomp.algebra.mxalgebra]
R1:1424 [in mathcomp.algebra.mxalgebra]
R1:1429 [in mathcomp.algebra.mxalgebra]
r1:143 [in mathcomp.field.closed_field]
R1:1437 [in mathcomp.algebra.mxalgebra]
R1:1447 [in mathcomp.algebra.mxalgebra]
R1:1456 [in mathcomp.algebra.mxalgebra]
R1:1464 [in mathcomp.algebra.mxalgebra]
R1:1479 [in mathcomp.algebra.mxalgebra]
R1:1486 [in mathcomp.algebra.mxalgebra]
R1:1493 [in mathcomp.algebra.mxalgebra]
R1:1499 [in mathcomp.algebra.mxalgebra]
R1:1507 [in mathcomp.algebra.mxalgebra]
R1:1512 [in mathcomp.algebra.mxalgebra]
R1:1517 [in mathcomp.algebra.mxalgebra]
r1:1546 [in mathcomp.ssreflect.seq]
R1:1577 [in mathcomp.algebra.mxalgebra]
r1:178 [in mathcomp.field.separable]
R1:2369 [in mathcomp.algebra.ssralg]
r1:270 [in mathcomp.fingroup.gproduct]
r1:293 [in mathcomp.algebra.interval]
r1:332 [in mathcomp.ssreflect.bigop]
r1:352 [in mathcomp.algebra.intdiv]
r1:354 [in mathcomp.algebra.intdiv]
r1:356 [in mathcomp.algebra.intdiv]
r1:375 [in mathcomp.ssreflect.bigop]
r1:383 [in mathcomp.ssreflect.bigop]
r1:389 [in mathcomp.ssreflect.bigop]
R1:40 [in mathcomp.field.cyclotomic]
R1:400 [in mathcomp.character.classfun]
R1:404 [in mathcomp.character.classfun]
r1:513 [in mathcomp.ssreflect.div]
r1:515 [in mathcomp.ssreflect.div]
r1:517 [in mathcomp.ssreflect.div]
r1:712 [in mathcomp.ssreflect.bigop]
r1:724 [in mathcomp.ssreflect.bigop]
r1:735 [in mathcomp.ssreflect.bigop]
r1:797 [in mathcomp.ssreflect.bigop]
r1:833 [in mathcomp.ssreflect.bigop]
r2v:41 [in mathcomp.algebra.vector]
r2:1158 [in mathcomp.algebra.mxalgebra]
R2:1381 [in mathcomp.algebra.mxalgebra]
R2:1387 [in mathcomp.algebra.mxalgebra]
R2:1394 [in mathcomp.algebra.mxalgebra]
R2:1419 [in mathcomp.algebra.mxalgebra]
R2:1425 [in mathcomp.algebra.mxalgebra]
R2:1430 [in mathcomp.algebra.mxalgebra]
R2:1438 [in mathcomp.algebra.mxalgebra]
R2:1448 [in mathcomp.algebra.mxalgebra]
R2:1457 [in mathcomp.algebra.mxalgebra]
R2:1465 [in mathcomp.algebra.mxalgebra]
R2:1480 [in mathcomp.algebra.mxalgebra]
R2:1487 [in mathcomp.algebra.mxalgebra]
R2:1494 [in mathcomp.algebra.mxalgebra]
R2:1503 [in mathcomp.algebra.mxalgebra]
R2:1508 [in mathcomp.algebra.mxalgebra]
R2:1513 [in mathcomp.algebra.mxalgebra]
R2:1518 [in mathcomp.algebra.mxalgebra]
r2:1548 [in mathcomp.ssreflect.seq]
R2:1578 [in mathcomp.algebra.mxalgebra]
R2:2370 [in mathcomp.algebra.ssralg]
r2:271 [in mathcomp.fingroup.gproduct]
r2:294 [in mathcomp.algebra.interval]
r2:333 [in mathcomp.ssreflect.bigop]
r2:353 [in mathcomp.algebra.intdiv]
r2:355 [in mathcomp.algebra.intdiv]
r2:357 [in mathcomp.algebra.intdiv]
r2:376 [in mathcomp.ssreflect.bigop]
r2:384 [in mathcomp.ssreflect.bigop]
r2:390 [in mathcomp.ssreflect.bigop]
R2:401 [in mathcomp.character.classfun]
R2:405 [in mathcomp.character.classfun]
R2:41 [in mathcomp.field.cyclotomic]
r2:514 [in mathcomp.ssreflect.div]
r2:516 [in mathcomp.ssreflect.div]
r2:518 [in mathcomp.ssreflect.div]
r2:713 [in mathcomp.ssreflect.bigop]
r2:726 [in mathcomp.ssreflect.bigop]
r2:736 [in mathcomp.ssreflect.bigop]
r2:798 [in mathcomp.ssreflect.bigop]
r2:834 [in mathcomp.ssreflect.bigop]
R3:1449 [in mathcomp.algebra.mxalgebra]
R3:1458 [in mathcomp.algebra.mxalgebra]
R3:1481 [in mathcomp.algebra.mxalgebra]
R3:1488 [in mathcomp.algebra.mxalgebra]
R3:1495 [in mathcomp.algebra.mxalgebra]
R4:1450 [in mathcomp.algebra.mxalgebra]
R4:1459 [in mathcomp.algebra.mxalgebra]
R:1 [in mathcomp.algebra.ssrnum]
r:10 [in mathcomp.field.algnum]
r:1002 [in mathcomp.algebra.ssralg]
r:1002 [in mathcomp.algebra.poly]
r:1008 [in mathcomp.algebra.polydiv]
r:1008 [in mathcomp.algebra.ssralg]
R:101 [in mathcomp.algebra.mxpoly]
r:101 [in mathcomp.character.inertia]
R:102 [in mathcomp.algebra.countalg]
r:102 [in mathcomp.algebra.polyXY]
r:1027 [in mathcomp.fingroup.fingroup]
r:103 [in mathcomp.algebra.polyXY]
R:103 [in mathcomp.fingroup.morphism]
r:1030 [in mathcomp.algebra.polydiv]
r:1034 [in mathcomp.fingroup.fingroup]
r:1035 [in mathcomp.algebra.polydiv]
r:104 [in mathcomp.algebra.poly]
R:105 [in mathcomp.fingroup.morphism]
r:1050 [in mathcomp.algebra.polydiv]
R:106 [in mathcomp.solvable.pgroup]
R:106 [in mathcomp.algebra.finalg]
R:107 [in mathcomp.fingroup.morphism]
R:1074 [in mathcomp.algebra.ssralg]
R:108 [in mathcomp.solvable.sylow]
R:108 [in mathcomp.algebra.ssrnum]
r:108 [in mathcomp.algebra.ssralg]
r:109 [in mathcomp.algebra.polydiv]
R:109 [in mathcomp.ssreflect.eqtype]
r:1098 [in mathcomp.ssreflect.bigop]
R:110 [in mathcomp.ssreflect.finfun]
R:110 [in mathcomp.solvable.pgroup]
R:110 [in mathcomp.algebra.finalg]
r:1103 [in mathcomp.algebra.ssralg]
r:1105 [in mathcomp.ssreflect.bigop]
r:112 [in mathcomp.field.finfield]
R:112 [in mathcomp.algebra.finalg]
R:1125 [in mathcomp.algebra.ssralg]
r:113 [in mathcomp.field.finfield]
R:113 [in mathcomp.algebra.ssrnum]
R:1131 [in mathcomp.algebra.ssralg]
R:1138 [in mathcomp.algebra.ssralg]
R:114 [in mathcomp.algebra.finalg]
r:114 [in mathcomp.algebra.ssralg]
R:114 [in mathcomp.ssreflect.eqtype]
r:115 [in mathcomp.field.finfield]
R:115 [in mathcomp.solvable.gfunctor]
R:1153 [in mathcomp.algebra.ssralg]
R:1155 [in mathcomp.algebra.ssralg]
R:1156 [in mathcomp.algebra.ssralg]
R:1157 [in mathcomp.algebra.ssralg]
r:1182 [in mathcomp.algebra.mxalgebra]
R:119 [in mathcomp.algebra.ssrnum]
r:1191 [in mathcomp.algebra.ssrnum]
r:1199 [in mathcomp.ssreflect.bigop]
r:12 [in mathcomp.ssreflect.div]
r:12 [in mathcomp.solvable.burnside_app]
R:120 [in mathcomp.algebra.finalg]
R:120 [in mathcomp.solvable.gseries]
R:120 [in mathcomp.solvable.gfunctor]
r:1203 [in mathcomp.ssreflect.bigop]
r:121 [in mathcomp.ssreflect.binomial]
r:1215 [in mathcomp.ssreflect.bigop]
R:122 [in mathcomp.solvable.gseries]
r:122 [in mathcomp.algebra.ssralg]
R:1223 [in mathcomp.algebra.ssralg]
R:1227 [in mathcomp.algebra.ssralg]
r:1227 [in mathcomp.ssreflect.bigop]
r:123 [in mathcomp.solvable.nilpotent]
r:124 [in mathcomp.field.closed_field]
R:124 [in mathcomp.algebra.finalg]
r:1240 [in mathcomp.ssreflect.bigop]
R:1243 [in mathcomp.algebra.ssralg]
r:1246 [in mathcomp.ssreflect.bigop]
r:1248 [in mathcomp.ssreflect.seq]
r:125 [in mathcomp.solvable.burnside_app]
R:126 [in mathcomp.algebra.finalg]
R:1261 [in mathcomp.algebra.ssralg]
R:1263 [in mathcomp.algebra.ssralg]
r:127 [in mathcomp.algebra.mxalgebra]
r:129 [in mathcomp.ssreflect.prime]
r:1295 [in mathcomp.ssreflect.bigop]
R:13 [in mathcomp.algebra.ssrnum]
r:13 [in mathcomp.solvable.burnside_app]
r:130 [in mathcomp.algebra.ssralg]
r:130 [in mathcomp.algebra.poly]
R:1305 [in mathcomp.algebra.ssralg]
r:131 [in mathcomp.algebra.polydiv]
r:131 [in mathcomp.solvable.burnside_app]
R:1313 [in mathcomp.algebra.ssralg]
R:1317 [in mathcomp.algebra.ssralg]
R:132 [in mathcomp.algebra.finalg]
R:1321 [in mathcomp.algebra.ssralg]
R:1325 [in mathcomp.algebra.ssralg]
R:133 [in mathcomp.algebra.ssrnum]
r:133 [in mathcomp.algebra.mxalgebra]
R:1330 [in mathcomp.algebra.ssralg]
R:1334 [in mathcomp.algebra.ssralg]
R:1338 [in mathcomp.algebra.ssralg]
R:1343 [in mathcomp.algebra.ssralg]
R:1347 [in mathcomp.algebra.ssralg]
r:135 [in mathcomp.algebra.polydiv]
R:135 [in mathcomp.algebra.ssrint]
R:1352 [in mathcomp.algebra.ssralg]
R:1354 [in mathcomp.algebra.ssralg]
R:1356 [in mathcomp.algebra.ssralg]
R:1358 [in mathcomp.algebra.ssralg]
R:136 [in mathcomp.algebra.mxpoly]
R:136 [in mathcomp.algebra.finalg]
R:1361 [in mathcomp.algebra.ssralg]
R:1363 [in mathcomp.algebra.ssralg]
R:1365 [in mathcomp.algebra.ssralg]
R:1368 [in mathcomp.algebra.ssralg]
r:137 [in mathcomp.algebra.polydiv]
R:137 [in mathcomp.fingroup.morphism]
R:1370 [in mathcomp.algebra.ssralg]
R:1372 [in mathcomp.algebra.mxalgebra]
R:1373 [in mathcomp.algebra.ssralg]
R:1376 [in mathcomp.algebra.ssralg]
R:1379 [in mathcomp.algebra.ssralg]
r:138 [in mathcomp.field.closed_field]
R:138 [in mathcomp.algebra.finalg]
r:1381 [in mathcomp.algebra.matrix]
R:1382 [in mathcomp.algebra.ssralg]
R:1385 [in mathcomp.algebra.ssralg]
r:1388 [in mathcomp.algebra.matrix]
R:1388 [in mathcomp.algebra.ssralg]
R:139 [in mathcomp.algebra.ssrint]
R:139 [in mathcomp.ssreflect.bigop]
r:1390 [in mathcomp.algebra.matrix]
R:1391 [in mathcomp.algebra.ssralg]
R:1395 [in mathcomp.algebra.ssralg]
R:1398 [in mathcomp.algebra.ssralg]
r:14 [in mathcomp.solvable.burnside_app]
r:140 [in mathcomp.algebra.polydiv]
R:140 [in mathcomp.field.algebraics_fundamentals]
R:141 [in mathcomp.ssreflect.binomial]
R:1410 [in mathcomp.algebra.ssralg]
R:1412 [in mathcomp.algebra.mxalgebra]
R:1414 [in mathcomp.algebra.ssralg]
R:1419 [in mathcomp.algebra.ssralg]
R:142 [in mathcomp.algebra.ssrint]
R:142 [in mathcomp.fingroup.morphism]
r:1428 [in mathcomp.ssreflect.order]
R:1429 [in mathcomp.algebra.ssralg]
r:1434 [in mathcomp.ssreflect.order]
R:1436 [in mathcomp.algebra.ssralg]
R:1439 [in mathcomp.algebra.mxalgebra]
r:144 [in mathcomp.algebra.polydiv]
R:1440 [in mathcomp.algebra.ssralg]
r:1441 [in mathcomp.ssreflect.order]
R:1444 [in mathcomp.algebra.ssralg]
R:1448 [in mathcomp.algebra.ssralg]
R:145 [in mathcomp.fingroup.morphism]
r:145 [in mathcomp.ssreflect.bigop]
R:1454 [in mathcomp.algebra.ssralg]
R:1459 [in mathcomp.algebra.ssralg]
r:146 [in mathcomp.fingroup.fingroup]
r:1462 [in mathcomp.ssreflect.order]
R:1464 [in mathcomp.algebra.ssralg]
R:147 [in mathcomp.ssreflect.finfun]
R:1471 [in mathcomp.algebra.ssralg]
R:1477 [in mathcomp.algebra.ssralg]
r:1478 [in mathcomp.algebra.matrix]
r:148 [in mathcomp.algebra.polydiv]
R:148 [in mathcomp.fingroup.morphism]
r:1482 [in mathcomp.ssreflect.seq]
r:1488 [in mathcomp.algebra.matrix]
R:149 [in mathcomp.algebra.mxpoly]
R:149 [in mathcomp.fingroup.morphism]
R:1495 [in mathcomp.algebra.ssralg]
r:1497 [in mathcomp.ssreflect.order]
r:1503 [in mathcomp.ssreflect.order]
R:1505 [in mathcomp.algebra.ssralg]
r:151 [in mathcomp.field.closed_field]
r:151 [in mathcomp.solvable.sylow]
R:151 [in mathcomp.fingroup.morphism]
r:1510 [in mathcomp.ssreflect.order]
R:1510 [in mathcomp.algebra.ssralg]
R:1515 [in mathcomp.algebra.ssralg]
R:152 [in mathcomp.algebra.ssrnum]
R:1520 [in mathcomp.algebra.ssralg]
R:1521 [in mathcomp.algebra.mxalgebra]
r:1524 [in mathcomp.ssreflect.seq]
R:1526 [in mathcomp.algebra.ssralg]
R:1527 [in mathcomp.algebra.mxalgebra]
R:153 [in mathcomp.algebra.mxpoly]
R:153 [in mathcomp.algebra.ssralg]
r:1530 [in mathcomp.ssreflect.order]
R:1530 [in mathcomp.algebra.mxalgebra]
R:1531 [in mathcomp.algebra.ssralg]
R:1533 [in mathcomp.algebra.mxalgebra]
r:1534 [in mathcomp.ssreflect.seq]
R:1536 [in mathcomp.algebra.ssralg]
r:1537 [in mathcomp.ssreflect.seq]
r:1542 [in mathcomp.ssreflect.seq]
R:1542 [in mathcomp.algebra.ssralg]
R:1543 [in mathcomp.algebra.mxalgebra]
R:1547 [in mathcomp.algebra.ssralg]
R:1549 [in mathcomp.algebra.mxalgebra]
R:1554 [in mathcomp.algebra.mxalgebra]
R:1557 [in mathcomp.algebra.mxalgebra]
r:1560 [in mathcomp.algebra.ssralg]
R:1561 [in mathcomp.algebra.mxalgebra]
R:1565 [in mathcomp.algebra.mxalgebra]
r:157 [in mathcomp.field.closed_field]
R:157 [in mathcomp.algebra.finalg]
R:157 [in mathcomp.algebra.ssralg]
R:1570 [in mathcomp.algebra.mxalgebra]
R:1573 [in mathcomp.algebra.mxalgebra]
R:158 [in mathcomp.algebra.mxpoly]
R:158 [in mathcomp.character.inertia]
R:158 [in mathcomp.algebra.ssrnum]
R:1582 [in mathcomp.algebra.mxalgebra]
R:159 [in mathcomp.fingroup.morphism]
r:1598 [in mathcomp.algebra.ssralg]
r:16 [in mathcomp.solvable.burnside_app]
R:160 [in mathcomp.fingroup.morphism]
r:163 [in mathcomp.ssreflect.bigop]
r:164 [in mathcomp.field.closed_field]
R:166 [in mathcomp.algebra.ssralg]
r:1670 [in mathcomp.algebra.matrix]
r:1675 [in mathcomp.algebra.matrix]
r:1677 [in mathcomp.algebra.matrix]
r:1679 [in mathcomp.algebra.matrix]
R:168 [in mathcomp.algebra.mxpoly]
r:1682 [in mathcomp.algebra.matrix]
r:1685 [in mathcomp.algebra.matrix]
r:1688 [in mathcomp.algebra.matrix]
R:169 [in mathcomp.fingroup.morphism]
r:169 [in mathcomp.algebra.vector]
r:1691 [in mathcomp.algebra.matrix]
R:1693 [in mathcomp.ssreflect.seq]
r:1696 [in mathcomp.algebra.matrix]
r:17 [in mathcomp.solvable.burnside_app]
r:17 [in mathcomp.fingroup.presentation]
r:170 [in mathcomp.field.galois]
r:1700 [in mathcomp.algebra.matrix]
r:1702 [in mathcomp.algebra.matrix]
r:1705 [in mathcomp.algebra.matrix]
r:1708 [in mathcomp.algebra.matrix]
r:1708 [in mathcomp.algebra.ssralg]
R:171 [in mathcomp.algebra.ssrnum]
r:1710 [in mathcomp.algebra.matrix]
r:1713 [in mathcomp.algebra.ssralg]
r:1717 [in mathcomp.algebra.ssralg]
R:1718 [in mathcomp.ssreflect.seq]
r:1719 [in mathcomp.ssreflect.order]
r:172 [in mathcomp.character.classfun]
r:1725 [in mathcomp.ssreflect.order]
r:1737 [in mathcomp.algebra.ssralg]
R:174 [in mathcomp.ssreflect.finfun]
r:174 [in mathcomp.character.character]
r:1741 [in mathcomp.algebra.ssralg]
r:175 [in mathcomp.ssreflect.generic_quotient]
R:175 [in mathcomp.ssreflect.finfun]
r:176 [in mathcomp.field.closed_field]
r:178 [in mathcomp.solvable.nilpotent]
r:18 [in mathcomp.ssreflect.div]
r:18 [in mathcomp.algebra.mxpoly]
R:181 [in mathcomp.algebra.ssralg]
R:182 [in mathcomp.solvable.cyclic]
R:182 [in mathcomp.algebra.ssralg]
R:1829 [in mathcomp.algebra.ssralg]
r:183 [in mathcomp.algebra.polydiv]
R:183 [in mathcomp.algebra.ssralg]
R:1832 [in mathcomp.ssreflect.seq]
R:1832 [in mathcomp.algebra.ssralg]
r:184 [in mathcomp.ssreflect.generic_quotient]
r:184 [in mathcomp.ssreflect.prime]
r:184 [in mathcomp.ssreflect.bigop]
r:185 [in mathcomp.field.closed_field]
R:1856 [in mathcomp.algebra.matrix]
r:1857 [in mathcomp.algebra.ssralg]
R:186 [in mathcomp.algebra.ssrnum]
R:186 [in mathcomp.algebra.ssralg]
r:186 [in mathcomp.solvable.nilpotent]
R:1865 [in mathcomp.algebra.matrix]
R:1867 [in mathcomp.algebra.matrix]
R:187 [in mathcomp.solvable.maximal]
R:1870 [in mathcomp.algebra.matrix]
r:1870 [in mathcomp.algebra.ssralg]
R:1872 [in mathcomp.algebra.matrix]
R:189 [in mathcomp.algebra.ssralg]
R:189 [in mathcomp.solvable.maximal]
r:1891 [in mathcomp.algebra.matrix]
R:1899 [in mathcomp.algebra.ssralg]
R:190 [in mathcomp.fingroup.morphism]
r:1900 [in mathcomp.algebra.matrix]
R:1901 [in mathcomp.algebra.ssralg]
R:1902 [in mathcomp.algebra.ssralg]
r:191 [in mathcomp.algebra.ssrint]
R:191 [in mathcomp.fingroup.morphism]
R:191 [in mathcomp.algebra.ssralg]
R:1916 [in mathcomp.algebra.matrix]
r:1921 [in mathcomp.ssreflect.seq]
r:1927 [in mathcomp.ssreflect.seq]
R:193 [in mathcomp.fingroup.morphism]
r:1931 [in mathcomp.ssreflect.seq]
r:1939 [in mathcomp.ssreflect.seq]
r:194 [in mathcomp.field.separable]
r:194 [in mathcomp.algebra.mxpoly]
R:194 [in mathcomp.character.classfun]
r:1947 [in mathcomp.ssreflect.seq]
r:1949 [in mathcomp.algebra.ssralg]
R:195 [in mathcomp.fingroup.morphism]
r:1954 [in mathcomp.ssreflect.seq]
r:1955 [in mathcomp.algebra.ssralg]
R:1958 [in mathcomp.algebra.matrix]
R:197 [in mathcomp.algebra.ssralg]
r:198 [in mathcomp.algebra.ssrint]
R:199 [in mathcomp.algebra.ssralg]
r:2 [in mathcomp.ssreflect.prime]
R:20 [in mathcomp.field.finfield]
R:201 [in mathcomp.fingroup.morphism]
R:2013 [in mathcomp.algebra.ssralg]
R:2017 [in mathcomp.algebra.ssralg]
R:202 [in mathcomp.algebra.ring_quotient]
R:203 [in mathcomp.fingroup.morphism]
r:204 [in mathcomp.field.separable]
r:204 [in mathcomp.ssreflect.bigop]
R:206 [in mathcomp.algebra.ring_quotient]
R:207 [in mathcomp.fingroup.morphism]
r:208 [in mathcomp.character.mxrepresentation]
R:208 [in mathcomp.fingroup.morphism]
R:208 [in mathcomp.solvable.maximal]
R:2090 [in mathcomp.algebra.ssralg]
R:21 [in mathcomp.algebra.mxpoly]
r:210 [in mathcomp.field.fieldext]
R:210 [in mathcomp.algebra.ring_quotient]
r:210 [in mathcomp.algebra.ssralg]
r:211 [in mathcomp.field.galois]
r:212 [in mathcomp.field.fieldext]
R:212 [in mathcomp.solvable.maximal]
R:2141 [in mathcomp.algebra.matrix]
R:215 [in mathcomp.algebra.ring_quotient]
R:217 [in mathcomp.algebra.ring_quotient]
r:217 [in mathcomp.algebra.ssralg]
R:2172 [in mathcomp.algebra.ssralg]
R:2176 [in mathcomp.algebra.matrix]
r:218 [in mathcomp.character.mxrepresentation]
R:2181 [in mathcomp.algebra.ssralg]
R:2188 [in mathcomp.algebra.ssralg]
R:219 [in mathcomp.algebra.ring_quotient]
r:22 [in mathcomp.fingroup.presentation]
R:220 [in mathcomp.fingroup.morphism]
r:220 [in mathcomp.ssreflect.bigop]
R:2222 [in mathcomp.algebra.ssralg]
R:223 [in mathcomp.algebra.ring_quotient]
R:2234 [in mathcomp.algebra.ssralg]
R:2236 [in mathcomp.algebra.ssralg]
R:2238 [in mathcomp.algebra.ssralg]
R:2240 [in mathcomp.algebra.ssralg]
R:227 [in mathcomp.algebra.ring_quotient]
r:228 [in mathcomp.fingroup.gproduct]
R:2291 [in mathcomp.algebra.ssrnum]
R:2293 [in mathcomp.algebra.ssrnum]
R:2299 [in mathcomp.algebra.matrix]
r:230 [in mathcomp.algebra.polydiv]
r:232 [in mathcomp.algebra.polydiv]
R:232 [in mathcomp.algebra.ssrnum]
r:2322 [in mathcomp.algebra.matrix]
R:2325 [in mathcomp.algebra.matrix]
R:234 [in mathcomp.algebra.ssrnum]
R:2340 [in mathcomp.algebra.ssrnum]
R:2342 [in mathcomp.algebra.ssrnum]
R:2344 [in mathcomp.algebra.ssrnum]
R:2347 [in mathcomp.algebra.ssrnum]
r:235 [in mathcomp.fingroup.gproduct]
r:235 [in mathcomp.ssreflect.bigop]
r:237 [in mathcomp.algebra.polydiv]
R:2371 [in mathcomp.algebra.ssralg]
R:239 [in mathcomp.algebra.ssrnum]
r:24 [in mathcomp.ssreflect.ssrbool]
r:241 [in mathcomp.character.classfun]
R:241 [in mathcomp.algebra.ssrnum]
r:248 [in mathcomp.ssreflect.bigop]
R:25 [in mathcomp.algebra.finalg]
r:254 [in mathcomp.field.fieldext]
r:254 [in mathcomp.character.classfun]
r:259 [in mathcomp.ssreflect.bigop]
R:26 [in mathcomp.algebra.countalg]
R:26 [in mathcomp.algebra.zmodp]
R:260 [in mathcomp.fingroup.quotient]
r:261 [in mathcomp.field.closed_field]
r:262 [in mathcomp.fingroup.gproduct]
r:265 [in mathcomp.solvable.extremal]
r:269 [in mathcomp.ssreflect.bigop]
r:27 [in mathcomp.fingroup.presentation]
R:273 [in mathcomp.fingroup.morphism]
R:276 [in mathcomp.fingroup.morphism]
r:279 [in mathcomp.algebra.ssrint]
r:28 [in mathcomp.field.separable]
R:280 [in mathcomp.fingroup.morphism]
r:2803 [in mathcomp.algebra.ssrnum]
r:283 [in mathcomp.ssreflect.bigop]
r:285 [in mathcomp.algebra.ssrint]
r:285 [in mathcomp.algebra.ssrnum]
r:287 [in mathcomp.algebra.mxalgebra]
r:289 [in mathcomp.solvable.abelian]
r:292 [in mathcomp.ssreflect.bigop]
r:294 [in mathcomp.ssreflect.bigop]
r:299 [in mathcomp.ssreflect.bigop]
R:30 [in mathcomp.algebra.countalg]
r:30 [in mathcomp.ssreflect.ssrbool]
r:303 [in mathcomp.character.character]
R:3033 [in mathcomp.algebra.ssrnum]
r:305 [in mathcomp.ssreflect.bigop]
r:309 [in mathcomp.character.classfun]
R:31 [in mathcomp.algebra.zmodp]
r:311 [in mathcomp.ssreflect.bigop]
r:315 [in mathcomp.field.fieldext]
r:316 [in mathcomp.algebra.vector]
r:317 [in mathcomp.ssreflect.bigop]
R:32 [in mathcomp.field.falgebra]
R:322 [in mathcomp.algebra.mxpoly]
R:322 [in mathcomp.solvable.extremal]
r:324 [in mathcomp.algebra.poly]
r:324 [in mathcomp.ssreflect.bigop]
R:328 [in mathcomp.algebra.mxpoly]
R:33 [in mathcomp.algebra.vector]
r:333 [in mathcomp.fingroup.gproduct]
r:338 [in mathcomp.character.classfun]
R:34 [in mathcomp.field.separable]
R:34 [in mathcomp.fingroup.morphism]
r:340 [in mathcomp.fingroup.gproduct]
r:345 [in mathcomp.ssreflect.bigop]
r:347 [in mathcomp.fingroup.gproduct]
r:347 [in mathcomp.character.character]
R:35 [in mathcomp.algebra.polyXY]
r:353 [in mathcomp.ssreflect.bigop]
r:357 [in mathcomp.algebra.mxpoly]
r:358 [in mathcomp.algebra.polydiv]
r:359 [in mathcomp.ssreflect.bigop]
R:36 [in mathcomp.algebra.countalg]
r:361 [in mathcomp.algebra.polydiv]
r:364 [in mathcomp.ssreflect.bigop]
R:368 [in mathcomp.algebra.interval]
r:368 [in mathcomp.ssreflect.bigop]
R:37 [in mathcomp.algebra.matrix]
r:370 [in mathcomp.algebra.ssralg]
r:370 [in mathcomp.algebra.poly]
r:371 [in mathcomp.ssreflect.bigop]
R:373 [in mathcomp.algebra.interval]
r:376 [in mathcomp.fingroup.gproduct]
R:377 [in mathcomp.field.closed_field]
r:380 [in mathcomp.field.galois]
R:381 [in mathcomp.field.closed_field]
r:383 [in mathcomp.fingroup.gproduct]
R:383 [in mathcomp.fingroup.morphism]
R:386 [in mathcomp.character.classfun]
R:386 [in mathcomp.fingroup.morphism]
r:388 [in mathcomp.algebra.mxpoly]
r:389 [in mathcomp.algebra.mxpoly]
R:391 [in mathcomp.character.classfun]
r:395 [in mathcomp.algebra.ssralg]
R:397 [in mathcomp.algebra.mxpoly]
r:397 [in mathcomp.ssreflect.bigop]
r:398 [in mathcomp.algebra.intdiv]
R:40 [in mathcomp.algebra.countalg]
R:40 [in mathcomp.algebra.matrix]
R:40 [in mathcomp.algebra.finalg]
R:402 [in mathcomp.algebra.mxpoly]
r:402 [in mathcomp.ssreflect.bigop]
r:404 [in mathcomp.field.galois]
r:405 [in mathcomp.field.galois]
R:407 [in mathcomp.character.classfun]
r:408 [in mathcomp.ssreflect.bigop]
R:409 [in mathcomp.algebra.mxpoly]
r:41 [in mathcomp.fingroup.morphism]
r:411 [in mathcomp.algebra.mxpoly]
R:412 [in mathcomp.character.character]
r:413 [in mathcomp.algebra.intdiv]
r:413 [in mathcomp.ssreflect.bigop]
r:417 [in mathcomp.field.galois]
R:419 [in mathcomp.algebra.intdiv]
R:420 [in mathcomp.algebra.intdiv]
r:420 [in mathcomp.field.galois]
R:420 [in mathcomp.fingroup.action]
R:423 [in mathcomp.fingroup.action]
r:423 [in mathcomp.fingroup.fingroup]
R:426 [in mathcomp.character.classfun]
R:429 [in mathcomp.character.classfun]
r:429 [in mathcomp.fingroup.gproduct]
r:43 [in mathcomp.field.cyclotomic]
R:43 [in mathcomp.algebra.matrix]
R:431 [in mathcomp.character.classfun]
r:433 [in mathcomp.algebra.polydiv]
r:433 [in mathcomp.fingroup.fingroup]
R:435 [in mathcomp.character.classfun]
r:436 [in mathcomp.algebra.polydiv]
r:436 [in mathcomp.fingroup.gproduct]
R:437 [in mathcomp.character.classfun]
r:438 [in mathcomp.algebra.ssrnum]
r:439 [in mathcomp.algebra.polydiv]
R:44 [in mathcomp.field.finfield]
R:44 [in mathcomp.algebra.finalg]
r:44 [in mathcomp.algebra.vector]
r:440 [in mathcomp.field.galois]
r:441 [in mathcomp.field.galois]
r:444 [in mathcomp.algebra.polydiv]
r:445 [in mathcomp.algebra.ssrnum]
R:448 [in mathcomp.character.classfun]
r:45 [in mathcomp.algebra.vector]
R:450 [in mathcomp.character.classfun]
R:456 [in mathcomp.algebra.ssrint]
R:46 [in mathcomp.algebra.countalg]
R:46 [in mathcomp.algebra.matrix]
R:46 [in mathcomp.field.finfield]
R:46 [in mathcomp.algebra.finalg]
r:461 [in mathcomp.field.galois]
r:461 [in mathcomp.character.mxrepresentation]
R:47 [in mathcomp.algebra.mxpoly]
r:476 [in mathcomp.character.character]
r:477 [in mathcomp.ssreflect.prime]
R:48 [in mathcomp.field.finfield]
r:480 [in mathcomp.algebra.mxpoly]
r:482 [in mathcomp.character.character]
R:487 [in mathcomp.algebra.ssralg]
r:49 [in mathcomp.field.separable]
R:49 [in mathcomp.algebra.matrix]
r:493 [in mathcomp.algebra.mxpoly]
r:498 [in mathcomp.algebra.mxpoly]
r:5 [in mathcomp.ssreflect.choice]
r:5 [in mathcomp.character.mxrepresentation]
R:50 [in mathcomp.algebra.countalg]
r:50 [in mathcomp.field.separable]
R:50 [in mathcomp.field.finfield]
r:506 [in mathcomp.algebra.polydiv]
r:515 [in mathcomp.algebra.mxpoly]
R:517 [in mathcomp.algebra.interval]
R:517 [in mathcomp.algebra.ssralg]
R:52 [in mathcomp.algebra.matrix]
R:52 [in mathcomp.field.finfield]
R:520 [in mathcomp.algebra.interval]
R:523 [in mathcomp.algebra.interval]
R:526 [in mathcomp.algebra.interval]
r:526 [in mathcomp.ssreflect.bigop]
R:529 [in mathcomp.algebra.interval]
r:53 [in mathcomp.field.separable]
R:531 [in mathcomp.ssreflect.finset]
R:532 [in mathcomp.algebra.interval]
r:534 [in mathcomp.ssreflect.bigop]
r:539 [in mathcomp.algebra.polydiv]
r:54 [in mathcomp.field.cyclotomic]
r:540 [in mathcomp.algebra.polydiv]
r:541 [in mathcomp.ssreflect.bigop]
r:55 [in mathcomp.field.cyclotomic]
R:55 [in mathcomp.algebra.matrix]
r:556 [in mathcomp.fingroup.fingroup]
R:557 [in mathcomp.algebra.ssrint]
r:56 [in mathcomp.field.cyclotomic]
R:56 [in mathcomp.algebra.countalg]
r:560 [in mathcomp.algebra.ssralg]
r:567 [in mathcomp.algebra.ssralg]
R:57 [in mathcomp.field.cyclotomic]
R:574 [in mathcomp.solvable.pgroup]
r:574 [in mathcomp.algebra.vector]
R:578 [in mathcomp.algebra.ssralg]
R:58 [in mathcomp.algebra.matrix]
R:58 [in mathcomp.ssreflect.bigop]
r:586 [in mathcomp.algebra.polydiv]
r:589 [in mathcomp.algebra.polydiv]
R:59 [in mathcomp.field.finfield]
R:590 [in mathcomp.algebra.ssralg]
r:598 [in mathcomp.algebra.polydiv]
R:6 [in mathcomp.algebra.poly]
R:60 [in mathcomp.algebra.countalg]
R:60 [in mathcomp.algebra.finalg]
r:601 [in mathcomp.algebra.polydiv]
R:604 [in mathcomp.ssreflect.bigop]
R:608 [in mathcomp.algebra.ssralg]
R:61 [in mathcomp.algebra.matrix]
R:61 [in mathcomp.field.finfield]
R:62 [in mathcomp.algebra.countalg]
R:62 [in mathcomp.fingroup.morphism]
R:62 [in mathcomp.ssreflect.bigop]
r:620 [in mathcomp.ssreflect.bigop]
R:63 [in mathcomp.field.finfield]
r:632 [in mathcomp.algebra.ssrnum]
R:634 [in mathcomp.solvable.abelian]
R:637 [in mathcomp.character.classfun]
r:638 [in mathcomp.algebra.ssrnum]
R:639 [in mathcomp.solvable.abelian]
r:639 [in mathcomp.ssreflect.bigop]
R:64 [in mathcomp.algebra.matrix]
R:64 [in mathcomp.algebra.finalg]
r:641 [in mathcomp.ssreflect.bigop]
r:645 [in mathcomp.ssreflect.bigop]
r:647 [in mathcomp.algebra.polydiv]
R:65 [in mathcomp.field.finfield]
R:65 [in mathcomp.fingroup.morphism]
r:65 [in mathcomp.solvable.center]
r:650 [in mathcomp.algebra.polydiv]
r:653 [in mathcomp.algebra.ssrnum]
R:653 [in mathcomp.algebra.poly]
R:654 [in mathcomp.algebra.poly]
R:655 [in mathcomp.algebra.poly]
R:656 [in mathcomp.algebra.poly]
r:658 [in mathcomp.ssreflect.bigop]
r:66 [in mathcomp.character.classfun]
R:66 [in mathcomp.algebra.finalg]
R:66 [in mathcomp.fingroup.morphism]
r:662 [in mathcomp.ssreflect.bigop]
r:663 [in mathcomp.algebra.vector]
r:668 [in mathcomp.algebra.polydiv]
R:668 [in mathcomp.ssreflect.finset]
r:668 [in mathcomp.ssreflect.bigop]
R:67 [in mathcomp.field.finfield]
R:67 [in mathcomp.ssreflect.bigop]
r:670 [in mathcomp.algebra.polydiv]
r:673 [in mathcomp.algebra.vector]
r:674 [in mathcomp.algebra.polydiv]
r:677 [in mathcomp.algebra.polydiv]
r:678 [in mathcomp.ssreflect.bigop]
R:68 [in mathcomp.algebra.countalg]
R:68 [in mathcomp.algebra.ssrnum]
r:684 [in mathcomp.ssreflect.bigop]
r:688 [in mathcomp.algebra.ssralg]
R:69 [in mathcomp.field.finfield]
r:691 [in mathcomp.ssreflect.bigop]
r:698 [in mathcomp.ssreflect.bigop]
r:7 [in mathcomp.algebra.polydiv]
r:7 [in mathcomp.ssreflect.ssrbool]
R:7 [in mathcomp.algebra.poly]
R:70 [in mathcomp.fingroup.morphism]
r:70 [in mathcomp.ssreflect.bigop]
r:705 [in mathcomp.ssreflect.bigop]
r:71 [in mathcomp.character.mxabelem]
R:71 [in mathcomp.algebra.ssrnum]
r:711 [in mathcomp.algebra.polydiv]
R:72 [in mathcomp.algebra.countalg]
R:72 [in mathcomp.algebra.finalg]
R:72 [in mathcomp.ssreflect.bigop]
r:729 [in mathcomp.algebra.polydiv]
R:73 [in mathcomp.algebra.ssrnum]
r:730 [in mathcomp.algebra.matrix]
R:731 [in mathcomp.algebra.ssrint]
r:732 [in mathcomp.algebra.polydiv]
r:735 [in mathcomp.algebra.polydiv]
R:735 [in mathcomp.algebra.ssrint]
R:74 [in mathcomp.ssreflect.ssrAC]
r:740 [in mathcomp.algebra.polydiv]
r:742 [in mathcomp.algebra.matrix]
r:75 [in mathcomp.solvable.nilpotent]
r:753 [in mathcomp.algebra.poly]
r:755 [in mathcomp.algebra.matrix]
R:756 [in mathcomp.character.classfun]
r:756 [in mathcomp.algebra.poly]
r:757 [in mathcomp.algebra.polydiv]
R:76 [in mathcomp.algebra.finalg]
R:76 [in mathcomp.fingroup.morphism]
r:76 [in mathcomp.solvable.center]
R:765 [in mathcomp.ssreflect.finset]
r:765 [in mathcomp.algebra.matrix]
r:769 [in mathcomp.algebra.ssralg]
R:78 [in mathcomp.algebra.countalg]
R:78 [in mathcomp.algebra.finalg]
R:78 [in mathcomp.fingroup.morphism]
r:780 [in mathcomp.algebra.mxalgebra]
r:782 [in mathcomp.algebra.ssralg]
r:782 [in mathcomp.algebra.mxalgebra]
r:784 [in mathcomp.algebra.poly]
R:79 [in mathcomp.ssreflect.ssrAC]
r:793 [in mathcomp.ssreflect.bigop]
r:799 [in mathcomp.algebra.polydiv]
r:8 [in mathcomp.ssreflect.prime]
r:8 [in mathcomp.solvable.gseries]
R:8 [in mathcomp.algebra.poly]
R:80 [in mathcomp.fingroup.morphism]
r:802 [in mathcomp.algebra.polydiv]
r:805 [in mathcomp.algebra.polydiv]
R:807 [in mathcomp.algebra.ssralg]
r:807 [in mathcomp.algebra.poly]
r:810 [in mathcomp.algebra.poly]
R:813 [in mathcomp.algebra.ssralg]
R:814 [in mathcomp.algebra.ssralg]
r:815 [in mathcomp.ssreflect.bigop]
R:82 [in mathcomp.algebra.countalg]
r:820 [in mathcomp.ssreflect.bigop]
R:821 [in mathcomp.algebra.poly]
r:822 [in mathcomp.algebra.vector]
R:822 [in mathcomp.algebra.poly]
R:825 [in mathcomp.algebra.ssrint]
r:827 [in mathcomp.ssreflect.bigop]
r:83 [in mathcomp.solvable.nilpotent]
r:830 [in mathcomp.algebra.polydiv]
R:830 [in mathcomp.algebra.ssrint]
r:832 [in mathcomp.algebra.polydiv]
r:834 [in mathcomp.algebra.polydiv]
R:837 [in mathcomp.algebra.ssrint]
r:839 [in mathcomp.ssreflect.ssrnat]
R:84 [in mathcomp.fingroup.morphism]
r:840 [in mathcomp.ssreflect.bigop]
R:843 [in mathcomp.algebra.ssrint]
r:844 [in mathcomp.ssreflect.finset]
r:846 [in mathcomp.ssreflect.bigop]
r:852 [in mathcomp.ssreflect.ssrnat]
R:854 [in mathcomp.algebra.matrix]
r:854 [in mathcomp.ssreflect.bigop]
r:862 [in mathcomp.algebra.polydiv]
r:863 [in mathcomp.ssreflect.ssrnat]
r:868 [in mathcomp.ssreflect.finset]
R:87 [in mathcomp.solvable.pgroup]
R:87 [in mathcomp.solvable.hall]
R:872 [in mathcomp.ssreflect.seq]
r:874 [in mathcomp.ssreflect.finset]
r:875 [in mathcomp.ssreflect.bigop]
r:877 [in mathcomp.ssreflect.ssrnat]
R:88 [in mathcomp.algebra.countalg]
r:88 [in mathcomp.character.inertia]
r:885 [in mathcomp.ssreflect.finset]
r:886 [in mathcomp.algebra.ssrnum]
R:89 [in mathcomp.fingroup.morphism]
r:891 [in mathcomp.algebra.matrix]
r:892 [in mathcomp.algebra.ssrnum]
r:892 [in mathcomp.algebra.ssralg]
r:893 [in mathcomp.algebra.vector]
r:895 [in mathcomp.algebra.polydiv]
r:895 [in mathcomp.algebra.vector]
r:898 [in mathcomp.algebra.ssrnum]
r:899 [in mathcomp.algebra.polydiv]
r:899 [in mathcomp.fingroup.fingroup]
R:9 [in mathcomp.field.cyclotomic]
r:9 [in mathcomp.field.algnum]
r:90 [in mathcomp.algebra.polydiv]
r:903 [in mathcomp.algebra.polydiv]
r:905 [in mathcomp.fingroup.fingroup]
R:906 [in mathcomp.algebra.poly]
r:907 [in mathcomp.algebra.ssrnum]
R:907 [in mathcomp.algebra.poly]
R:908 [in mathcomp.character.character]
R:908 [in mathcomp.algebra.poly]
R:909 [in mathcomp.algebra.poly]
r:91 [in mathcomp.solvable.nilpotent]
R:910 [in mathcomp.algebra.poly]
R:911 [in mathcomp.algebra.poly]
R:92 [in mathcomp.algebra.countalg]
R:93 [in mathcomp.algebra.ssrnum]
R:93 [in mathcomp.fingroup.morphism]
r:944 [in mathcomp.algebra.poly]
r:950 [in mathcomp.algebra.polydiv]
r:953 [in mathcomp.algebra.polydiv]
R:969 [in mathcomp.algebra.ssralg]
R:97 [in mathcomp.algebra.ssrnum]
r:970 [in mathcomp.algebra.polydiv]
r:973 [in mathcomp.algebra.polydiv]
r:976 [in mathcomp.algebra.polydiv]
R:978 [in mathcomp.algebra.ssralg]
R:98 [in mathcomp.algebra.countalg]
r:99 [in mathcomp.solvable.nilpotent]

Global Index

_

(69505 entries)

Notation Index

H

J

T

W

X

Y

_

(1943 entries)

Binder Index

_

other

(39748 entries)

Module Index

H

J

K

L

T

W

X

Y

Z

_

other

(379 entries)

Variable Index

J

W

X

Y

_

other

(3958 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(13542 entries)

Constructor Index

J

K

W

Y

_

other

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

(134 entries)

Projection Index

H

J

K

L

W

X

Y

_

other

(452 entries)

Section Index

J

W

X

Y

_

other

(1344 entries)

Abbreviation Index

Y

_

other

(1014 entries)

Definition Index

Y

_

other

(6127 entries)

Record Index

B

H

J

K

L

W

X

Y

_

other

(248 entries)