mathcomp.ssreflect.tuple

Global Index

_

(71649 entries)

Notation Index

H

J

T

W

X

Y

_

(1792 entries)

Binder Index

_

other

(46193 entries)

Module Index

H

J

K

L

W

X

Y

_

other

(266 entries)

Variable Index

J

W

X

Y

_

other

(3623 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(14204 entries)

Constructor Index

J

K

W

Y

_

other

(259 entries)

Axiom Index

B

C

D

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(8 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(134 entries)

Projection Index

H

I

J

K

L

N

O

Q

U

W

X

Y

Z

_

other

(44 entries)

Section Index

J

W

X

Y

_

other

(1276 entries)

Abbreviation Index

Y

_

other

(682 entries)

Definition Index

Y

_

other

(3041 entries)

Record Index

F

H

I

J

K

L

O

Q

U

W

X

Y

Z

_

other

(36 entries)

R (binder)

real:2406 [in mathcomp.algebra.ssrnum]
recf:549 [in mathcomp.algebra.mxpoly]
redg:1565 [in mathcomp.algebra.ssralg]
repr_ofK_subproof:5 [in mathcomp.ssreflect.generic_quotient]
repr_of:3 [in mathcomp.ssreflect.generic_quotient]
rfG:656 [in mathcomp.character.character]
rGf:1422 [in mathcomp.character.mxrepresentation]
rG0:156 [in mathcomp.character.mxrepresentation]
rG1:109 [in mathcomp.character.character]
rG1:112 [in mathcomp.character.character]
rG1:1263 [in mathcomp.character.mxrepresentation]
rG1:1418 [in mathcomp.character.mxrepresentation]
rG1:166 [in mathcomp.character.character]
rG1:181 [in mathcomp.character.character]
rG1:183 [in mathcomp.character.character]
rG1:310 [in mathcomp.character.character]
rG1:316 [in mathcomp.character.character]
rG1:365 [in mathcomp.character.character]
rG1:829 [in mathcomp.character.mxrepresentation]
rG1:838 [in mathcomp.character.mxrepresentation]
rG1:844 [in mathcomp.character.mxrepresentation]
rG1:849 [in mathcomp.character.mxrepresentation]
rG1:854 [in mathcomp.character.mxrepresentation]
rG1:868 [in mathcomp.character.mxrepresentation]
rG1:872 [in mathcomp.character.mxrepresentation]
rG1:877 [in mathcomp.character.mxrepresentation]
rG1:881 [in mathcomp.character.mxrepresentation]
rG1:891 [in mathcomp.character.mxrepresentation]
rG1:896 [in mathcomp.character.mxrepresentation]
rG2:110 [in mathcomp.character.character]
rG2:113 [in mathcomp.character.character]
rG2:1264 [in mathcomp.character.mxrepresentation]
rG2:1419 [in mathcomp.character.mxrepresentation]
rG2:167 [in mathcomp.character.character]
rG2:182 [in mathcomp.character.character]
rG2:184 [in mathcomp.character.character]
rG2:311 [in mathcomp.character.character]
rG2:317 [in mathcomp.character.character]
rG2:366 [in mathcomp.character.character]
rG2:831 [in mathcomp.character.mxrepresentation]
rG2:839 [in mathcomp.character.mxrepresentation]
rG2:845 [in mathcomp.character.mxrepresentation]
rG2:850 [in mathcomp.character.mxrepresentation]
rG2:855 [in mathcomp.character.mxrepresentation]
rG2:869 [in mathcomp.character.mxrepresentation]
rG2:873 [in mathcomp.character.mxrepresentation]
rG2:878 [in mathcomp.character.mxrepresentation]
rG2:882 [in mathcomp.character.mxrepresentation]
rG2:892 [in mathcomp.character.mxrepresentation]
rG2:897 [in mathcomp.character.mxrepresentation]
rG3:851 [in mathcomp.character.mxrepresentation]
rG:1001 [in mathcomp.character.character]
rG:1042 [in mathcomp.character.character]
rG:1421 [in mathcomp.character.mxrepresentation]
rG:1440 [in mathcomp.character.mxrepresentation]
rG:173 [in mathcomp.character.character]
rG:176 [in mathcomp.character.character]
rG:178 [in mathcomp.character.character]
rG:188 [in mathcomp.character.character]
rG:195 [in mathcomp.character.character]
rG:215 [in mathcomp.character.mxabelem]
rG:237 [in mathcomp.character.character]
rG:304 [in mathcomp.character.character]
rG:319 [in mathcomp.character.character]
rG:320 [in mathcomp.character.character]
rG:352 [in mathcomp.character.character]
rG:362 [in mathcomp.character.character]
rG:371 [in mathcomp.character.character]
rG:426 [in mathcomp.character.character]
rG:564 [in mathcomp.character.character]
rG:570 [in mathcomp.character.character]
rG:602 [in mathcomp.character.character]
rG:628 [in mathcomp.character.character]
rG:799 [in mathcomp.character.mxrepresentation]
rG:810 [in mathcomp.character.mxrepresentation]
rG:812 [in mathcomp.character.mxrepresentation]
rG:815 [in mathcomp.character.mxrepresentation]
rG:817 [in mathcomp.character.mxrepresentation]
rG:820 [in mathcomp.character.mxrepresentation]
rG:841 [in mathcomp.character.mxrepresentation]
rG:861 [in mathcomp.character.mxrepresentation]
rG:884 [in mathcomp.character.mxrepresentation]
rG:89 [in mathcomp.character.integral_char]
rG:93 [in mathcomp.character.integral_char]
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:462 [in mathcomp.ssreflect.prime]
rho:465 [in mathcomp.ssreflect.prime]
rho:468 [in mathcomp.ssreflect.prime]
rho:473 [in mathcomp.ssreflect.prime]
rho:518 [in mathcomp.ssreflect.prime]
rho:548 [in mathcomp.ssreflect.prime]
rho:551 [in mathcomp.ssreflect.prime]
rho:569 [in mathcomp.solvable.pgroup]
rho:572 [in mathcomp.solvable.pgroup]
rho:575 [in mathcomp.solvable.pgroup]
rho:578 [in mathcomp.solvable.pgroup]
rho:583 [in mathcomp.solvable.pgroup]
rho:592 [in mathcomp.solvable.pgroup]
rhs:100 [in mathcomp.ssreflect.choice]
rhs:107 [in mathcomp.ssreflect.choice]
rid:102 [in mathcomp.ssreflect.ssrAC]
ringS:576 [in mathcomp.algebra.poly]
ringS:614 [in mathcomp.algebra.poly]
ringS:657 [in mathcomp.algebra.poly]
ringS:798 [in mathcomp.algebra.poly]
rI:1582 [in mathcomp.ssreflect.bigop]
rI:1605 [in mathcomp.ssreflect.bigop]
rI:2199 [in mathcomp.ssreflect.bigop]
rI:2221 [in mathcomp.ssreflect.bigop]
rI:2354 [in mathcomp.ssreflect.bigop]
rI:340 [in mathcomp.algebra.poly]
rI:349 [in mathcomp.algebra.poly]
rI:356 [in mathcomp.algebra.poly]
rJ:1583 [in mathcomp.ssreflect.bigop]
rJ:1606 [in mathcomp.ssreflect.bigop]
rJ:2200 [in mathcomp.ssreflect.bigop]
rJ:2222 [in mathcomp.ssreflect.bigop]
rJ:2355 [in mathcomp.ssreflect.bigop]
rk:183 [in mathcomp.algebra.vector]
Rle:2363 [in mathcomp.algebra.ssrnum]
Rle:2411 [in mathcomp.algebra.ssrnum]
Rle:2452 [in mathcomp.algebra.ssrnum]
Rlt:2364 [in mathcomp.algebra.ssrnum]
Rlt:2412 [in mathcomp.algebra.ssrnum]
Rlt:2451 [in mathcomp.algebra.ssrnum]
rmorphism_subproof:837 [in mathcomp.algebra.ssralg]
rngS:2183 [in mathcomp.algebra.ssralg]
RoverFp:175 [in mathcomp.field.finfield]
row1:718 [in mathcomp.algebra.matrix]
row3:720 [in mathcomp.algebra.matrix]
rpredNr:1937 [in mathcomp.algebra.ssralg]
rpredVr:1952 [in mathcomp.algebra.ssralg]
rpredZ:1958 [in mathcomp.algebra.ssralg]
rpred0D:1942 [in mathcomp.algebra.ssralg]
rpred1M:1947 [in mathcomp.algebra.ssralg]
rP:153 [in mathcomp.ssreflect.ssrbool]
rP:71 [in mathcomp.ssreflect.ssrbool]
rqT:81 [in mathcomp.algebra.ring_quotient]
rqT:82 [in mathcomp.algebra.ring_quotient]
rr:1979 [in mathcomp.ssreflect.bigop]
rr:206 [in mathcomp.field.closed_field]
rr:212 [in mathcomp.field.closed_field]
rR:252 [in mathcomp.algebra.mxpoly]
rR:260 [in mathcomp.algebra.rat]
rR:263 [in mathcomp.algebra.rat]
rr:470 [in mathcomp.algebra.polydiv]
rr:479 [in mathcomp.algebra.polydiv]
rR:61 [in mathcomp.field.algnum]
rr:68 [in mathcomp.algebra.polydiv]
rr:77 [in mathcomp.algebra.polydiv]
rR:836 [in mathcomp.algebra.poly]
rs1:289 [in mathcomp.field.falgebra]
rs2:290 [in mathcomp.field.falgebra]
rs:10 [in mathcomp.field.galois]
rs:1099 [in mathcomp.algebra.poly]
rs:1119 [in mathcomp.algebra.poly]
rs:1121 [in mathcomp.algebra.poly]
rs:1150 [in mathcomp.algebra.poly]
rs:1154 [in mathcomp.algebra.poly]
rs:1160 [in mathcomp.algebra.poly]
rs:1162 [in mathcomp.algebra.poly]
rs:1169 [in mathcomp.algebra.poly]
rs:1174 [in mathcomp.algebra.poly]
rs:1175 [in mathcomp.algebra.poly]
rs:188 [in mathcomp.algebra.polydiv]
rs:215 [in mathcomp.solvable.cyclic]
rs:268 [in mathcomp.field.separable]
rs:273 [in mathcomp.field.falgebra]
rs:275 [in mathcomp.field.falgebra]
rs:287 [in mathcomp.field.falgebra]
rs:32 [in mathcomp.field.fieldext]
rs:388 [in mathcomp.algebra.polydiv]
rs:6 [in mathcomp.field.galois]
rs:778 [in mathcomp.algebra.mxpoly]
rs:838 [in mathcomp.algebra.mxpoly]
rs:839 [in mathcomp.algebra.mxpoly]
rs:843 [in mathcomp.algebra.mxpoly]
rs:855 [in mathcomp.algebra.mxpoly]
rs:856 [in mathcomp.algebra.mxpoly]
RtoK:379 [in mathcomp.algebra.mxpoly]
RtoK:385 [in mathcomp.algebra.mxpoly]
rT':29 [in mathcomp.fingroup.action]
rT:1 [in mathcomp.ssreflect.ssrfun]
rT:10 [in mathcomp.ssreflect.ssrfun]
rT:1017 [in mathcomp.character.character]
rT:102 [in mathcomp.solvable.gfunctor]
rT:1023 [in mathcomp.character.character]
rT:107 [in mathcomp.solvable.gfunctor]
rt:109 [in mathcomp.field.closed_field]
rT:112 [in mathcomp.solvable.gfunctor]
rT:118 [in mathcomp.solvable.gfunctor]
rT:119 [in mathcomp.solvable.cyclic]
rT:123 [in mathcomp.solvable.gfunctor]
rT:123 [in mathcomp.solvable.maximal]
rT:128 [in mathcomp.solvable.maximal]
rT:13 [in mathcomp.ssreflect.ssrfun]
rT:1328 [in mathcomp.ssreflect.seq]
rT:1333 [in mathcomp.ssreflect.seq]
rT:148 [in mathcomp.solvable.center]
rT:149 [in mathcomp.ssreflect.ssrbool]
rT:15 [in mathcomp.field.fieldext]
rT:151 [in mathcomp.solvable.commutator]
rT:152 [in mathcomp.solvable.gseries]
rT:16 [in mathcomp.ssreflect.ssrfun]
rT:17 [in mathcomp.fingroup.action]
rT:171 [in mathcomp.solvable.commutator]
rT:18 [in mathcomp.field.fieldext]
rT:19 [in mathcomp.ssreflect.ssrfun]
rT:21 [in mathcomp.field.fieldext]
rT:212 [in mathcomp.ssreflect.eqtype]
rT:22 [in mathcomp.ssreflect.ssrfun]
rT:253 [in mathcomp.solvable.nilpotent]
rT:256 [in mathcomp.solvable.nilpotent]
rT:260 [in mathcomp.fingroup.quotient]
rT:27 [in mathcomp.ssreflect.ssrfun]
rT:28 [in mathcomp.fingroup.action]
rT:32 [in mathcomp.ssreflect.ssrfun]
rT:33 [in mathcomp.ssreflect.finfun]
rT:38 [in mathcomp.ssreflect.ssrfun]
rT:39 [in mathcomp.solvable.maximal]
rT:412 [in mathcomp.fingroup.morphism]
rT:419 [in mathcomp.fingroup.morphism]
rT:425 [in mathcomp.fingroup.morphism]
rT:427 [in mathcomp.solvable.abelian]
rT:429 [in mathcomp.fingroup.morphism]
rT:437 [in mathcomp.fingroup.morphism]
rT:44 [in mathcomp.ssreflect.ssrfun]
rT:441 [in mathcomp.fingroup.morphism]
rT:442 [in mathcomp.solvable.abelian]
rT:445 [in mathcomp.fingroup.morphism]
rT:446 [in mathcomp.solvable.abelian]
rT:449 [in mathcomp.fingroup.morphism]
rT:45 [in mathcomp.solvable.maximal]
rT:455 [in mathcomp.fingroup.morphism]
rT:460 [in mathcomp.fingroup.morphism]
rT:466 [in mathcomp.solvable.pgroup]
rT:473 [in mathcomp.solvable.pgroup]
rT:49 [in mathcomp.solvable.maximal]
rT:522 [in mathcomp.ssreflect.finset]
rT:530 [in mathcomp.ssreflect.finset]
rT:539 [in mathcomp.ssreflect.finset]
rT:57 [in mathcomp.fingroup.presentation]
rT:579 [in mathcomp.algebra.vector]
rT:59 [in mathcomp.solvable.center]
rT:599 [in mathcomp.solvable.pgroup]
rT:605 [in mathcomp.ssreflect.fintype]
rT:655 [in mathcomp.algebra.vector]
rT:658 [in mathcomp.algebra.vector]
rT:663 [in mathcomp.algebra.vector]
rT:668 [in mathcomp.algebra.vector]
rT:67 [in mathcomp.ssreflect.ssrbool]
rT:67 [in mathcomp.solvable.maximal]
rT:671 [in mathcomp.algebra.vector]
rT:674 [in mathcomp.algebra.vector]
rT:678 [in mathcomp.algebra.vector]
rT:69 [in mathcomp.fingroup.presentation]
rT:70 [in mathcomp.solvable.gseries]
rT:71 [in mathcomp.fingroup.presentation]
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:86 [in mathcomp.ssreflect.finfun]
rT:860 [in mathcomp.character.classfun]
rT:864 [in mathcomp.character.classfun]
rT:867 [in mathcomp.algebra.vector]
rT:869 [in mathcomp.algebra.vector]
rT:87 [in mathcomp.ssreflect.finfun]
rT:87 [in mathcomp.fingroup.presentation]
rT:88 [in mathcomp.ssreflect.finfun]
rT:88 [in mathcomp.ssreflect.ssrbool]
rT:880 [in mathcomp.ssreflect.finset]
rT:89 [in mathcomp.ssreflect.finfun]
rT:92 [in mathcomp.fingroup.presentation]
rT:94 [in mathcomp.ssreflect.ssrbool]
rT:99 [in mathcomp.fingroup.presentation]
rU:119 [in mathcomp.character.character]
rU:127 [in mathcomp.character.character]
rV:120 [in mathcomp.character.character]
rv:170 [in mathcomp.algebra.vector]
rv:19 [in mathcomp.field.finfield]
rV:288 [in mathcomp.algebra.ssrint]
rw:1022 [in mathcomp.algebra.vector]
rw:1026 [in mathcomp.algebra.vector]
rW:149 [in mathcomp.character.character]
rW:156 [in mathcomp.character.character]
rxx:204 [in mathcomp.ssreflect.generic_quotient]
Rx:157 [in mathcomp.field.algebraics_fundamentals]
rX:175 [in mathcomp.solvable.finmodule]
rX:188 [in mathcomp.solvable.finmodule]
rz:214 [in mathcomp.field.galois]
r_a:519 [in mathcomp.field.galois]
R_:3285 [in mathcomp.algebra.matrix]
r_:3096 [in mathcomp.algebra.matrix]
R_:3066 [in mathcomp.algebra.matrix]
R_:3059 [in mathcomp.algebra.matrix]
R_:3047 [in mathcomp.algebra.matrix]
R_:2854 [in mathcomp.algebra.matrix]
R_:2835 [in mathcomp.algebra.matrix]
R_:2809 [in mathcomp.algebra.matrix]
R_:2795 [in mathcomp.algebra.matrix]
R_:2790 [in mathcomp.algebra.matrix]
R_:2783 [in mathcomp.algebra.matrix]
R_:2752 [in mathcomp.algebra.matrix]
r_:883 [in mathcomp.ssreflect.bigop]
r_:872 [in mathcomp.ssreflect.bigop]
R_:1800 [in mathcomp.algebra.mxalgebra]
R_:1609 [in mathcomp.algebra.mxalgebra]
R'_:2796 [in mathcomp.algebra.matrix]
R'_:2784 [in mathcomp.algebra.matrix]
R':2010 [in mathcomp.ssreflect.seq]
r':2250 [in mathcomp.ssreflect.seq]
r':2258 [in mathcomp.ssreflect.seq]
r':2268 [in mathcomp.ssreflect.seq]
r':2274 [in mathcomp.ssreflect.seq]
r':2312 [in mathcomp.ssreflect.seq]
r':2352 [in mathcomp.ssreflect.seq]
r':2356 [in mathcomp.ssreflect.seq]
r':2361 [in mathcomp.ssreflect.seq]
r':2365 [in mathcomp.ssreflect.seq]
r':2373 [in mathcomp.ssreflect.seq]
R':557 [in mathcomp.algebra.ssrint]
R':759 [in mathcomp.algebra.ssrint]
r1:1113 [in mathcomp.ssreflect.bigop]
r1:12 [in mathcomp.algebra.polydiv]
r1:1256 [in mathcomp.algebra.mxalgebra]
r1:131 [in mathcomp.field.closed_field]
r1:1371 [in mathcomp.ssreflect.bigop]
r1:1389 [in mathcomp.ssreflect.bigop]
r1:1406 [in mathcomp.ssreflect.bigop]
r1:143 [in mathcomp.field.closed_field]
R1:1589 [in mathcomp.algebra.mxalgebra]
R1:1595 [in mathcomp.algebra.mxalgebra]
R1:1602 [in mathcomp.algebra.mxalgebra]
R1:1631 [in mathcomp.algebra.mxalgebra]
R1:1639 [in mathcomp.algebra.mxalgebra]
R1:1644 [in mathcomp.algebra.mxalgebra]
R1:1652 [in mathcomp.algebra.mxalgebra]
r1:1656 [in mathcomp.ssreflect.seq]
R1:1662 [in mathcomp.algebra.mxalgebra]
R1:1671 [in mathcomp.algebra.mxalgebra]
R1:1679 [in mathcomp.algebra.mxalgebra]
R1:1696 [in mathcomp.algebra.mxalgebra]
R1:1703 [in mathcomp.algebra.mxalgebra]
R1:1710 [in mathcomp.algebra.mxalgebra]
R1:1716 [in mathcomp.algebra.mxalgebra]
R1:1724 [in mathcomp.algebra.mxalgebra]
R1:1729 [in mathcomp.algebra.mxalgebra]
R1:1734 [in mathcomp.algebra.mxalgebra]
r1:1781 [in mathcomp.ssreflect.bigop]
R1:1794 [in mathcomp.algebra.mxalgebra]
r1:1799 [in mathcomp.ssreflect.bigop]
r1:1816 [in mathcomp.ssreflect.bigop]
r1:188 [in mathcomp.field.separable]
r1:2022 [in mathcomp.ssreflect.bigop]
R1:2809 [in mathcomp.algebra.ssralg]
r1:286 [in mathcomp.fingroup.gproduct]
r1:366 [in mathcomp.algebra.intdiv]
r1:368 [in mathcomp.algebra.intdiv]
r1:370 [in mathcomp.algebra.intdiv]
R1:46 [in mathcomp.field.cyclotomic]
R1:481 [in mathcomp.character.classfun]
R1:485 [in mathcomp.character.classfun]
r1:511 [in mathcomp.ssreflect.div]
r1:513 [in mathcomp.ssreflect.div]
r1:515 [in mathcomp.ssreflect.div]
r1:556 [in mathcomp.ssreflect.bigop]
r1:623 [in mathcomp.ssreflect.bigop]
r1:637 [in mathcomp.ssreflect.bigop]
r1:647 [in mathcomp.ssreflect.bigop]
r2v:33 [in mathcomp.algebra.vector]
r2:1114 [in mathcomp.ssreflect.bigop]
r2:1257 [in mathcomp.algebra.mxalgebra]
r2:1372 [in mathcomp.ssreflect.bigop]
r2:1391 [in mathcomp.ssreflect.bigop]
r2:1407 [in mathcomp.ssreflect.bigop]
R2:1590 [in mathcomp.algebra.mxalgebra]
R2:1596 [in mathcomp.algebra.mxalgebra]
R2:1603 [in mathcomp.algebra.mxalgebra]
R2:1632 [in mathcomp.algebra.mxalgebra]
R2:1640 [in mathcomp.algebra.mxalgebra]
R2:1645 [in mathcomp.algebra.mxalgebra]
R2:1653 [in mathcomp.algebra.mxalgebra]
r2:1658 [in mathcomp.ssreflect.seq]
R2:1663 [in mathcomp.algebra.mxalgebra]
R2:1672 [in mathcomp.algebra.mxalgebra]
R2:1680 [in mathcomp.algebra.mxalgebra]
R2:1697 [in mathcomp.algebra.mxalgebra]
R2:1704 [in mathcomp.algebra.mxalgebra]
R2:1711 [in mathcomp.algebra.mxalgebra]
R2:1720 [in mathcomp.algebra.mxalgebra]
R2:1725 [in mathcomp.algebra.mxalgebra]
R2:1730 [in mathcomp.algebra.mxalgebra]
R2:1735 [in mathcomp.algebra.mxalgebra]
r2:1782 [in mathcomp.ssreflect.bigop]
R2:1795 [in mathcomp.algebra.mxalgebra]
r2:1801 [in mathcomp.ssreflect.bigop]
r2:1817 [in mathcomp.ssreflect.bigop]
r2:2023 [in mathcomp.ssreflect.bigop]
R2:2810 [in mathcomp.algebra.ssralg]
r2:287 [in mathcomp.fingroup.gproduct]
r2:367 [in mathcomp.algebra.intdiv]
r2:369 [in mathcomp.algebra.intdiv]
r2:371 [in mathcomp.algebra.intdiv]
R2:47 [in mathcomp.field.cyclotomic]
R2:482 [in mathcomp.character.classfun]
R2:486 [in mathcomp.character.classfun]
r2:512 [in mathcomp.ssreflect.div]
r2:514 [in mathcomp.ssreflect.div]
r2:516 [in mathcomp.ssreflect.div]
r2:557 [in mathcomp.ssreflect.bigop]
r2:624 [in mathcomp.ssreflect.bigop]
r2:638 [in mathcomp.ssreflect.bigop]
r2:648 [in mathcomp.ssreflect.bigop]
R3:1664 [in mathcomp.algebra.mxalgebra]
R3:1673 [in mathcomp.algebra.mxalgebra]
R3:1698 [in mathcomp.algebra.mxalgebra]
R3:1705 [in mathcomp.algebra.mxalgebra]
R3:1712 [in mathcomp.algebra.mxalgebra]
R4:1665 [in mathcomp.algebra.mxalgebra]
R4:1674 [in mathcomp.algebra.mxalgebra]
R:1 [in mathcomp.field.fieldext]
R:1 [in mathcomp.field.separable]
R:1 [in mathcomp.algebra.ssrnum]
R:1 [in mathcomp.algebra.vector]
R:1 [in mathcomp.field.falgebra]
R:10 [in mathcomp.algebra.countalg]
R:10 [in mathcomp.algebra.finalg]
R:100 [in mathcomp.algebra.finalg]
R:1002 [in mathcomp.algebra.ssralg]
r:1003 [in mathcomp.algebra.poly]
r:1006 [in mathcomp.algebra.poly]
r:1006 [in mathcomp.ssreflect.bigop]
R:1007 [in mathcomp.algebra.ssralg]
r:1008 [in mathcomp.fingroup.fingroup]
r:1009 [in mathcomp.algebra.polydiv]
R:101 [in mathcomp.algebra.finalg]
r:101 [in mathcomp.algebra.poly]
r:1014 [in mathcomp.algebra.polydiv]
r:1018 [in mathcomp.fingroup.fingroup]
R:102 [in mathcomp.algebra.finalg]
R:1025 [in mathcomp.character.character]
r:1029 [in mathcomp.algebra.polydiv]
r:103 [in mathcomp.algebra.polyXY]
R:103 [in mathcomp.algebra.finalg]
r:103 [in mathcomp.solvable.nilpotent]
r:104 [in mathcomp.algebra.polyXY]
R:104 [in mathcomp.algebra.finalg]
r:1048 [in mathcomp.algebra.vector]
r:105 [in mathcomp.character.inertia]
R:105 [in mathcomp.algebra.finalg]
r:1050 [in mathcomp.algebra.vector]
r:1052 [in mathcomp.ssreflect.finset]
r:1056 [in mathcomp.algebra.ssralg]
R:106 [in mathcomp.solvable.pgroup]
R:106 [in mathcomp.algebra.finalg]
r:1063 [in mathcomp.ssreflect.bigop]
r:1069 [in mathcomp.ssreflect.bigop]
R:107 [in mathcomp.fingroup.morphism]
r:1077 [in mathcomp.ssreflect.bigop]
r:108 [in mathcomp.algebra.polydiv]
R:108 [in mathcomp.ssreflect.eqtype]
r:1089 [in mathcomp.ssreflect.bigop]
R:109 [in mathcomp.fingroup.morphism]
r:109 [in mathcomp.algebra.ssralg]
r:1090 [in mathcomp.ssreflect.finset]
R:11 [in mathcomp.field.cyclotomic]
R:11 [in mathcomp.algebra.matrix]
r:11 [in mathcomp.field.algnum]
R:110 [in mathcomp.ssreflect.finfun]
R:110 [in mathcomp.solvable.pgroup]
R:110 [in mathcomp.algebra.ssrnum]
r:1100 [in mathcomp.ssreflect.finset]
R:1100 [in mathcomp.algebra.ssralg]
r:1103 [in mathcomp.ssreflect.bigop]
R:1107 [in mathcomp.algebra.ssralg]
R:111 [in mathcomp.fingroup.morphism]
R:1112 [in mathcomp.algebra.ssralg]
R:1122 [in mathcomp.algebra.poly]
R:1123 [in mathcomp.algebra.poly]
R:1124 [in mathcomp.algebra.poly]
R:1125 [in mathcomp.algebra.poly]
R:1126 [in mathcomp.algebra.ssralg]
R:1126 [in mathcomp.algebra.poly]
r:1127 [in mathcomp.ssreflect.finset]
R:1127 [in mathcomp.algebra.poly]
R:1128 [in mathcomp.algebra.poly]
R:1129 [in mathcomp.algebra.ssralg]
R:1129 [in mathcomp.algebra.poly]
R:113 [in mathcomp.ssreflect.eqtype]
R:1130 [in mathcomp.algebra.poly]
R:1131 [in mathcomp.algebra.poly]
R:1132 [in mathcomp.algebra.ssralg]
R:1141 [in mathcomp.algebra.ssralg]
r:1144 [in mathcomp.fingroup.fingroup]
r:1147 [in mathcomp.ssreflect.bigop]
r:1149 [in mathcomp.algebra.ssrnum]
R:115 [in mathcomp.solvable.gfunctor]
r:115 [in mathcomp.solvable.nilpotent]
r:1152 [in mathcomp.algebra.ssralg]
r:1155 [in mathcomp.fingroup.fingroup]
R:116 [in mathcomp.algebra.ssrnum]
r:1162 [in mathcomp.algebra.ssralg]
r:1168 [in mathcomp.algebra.poly]
r:1168 [in mathcomp.ssreflect.bigop]
r:1172 [in mathcomp.algebra.poly]
r:118 [in mathcomp.ssreflect.tuple]
R:118 [in mathcomp.algebra.ssrnum]
r:119 [in mathcomp.algebra.ssralg]
r:12 [in mathcomp.ssreflect.div]
r:12 [in mathcomp.field.algnum]
R:12 [in mathcomp.algebra.vector]
r:120 [in mathcomp.ssreflect.tuple]
R:120 [in mathcomp.solvable.sylow]
R:120 [in mathcomp.solvable.gseries]
R:120 [in mathcomp.solvable.gfunctor]
R:121 [in mathcomp.algebra.mxpoly]
R:121 [in mathcomp.algebra.finalg]
R:1210 [in mathcomp.algebra.ssralg]
R:1218 [in mathcomp.algebra.ssralg]
R:122 [in mathcomp.solvable.gseries]
R:122 [in mathcomp.ssreflect.bigop]
R:1223 [in mathcomp.algebra.ssralg]
R:1227 [in mathcomp.algebra.ssralg]
R:123 [in mathcomp.algebra.finalg]
R:1234 [in mathcomp.algebra.ssralg]
r:1237 [in mathcomp.algebra.poly]
r:124 [in mathcomp.field.closed_field]
r:125 [in mathcomp.algebra.interval]
R:125 [in mathcomp.algebra.finalg]
r:1254 [in mathcomp.algebra.ssralg]
R:126 [in mathcomp.ssreflect.bigop]
r:127 [in mathcomp.field.finfield]
R:127 [in mathcomp.algebra.finalg]
r:127 [in mathcomp.solvable.burnside_app]
r:128 [in mathcomp.field.finfield]
r:1281 [in mathcomp.algebra.mxalgebra]
R:129 [in mathcomp.algebra.finalg]
R:1298 [in mathcomp.algebra.ssralg]
R:13 [in mathcomp.algebra.countalg]
R:13 [in mathcomp.algebra.finalg]
r:130 [in mathcomp.algebra.polydiv]
r:130 [in mathcomp.field.finfield]
R:1308 [in mathcomp.algebra.ssralg]
R:131 [in mathcomp.algebra.finalg]
r:131 [in mathcomp.algebra.poly]
R:131 [in mathcomp.ssreflect.bigop]
R:1311 [in mathcomp.algebra.ssralg]
R:1313 [in mathcomp.algebra.ssralg]
r:1317 [in mathcomp.ssreflect.seq]
r:1317 [in mathcomp.ssreflect.bigop]
r:132 [in mathcomp.ssreflect.prime]
r:1327 [in mathcomp.ssreflect.bigop]
R:133 [in mathcomp.algebra.finalg]
r:133 [in mathcomp.solvable.burnside_app]
r:133 [in mathcomp.algebra.ssralg]
r:1338 [in mathcomp.ssreflect.bigop]
r:134 [in mathcomp.algebra.polydiv]
r:134 [in mathcomp.ssreflect.bigop]
r:1349 [in mathcomp.ssreflect.bigop]
R:135 [in mathcomp.algebra.finalg]
r:136 [in mathcomp.algebra.polydiv]
R:136 [in mathcomp.algebra.ring_quotient]
r:1360 [in mathcomp.ssreflect.bigop]
R:137 [in mathcomp.algebra.finalg]
r:138 [in mathcomp.field.closed_field]
R:1381 [in mathcomp.algebra.ssralg]
R:1384 [in mathcomp.algebra.ssralg]
r:139 [in mathcomp.algebra.polydiv]
R:139 [in mathcomp.algebra.ssrint]
R:139 [in mathcomp.algebra.finalg]
R:1393 [in mathcomp.algebra.ssralg]
R:1397 [in mathcomp.algebra.ssralg]
r:14 [in mathcomp.solvable.burnside_app]
R:140 [in mathcomp.algebra.ring_quotient]
R:1402 [in mathcomp.algebra.ssralg]
r:1408 [in mathcomp.algebra.matrix]
R:141 [in mathcomp.algebra.finalg]
R:141 [in mathcomp.fingroup.morphism]
r:1415 [in mathcomp.algebra.matrix]
r:1417 [in mathcomp.algebra.matrix]
r:143 [in mathcomp.algebra.polydiv]
R:143 [in mathcomp.algebra.ssrint]
R:143 [in mathcomp.algebra.finalg]
r:143 [in mathcomp.solvable.nilpotent]
r:1435 [in mathcomp.ssreflect.bigop]
R:144 [in mathcomp.algebra.ring_quotient]
r:1449 [in mathcomp.ssreflect.bigop]
R:145 [in mathcomp.algebra.finalg]
r:145 [in mathcomp.algebra.ssralg]
r:1459 [in mathcomp.ssreflect.bigop]
R:146 [in mathcomp.algebra.ssrint]
R:146 [in mathcomp.algebra.finalg]
R:146 [in mathcomp.fingroup.morphism]
r:147 [in mathcomp.algebra.polydiv]
R:147 [in mathcomp.ssreflect.finfun]
R:147 [in mathcomp.algebra.finalg]
r:148 [in mathcomp.field.closed_field]
R:148 [in mathcomp.algebra.finalg]
r:1485 [in mathcomp.algebra.ssralg]
R:149 [in mathcomp.algebra.ring_quotient]
R:149 [in mathcomp.algebra.finalg]
R:149 [in mathcomp.fingroup.morphism]
r:1490 [in mathcomp.algebra.ssralg]
r:1494 [in mathcomp.algebra.ssralg]
r:15 [in mathcomp.solvable.burnside_app]
R:150 [in mathcomp.algebra.finalg]
R:151 [in mathcomp.algebra.ring_quotient]
R:151 [in mathcomp.algebra.finalg]
r:1512 [in mathcomp.algebra.matrix]
r:1514 [in mathcomp.algebra.ssralg]
r:1515 [in mathcomp.ssreflect.order]
r:1518 [in mathcomp.algebra.ssralg]
r:152 [in mathcomp.ssreflect.generic_quotient]
R:152 [in mathcomp.field.algebraics_fundamentals]
R:152 [in mathcomp.fingroup.morphism]
r:1523 [in mathcomp.ssreflect.order]
r:1526 [in mathcomp.algebra.matrix]
R:153 [in mathcomp.algebra.ring_quotient]
R:153 [in mathcomp.fingroup.morphism]
r:1547 [in mathcomp.ssreflect.order]
r:155 [in mathcomp.field.closed_field]
R:155 [in mathcomp.fingroup.morphism]
r:1556 [in mathcomp.ssreflect.order]
r:156 [in mathcomp.algebra.mxalgebra]
r:158 [in mathcomp.ssreflect.binomial]
R:158 [in mathcomp.algebra.ring_quotient]
R:1581 [in mathcomp.algebra.mxalgebra]
r:1592 [in mathcomp.ssreflect.seq]
R:16 [in mathcomp.algebra.countalg]
R:16 [in mathcomp.algebra.finalg]
r:16 [in mathcomp.solvable.burnside_app]
r:1606 [in mathcomp.ssreflect.order]
r:161 [in mathcomp.ssreflect.generic_quotient]
R:1612 [in mathcomp.algebra.ssralg]
R:1615 [in mathcomp.algebra.ssralg]
R:1618 [in mathcomp.algebra.ssralg]
R:162 [in mathcomp.algebra.ring_quotient]
r:162 [in mathcomp.algebra.ssrnum]
r:162 [in mathcomp.algebra.mxalgebra]
R:1625 [in mathcomp.algebra.mxalgebra]
r:1627 [in mathcomp.ssreflect.order]
R:163 [in mathcomp.fingroup.morphism]
r:1634 [in mathcomp.ssreflect.seq]
r:1634 [in mathcomp.algebra.ssralg]
r:1635 [in mathcomp.ssreflect.order]
r:164 [in mathcomp.field.closed_field]
R:164 [in mathcomp.fingroup.morphism]
r:1644 [in mathcomp.ssreflect.seq]
r:1647 [in mathcomp.ssreflect.seq]
r:1651 [in mathcomp.algebra.ssralg]
r:1652 [in mathcomp.ssreflect.seq]
R:1654 [in mathcomp.algebra.mxalgebra]
r:1659 [in mathcomp.ssreflect.order]
R:166 [in mathcomp.algebra.ring_quotient]
R:166 [in mathcomp.character.inertia]
r:1668 [in mathcomp.ssreflect.bigop]
r:167 [in mathcomp.solvable.sylow]
r:1672 [in mathcomp.ssreflect.bigop]
r:1676 [in mathcomp.ssreflect.order]
r:1678 [in mathcomp.ssreflect.bigop]
R:168 [in mathcomp.algebra.mxpoly]
r:168 [in mathcomp.fingroup.fingroup]
R:1685 [in mathcomp.algebra.ssralg]
R:1687 [in mathcomp.algebra.ssralg]
R:1690 [in mathcomp.algebra.ssralg]
R:1695 [in mathcomp.algebra.ssralg]
R:1696 [in mathcomp.algebra.ssralg]
R:1699 [in mathcomp.algebra.ssralg]
r:1699 [in mathcomp.ssreflect.bigop]
r:17 [in mathcomp.fingroup.presentation]
R:1701 [in mathcomp.algebra.ssralg]
r:1705 [in mathcomp.ssreflect.bigop]
R:1707 [in mathcomp.algebra.ssralg]
R:171 [in mathcomp.algebra.ring_quotient]
r:1713 [in mathcomp.ssreflect.bigop]
r:1718 [in mathcomp.ssreflect.order]
r:1720 [in mathcomp.algebra.matrix]
r:1725 [in mathcomp.algebra.matrix]
r:1727 [in mathcomp.algebra.matrix]
r:1727 [in mathcomp.ssreflect.bigop]
r:1729 [in mathcomp.algebra.matrix]
r:173 [in mathcomp.field.galois]
R:173 [in mathcomp.fingroup.morphism]
r:1732 [in mathcomp.algebra.matrix]
r:1735 [in mathcomp.algebra.matrix]
r:1736 [in mathcomp.algebra.ssralg]
r:1737 [in mathcomp.ssreflect.bigop]
r:1738 [in mathcomp.algebra.matrix]
R:1738 [in mathcomp.algebra.mxalgebra]
r:1741 [in mathcomp.algebra.matrix]
R:1744 [in mathcomp.algebra.mxalgebra]
r:1746 [in mathcomp.algebra.matrix]
r:1746 [in mathcomp.algebra.ssralg]
R:1747 [in mathcomp.algebra.mxalgebra]
r:1748 [in mathcomp.ssreflect.bigop]
R:175 [in mathcomp.algebra.ring_quotient]
r:1750 [in mathcomp.algebra.matrix]
R:1750 [in mathcomp.algebra.mxalgebra]
r:1752 [in mathcomp.algebra.matrix]
r:1755 [in mathcomp.algebra.matrix]
r:1758 [in mathcomp.algebra.matrix]
r:1759 [in mathcomp.ssreflect.bigop]
R:176 [in mathcomp.ssreflect.finfun]
r:176 [in mathcomp.field.closed_field]
r:1760 [in mathcomp.algebra.matrix]
R:1760 [in mathcomp.algebra.mxalgebra]
R:1766 [in mathcomp.algebra.mxalgebra]
r:177 [in mathcomp.algebra.polydiv]
R:177 [in mathcomp.ssreflect.finfun]
r:1770 [in mathcomp.ssreflect.bigop]
R:1771 [in mathcomp.algebra.mxalgebra]
R:1774 [in mathcomp.algebra.mxalgebra]
R:1778 [in mathcomp.algebra.mxalgebra]
r:1779 [in mathcomp.algebra.ssralg]
R:1782 [in mathcomp.algebra.mxalgebra]
R:1787 [in mathcomp.algebra.mxalgebra]
R:1790 [in mathcomp.algebra.mxalgebra]
R:1799 [in mathcomp.algebra.mxalgebra]
r:18 [in mathcomp.ssreflect.div]
r:18 [in mathcomp.algebra.mxpoly]
r:18 [in mathcomp.solvable.burnside_app]
R:180 [in mathcomp.algebra.ring_quotient]
R:181 [in mathcomp.algebra.mxpoly]
r:181 [in mathcomp.field.closed_field]
R:1816 [in mathcomp.algebra.ssralg]
R:182 [in mathcomp.ssreflect.binomial]
R:1820 [in mathcomp.algebra.ssralg]
R:186 [in mathcomp.algebra.ssralg]
r:186 [in mathcomp.character.character]
R:187 [in mathcomp.algebra.mxpoly]
r:188 [in mathcomp.ssreflect.prime]
R:1889 [in mathcomp.algebra.ssralg]
R:19 [in mathcomp.algebra.countalg]
R:19 [in mathcomp.algebra.finalg]
R:19 [in mathcomp.algebra.ssrnum]
r:19 [in mathcomp.solvable.burnside_app]
R:1905 [in mathcomp.algebra.ssralg]
r:191 [in mathcomp.field.fieldext]
R:1917 [in mathcomp.algebra.ssralg]
r:1919 [in mathcomp.ssreflect.order]
R:192 [in mathcomp.algebra.mxpoly]
R:192 [in mathcomp.solvable.cyclic]
R:1924 [in mathcomp.algebra.ssralg]
r:1929 [in mathcomp.ssreflect.order]
r:193 [in mathcomp.field.fieldext]
R:194 [in mathcomp.fingroup.morphism]
R:1942 [in mathcomp.algebra.matrix]
R:1945 [in mathcomp.algebra.ssralg]
R:195 [in mathcomp.fingroup.morphism]
R:1950 [in mathcomp.algebra.ssralg]
R:1951 [in mathcomp.algebra.matrix]
R:1955 [in mathcomp.algebra.ssralg]
R:1956 [in mathcomp.algebra.matrix]
R:1959 [in mathcomp.algebra.matrix]
R:196 [in mathcomp.algebra.ssralg]
R:197 [in mathcomp.fingroup.morphism]
R:1977 [in mathcomp.algebra.ssralg]
r:1978 [in mathcomp.algebra.matrix]
r:198 [in mathcomp.character.classfun]
R:1982 [in mathcomp.algebra.ssralg]
r:1985 [in mathcomp.ssreflect.bigop]
r:1986 [in mathcomp.ssreflect.bigop]
r:1987 [in mathcomp.algebra.matrix]
R:1987 [in mathcomp.algebra.ssralg]
r:1987 [in mathcomp.ssreflect.bigop]
R:199 [in mathcomp.fingroup.morphism]
R:1992 [in mathcomp.algebra.ssralg]
r:1994 [in mathcomp.ssreflect.bigop]
R:1997 [in mathcomp.algebra.ssralg]
r:2 [in mathcomp.ssreflect.prime]
R:2002 [in mathcomp.algebra.ssralg]
R:2003 [in mathcomp.algebra.matrix]
R:2007 [in mathcomp.algebra.ssralg]
R:2009 [in mathcomp.ssreflect.seq]
r:2011 [in mathcomp.ssreflect.bigop]
R:2012 [in mathcomp.algebra.ssralg]
R:2017 [in mathcomp.algebra.ssralg]
R:202 [in mathcomp.algebra.mxpoly]
r:202 [in mathcomp.algebra.ssrint]
r:202 [in mathcomp.solvable.nilpotent]
R:2022 [in mathcomp.algebra.ssralg]
r:2033 [in mathcomp.ssreflect.bigop]
R:2034 [in mathcomp.ssreflect.seq]
R:2036 [in mathcomp.algebra.ssralg]
r:204 [in mathcomp.field.separable]
R:2041 [in mathcomp.algebra.ssralg]
r:2043 [in mathcomp.ssreflect.bigop]
R:2045 [in mathcomp.algebra.ssralg]
R:2047 [in mathcomp.algebra.matrix]
R:205 [in mathcomp.fingroup.morphism]
R:2050 [in mathcomp.algebra.ssralg]
R:2054 [in mathcomp.algebra.ssralg]
r:2057 [in mathcomp.ssreflect.bigop]
R:2059 [in mathcomp.algebra.ssralg]
R:206 [in mathcomp.algebra.mxpoly]
R:2063 [in mathcomp.algebra.ssralg]
R:2068 [in mathcomp.algebra.ssralg]
R:207 [in mathcomp.fingroup.morphism]
R:2072 [in mathcomp.algebra.ssralg]
R:2077 [in mathcomp.algebra.ssralg]
R:2081 [in mathcomp.algebra.ssralg]
R:2088 [in mathcomp.algebra.ssralg]
R:2094 [in mathcomp.algebra.ssralg]
R:21 [in mathcomp.algebra.mxpoly]
R:210 [in mathcomp.algebra.mxpoly]
R:2101 [in mathcomp.algebra.ssralg]
R:2107 [in mathcomp.algebra.ssralg]
R:211 [in mathcomp.fingroup.morphism]
R:2112 [in mathcomp.algebra.ssralg]
R:2116 [in mathcomp.algebra.ssralg]
R:212 [in mathcomp.fingroup.morphism]
R:2123 [in mathcomp.algebra.ssralg]
r:213 [in mathcomp.algebra.ssrint]
R:213 [in mathcomp.algebra.ssralg]
r:2134 [in mathcomp.algebra.ssralg]
r:214 [in mathcomp.solvable.nilpotent]
R:2148 [in mathcomp.ssreflect.seq]
R:215 [in mathcomp.algebra.ssralg]
R:215 [in mathcomp.solvable.maximal]
r:216 [in mathcomp.field.separable]
r:216 [in mathcomp.character.mxrepresentation]
r:216 [in mathcomp.algebra.vector]
r:2169 [in mathcomp.algebra.ssralg]
R:217 [in mathcomp.solvable.maximal]
R:218 [in mathcomp.algebra.ssralg]
R:22 [in mathcomp.algebra.countalg]
R:22 [in mathcomp.algebra.finalg]
r:22 [in mathcomp.fingroup.presentation]
R:22 [in mathcomp.field.falgebra]
R:221 [in mathcomp.algebra.ssralg]
R:224 [in mathcomp.fingroup.morphism]
R:224 [in mathcomp.algebra.ssralg]
r:2249 [in mathcomp.ssreflect.seq]
r:2257 [in mathcomp.ssreflect.seq]
r:226 [in mathcomp.algebra.polydiv]
R:226 [in mathcomp.algebra.ssralg]
r:2267 [in mathcomp.ssreflect.seq]
R:2270 [in mathcomp.algebra.matrix]
r:2273 [in mathcomp.ssreflect.seq]
r:2277 [in mathcomp.ssreflect.seq]
R:2277 [in mathcomp.algebra.ssralg]
r:228 [in mathcomp.algebra.polydiv]
r:228 [in mathcomp.character.mxrepresentation]
r:228 [in mathcomp.fingroup.gproduct]
r:2283 [in mathcomp.ssreflect.bigop]
R:2284 [in mathcomp.algebra.ssralg]
r:2285 [in mathcomp.ssreflect.seq]
R:2289 [in mathcomp.algebra.ssralg]
r:2293 [in mathcomp.ssreflect.seq]
R:2296 [in mathcomp.algebra.ssralg]
r:2296 [in mathcomp.ssreflect.bigop]
r:2300 [in mathcomp.ssreflect.seq]
R:2303 [in mathcomp.algebra.matrix]
R:2303 [in mathcomp.algebra.ssralg]
R:2308 [in mathcomp.algebra.matrix]
r:231 [in mathcomp.field.galois]
r:2311 [in mathcomp.ssreflect.seq]
R:2313 [in mathcomp.algebra.matrix]
R:2313 [in mathcomp.algebra.ssralg]
r:2313 [in mathcomp.ssreflect.bigop]
R:2316 [in mathcomp.algebra.matrix]
R:2318 [in mathcomp.algebra.ssralg]
R:232 [in mathcomp.character.classfun]
R:2323 [in mathcomp.algebra.matrix]
R:2324 [in mathcomp.algebra.ssralg]
r:233 [in mathcomp.algebra.polydiv]
R:2330 [in mathcomp.algebra.ssralg]
r:2331 [in mathcomp.ssreflect.bigop]
R:2339 [in mathcomp.algebra.ssralg]
r:2342 [in mathcomp.ssreflect.bigop]
R:2345 [in mathcomp.algebra.ssralg]
R:2349 [in mathcomp.algebra.ssralg]
r:235 [in mathcomp.field.fieldext]
r:2351 [in mathcomp.ssreflect.seq]
r:2355 [in mathcomp.ssreflect.seq]
R:2358 [in mathcomp.algebra.ssralg]
R:236 [in mathcomp.solvable.maximal]
r:2360 [in mathcomp.ssreflect.seq]
R:2362 [in mathcomp.algebra.ssrnum]
r:2364 [in mathcomp.ssreflect.seq]
r:2369 [in mathcomp.ssreflect.seq]
r:237 [in mathcomp.algebra.mxpoly]
R:2370 [in mathcomp.algebra.ssralg]
r:2372 [in mathcomp.ssreflect.seq]
R:2379 [in mathcomp.algebra.ssralg]
r:238 [in mathcomp.algebra.mxpoly]
R:238 [in mathcomp.algebra.ssrnum]
R:2387 [in mathcomp.algebra.ssralg]
R:2389 [in mathcomp.algebra.ssrnum]
r:239 [in mathcomp.algebra.mxpoly]
r:239 [in mathcomp.fingroup.gproduct]
R:2398 [in mathcomp.algebra.ssralg]
R:24 [in mathcomp.algebra.ssrnum]
R:240 [in mathcomp.solvable.maximal]
R:2405 [in mathcomp.algebra.ssrnum]
R:2407 [in mathcomp.algebra.ssralg]
R:2408 [in mathcomp.algebra.ssrnum]
R:2410 [in mathcomp.algebra.ssrnum]
R:2415 [in mathcomp.algebra.ssralg]
R:242 [in mathcomp.algebra.ssralg]
R:2426 [in mathcomp.algebra.ssralg]
R:2431 [in mathcomp.algebra.ssralg]
R:2435 [in mathcomp.algebra.ssrnum]
R:2437 [in mathcomp.algebra.matrix]
R:2438 [in mathcomp.algebra.ssralg]
R:244 [in mathcomp.algebra.ssralg]
R:2448 [in mathcomp.algebra.ssralg]
R:2450 [in mathcomp.algebra.ssrnum]
R:2453 [in mathcomp.algebra.ssralg]
r:2456 [in mathcomp.algebra.matrix]
R:2458 [in mathcomp.algebra.ssralg]
R:2459 [in mathcomp.algebra.matrix]
R:2464 [in mathcomp.algebra.ssralg]
R:2475 [in mathcomp.algebra.ssrnum]
R:2490 [in mathcomp.algebra.ssralg]
R:2497 [in mathcomp.algebra.ssralg]
R:25 [in mathcomp.algebra.countalg]
R:25 [in mathcomp.algebra.vector]
R:2503 [in mathcomp.algebra.ssralg]
R:2503 [in mathcomp.ssreflect.bigop]
R:2510 [in mathcomp.algebra.ssralg]
R:2516 [in mathcomp.algebra.ssralg]
R:2525 [in mathcomp.algebra.ssralg]
R:2533 [in mathcomp.algebra.ssralg]
r:2539 [in mathcomp.ssreflect.bigop]
R:2542 [in mathcomp.algebra.ssralg]
r:2545 [in mathcomp.ssreflect.bigop]
r:255 [in mathcomp.algebra.ssralg]
R:2550 [in mathcomp.algebra.ssralg]
R:2559 [in mathcomp.algebra.ssralg]
R:2567 [in mathcomp.algebra.ssralg]
R:2574 [in mathcomp.algebra.ssralg]
R:2580 [in mathcomp.algebra.ssralg]
R:2587 [in mathcomp.algebra.ssralg]
R:2593 [in mathcomp.algebra.ssralg]
r:2594 [in mathcomp.ssreflect.bigop]
R:26 [in mathcomp.algebra.zmodp]
R:2600 [in mathcomp.algebra.ssralg]
R:2606 [in mathcomp.algebra.ssralg]
R:2608 [in mathcomp.algebra.ssralg]
R:2610 [in mathcomp.algebra.ssralg]
R:2612 [in mathcomp.algebra.ssralg]
r:2619 [in mathcomp.ssreflect.bigop]
R:262 [in mathcomp.fingroup.quotient]
r:263 [in mathcomp.field.closed_field]
r:2631 [in mathcomp.ssreflect.bigop]
r:2655 [in mathcomp.ssreflect.bigop]
r:266 [in mathcomp.algebra.ssralg]
r:2667 [in mathcomp.ssreflect.bigop]
r:2675 [in mathcomp.ssreflect.bigop]
r:2683 [in mathcomp.ssreflect.bigop]
R:27 [in mathcomp.algebra.finalg]
r:27 [in mathcomp.fingroup.presentation]
R:271 [in mathcomp.algebra.interval]
r:2712 [in mathcomp.ssreflect.bigop]
r:2729 [in mathcomp.ssreflect.bigop]
r:274 [in mathcomp.fingroup.gproduct]
R:277 [in mathcomp.fingroup.morphism]
r:2772 [in mathcomp.ssreflect.bigop]
R:28 [in mathcomp.algebra.countalg]
r:280 [in mathcomp.solvable.extremal]
R:280 [in mathcomp.fingroup.morphism]
R:2811 [in mathcomp.algebra.ssralg]
R:284 [in mathcomp.fingroup.morphism]
R:2844 [in mathcomp.algebra.matrix]
r:287 [in mathcomp.character.classfun]
R:29 [in mathcomp.algebra.countalg]
r:29 [in mathcomp.field.separable]
R:2931 [in mathcomp.algebra.matrix]
R:295 [in mathcomp.ssreflect.bigop]
r:298 [in mathcomp.algebra.ssrint]
r:301 [in mathcomp.ssreflect.bigop]
r:302 [in mathcomp.algebra.poly]
R:3033 [in mathcomp.algebra.matrix]
r:304 [in mathcomp.character.classfun]
r:308 [in mathcomp.algebra.ssrint]
R:3090 [in mathcomp.algebra.matrix]
r:3093 [in mathcomp.algebra.matrix]
r:315 [in mathcomp.solvable.abelian]
r:316 [in mathcomp.algebra.mxalgebra]
r:319 [in mathcomp.field.fieldext]
R:32 [in mathcomp.algebra.finalg]
R:3246 [in mathcomp.algebra.matrix]
r:325 [in mathcomp.ssreflect.bigop]
r:328 [in mathcomp.algebra.ssrnum]
R:3280 [in mathcomp.algebra.matrix]
R:3291 [in mathcomp.algebra.matrix]
R:33 [in mathcomp.algebra.zmodp]
R:3306 [in mathcomp.algebra.matrix]
r:337 [in mathcomp.algebra.ssrnum]
R:34 [in mathcomp.fingroup.morphism]
R:340 [in mathcomp.solvable.extremal]
r:343 [in mathcomp.character.character]
r:350 [in mathcomp.ssreflect.tuple]
r:352 [in mathcomp.ssreflect.tuple]
r:352 [in mathcomp.ssreflect.bigop]
r:354 [in mathcomp.algebra.polydiv]
r:357 [in mathcomp.algebra.polydiv]
r:36 [in mathcomp.algebra.vector]
r:365 [in mathcomp.fingroup.gproduct]
R:37 [in mathcomp.field.separable]
R:37 [in mathcomp.algebra.polyXY]
R:37 [in mathcomp.algebra.finalg]
r:37 [in mathcomp.algebra.vector]
r:376 [in mathcomp.fingroup.gproduct]
R:377 [in mathcomp.algebra.mxpoly]
r:378 [in mathcomp.algebra.poly]
r:378 [in mathcomp.ssreflect.bigop]
r:381 [in mathcomp.algebra.vector]
r:382 [in mathcomp.character.classfun]
R:383 [in mathcomp.algebra.mxpoly]
r:387 [in mathcomp.fingroup.gproduct]
R:393 [in mathcomp.fingroup.morphism]
r:395 [in mathcomp.character.character]
R:396 [in mathcomp.fingroup.morphism]
r:398 [in mathcomp.ssreflect.bigop]
R:4 [in mathcomp.algebra.countalg]
R:4 [in mathcomp.algebra.finalg]
R:4 [in mathcomp.algebra.ssrnum]
R:40 [in mathcomp.algebra.ssrnum]
R:405 [in mathcomp.field.closed_field]
R:409 [in mathcomp.field.closed_field]
r:41 [in mathcomp.fingroup.morphism]
r:412 [in mathcomp.algebra.mxpoly]
r:414 [in mathcomp.algebra.intdiv]
r:414 [in mathcomp.field.galois]
r:415 [in mathcomp.character.classfun]
r:417 [in mathcomp.ssreflect.bigop]
R:42 [in mathcomp.algebra.matrix]
R:42 [in mathcomp.algebra.finalg]
r:426 [in mathcomp.fingroup.gproduct]
R:43 [in mathcomp.algebra.finalg]
R:43 [in mathcomp.algebra.ssrnum]
r:431 [in mathcomp.algebra.intdiv]
r:432 [in mathcomp.algebra.poly]
r:433 [in mathcomp.algebra.polydiv]
r:434 [in mathcomp.ssreflect.bigop]
r:436 [in mathcomp.algebra.polydiv]
R:437 [in mathcomp.algebra.intdiv]
r:437 [in mathcomp.fingroup.gproduct]
R:438 [in mathcomp.algebra.intdiv]
r:439 [in mathcomp.algebra.polydiv]
R:44 [in mathcomp.algebra.finalg]
r:443 [in mathcomp.algebra.mxpoly]
r:443 [in mathcomp.algebra.ssralg]
r:444 [in mathcomp.algebra.polydiv]
r:444 [in mathcomp.algebra.mxpoly]
r:446 [in mathcomp.field.galois]
r:447 [in mathcomp.field.galois]
r:447 [in mathcomp.ssreflect.bigop]
R:45 [in mathcomp.algebra.matrix]
r:45 [in mathcomp.algebra.rat]
R:452 [in mathcomp.algebra.mxpoly]
R:457 [in mathcomp.algebra.mxpoly]
r:459 [in mathcomp.ssreflect.bigop]
R:462 [in mathcomp.fingroup.action]
r:462 [in mathcomp.fingroup.fingroup]
r:463 [in mathcomp.field.galois]
R:464 [in mathcomp.algebra.mxpoly]
R:465 [in mathcomp.fingroup.action]
r:466 [in mathcomp.algebra.mxpoly]
R:467 [in mathcomp.character.classfun]
r:468 [in mathcomp.field.galois]
R:47 [in mathcomp.algebra.mxpoly]
R:472 [in mathcomp.character.classfun]
R:472 [in mathcomp.character.character]
r:476 [in mathcomp.fingroup.fingroup]
r:477 [in mathcomp.ssreflect.bigop]
R:48 [in mathcomp.algebra.matrix]
R:483 [in mathcomp.algebra.ssrint]
R:488 [in mathcomp.character.classfun]
r:49 [in mathcomp.field.cyclotomic]
r:490 [in mathcomp.ssreflect.bigop]
r:492 [in mathcomp.field.galois]
r:493 [in mathcomp.field.galois]
r:494 [in mathcomp.algebra.ssralg]
r:494 [in mathcomp.ssreflect.bigop]
r:5 [in mathcomp.ssreflect.choice]
r:5 [in mathcomp.character.mxrepresentation]
r:501 [in mathcomp.character.mxrepresentation]
r:501 [in mathcomp.fingroup.gproduct]
r:503 [in mathcomp.ssreflect.bigop]
r:506 [in mathcomp.algebra.polydiv]
R:507 [in mathcomp.character.classfun]
R:51 [in mathcomp.algebra.matrix]
R:51 [in mathcomp.algebra.fraction]
R:510 [in mathcomp.character.classfun]
R:512 [in mathcomp.character.classfun]
r:512 [in mathcomp.fingroup.gproduct]
r:513 [in mathcomp.ssreflect.bigop]
R:516 [in mathcomp.character.classfun]
r:517 [in mathcomp.field.galois]
R:518 [in mathcomp.character.classfun]
r:52 [in mathcomp.field.separable]
r:523 [in mathcomp.ssreflect.bigop]
r:526 [in mathcomp.algebra.ssrnum]
R:529 [in mathcomp.character.classfun]
r:53 [in mathcomp.field.separable]
R:531 [in mathcomp.character.classfun]
r:533 [in mathcomp.ssreflect.bigop]
r:534 [in mathcomp.algebra.ssrnum]
r:537 [in mathcomp.algebra.mxpoly]
r:538 [in mathcomp.algebra.polydiv]
r:539 [in mathcomp.algebra.polydiv]
R:54 [in mathcomp.algebra.finalg]
R:541 [in mathcomp.ssreflect.finset]
r:544 [in mathcomp.ssreflect.bigop]
R:55 [in mathcomp.field.finfield]
R:55 [in mathcomp.algebra.finalg]
r:550 [in mathcomp.algebra.mxpoly]
r:550 [in mathcomp.character.character]
r:555 [in mathcomp.algebra.mxpoly]
r:556 [in mathcomp.character.character]
r:557 [in mathcomp.algebra.ssrnum]
r:56 [in mathcomp.field.separable]
R:56 [in mathcomp.algebra.finalg]
r:566 [in mathcomp.ssreflect.prime]
R:57 [in mathcomp.field.finfield]
R:57 [in mathcomp.algebra.finalg]
r:572 [in mathcomp.algebra.mxpoly]
r:573 [in mathcomp.algebra.mxpoly]
r:574 [in mathcomp.algebra.mxpoly]
r:574 [in mathcomp.algebra.ssrnum]
r:575 [in mathcomp.ssreflect.bigop]
R:584 [in mathcomp.algebra.ssrint]
r:585 [in mathcomp.algebra.polydiv]
r:587 [in mathcomp.ssreflect.bigop]
r:588 [in mathcomp.algebra.polydiv]
R:59 [in mathcomp.field.finfield]
R:59 [in mathcomp.algebra.finalg]
r:597 [in mathcomp.algebra.polydiv]
r:597 [in mathcomp.ssreflect.bigop]
R:6 [in mathcomp.algebra.vector]
r:600 [in mathcomp.algebra.polydiv]
R:601 [in mathcomp.algebra.ssralg]
R:602 [in mathcomp.solvable.pgroup]
r:606 [in mathcomp.ssreflect.bigop]
R:61 [in mathcomp.field.finfield]
r:612 [in mathcomp.ssreflect.bigop]
r:617 [in mathcomp.ssreflect.bigop]
R:618 [in mathcomp.algebra.ssralg]
r:62 [in mathcomp.field.cyclotomic]
r:624 [in mathcomp.fingroup.fingroup]
r:63 [in mathcomp.field.cyclotomic]
R:63 [in mathcomp.field.finfield]
r:64 [in mathcomp.field.cyclotomic]
r:646 [in mathcomp.algebra.polydiv]
r:649 [in mathcomp.algebra.polydiv]
R:65 [in mathcomp.field.cyclotomic]
r:654 [in mathcomp.algebra.ssralg]
r:659 [in mathcomp.ssreflect.bigop]
R:66 [in mathcomp.algebra.ssrnum]
R:66 [in mathcomp.fingroup.morphism]
r:665 [in mathcomp.algebra.ssralg]
r:667 [in mathcomp.algebra.polydiv]
r:668 [in mathcomp.ssreflect.bigop]
r:669 [in mathcomp.algebra.polydiv]
r:673 [in mathcomp.algebra.polydiv]
r:676 [in mathcomp.algebra.polydiv]
R:677 [in mathcomp.solvable.abelian]
r:678 [in mathcomp.ssreflect.bigop]
R:680 [in mathcomp.algebra.ssralg]
R:682 [in mathcomp.solvable.abelian]
r:687 [in mathcomp.ssreflect.bigop]
R:688 [in mathcomp.algebra.ssralg]
R:69 [in mathcomp.algebra.ssrnum]
R:69 [in mathcomp.fingroup.morphism]
r:69 [in mathcomp.solvable.center]
R:693 [in mathcomp.algebra.ssralg]
r:699 [in mathcomp.algebra.vector]
r:7 [in mathcomp.algebra.polydiv]
R:7 [in mathcomp.algebra.countalg]
R:7 [in mathcomp.algebra.finalg]
R:70 [in mathcomp.field.finfield]
R:70 [in mathcomp.algebra.finalg]
R:70 [in mathcomp.fingroup.morphism]
R:701 [in mathcomp.ssreflect.finset]
r:71 [in mathcomp.character.mxabelem]
R:71 [in mathcomp.algebra.finalg]
r:712 [in mathcomp.algebra.polydiv]
R:718 [in mathcomp.character.classfun]
R:72 [in mathcomp.field.finfield]
R:72 [in mathcomp.algebra.finalg]
R:73 [in mathcomp.algebra.finalg]
r:730 [in mathcomp.algebra.polydiv]
r:733 [in mathcomp.algebra.polydiv]
r:736 [in mathcomp.algebra.polydiv]
r:736 [in mathcomp.algebra.matrix]
R:74 [in mathcomp.field.finfield]
R:74 [in mathcomp.algebra.finalg]
R:74 [in mathcomp.fingroup.morphism]
r:741 [in mathcomp.algebra.polydiv]
R:75 [in mathcomp.ssreflect.ssrAC]
R:75 [in mathcomp.algebra.finalg]
r:750 [in mathcomp.algebra.matrix]
R:758 [in mathcomp.algebra.ssrint]
r:76 [in mathcomp.character.classfun]
R:76 [in mathcomp.field.finfield]
R:76 [in mathcomp.algebra.ssrnum]
r:760 [in mathcomp.algebra.polydiv]
r:761 [in mathcomp.algebra.matrix]
R:762 [in mathcomp.algebra.ssrint]
r:771 [in mathcomp.algebra.matrix]
r:779 [in mathcomp.algebra.mxpoly]
R:78 [in mathcomp.field.finfield]
r:780 [in mathcomp.algebra.mxpoly]
r:781 [in mathcomp.algebra.mxpoly]
r:788 [in mathcomp.algebra.ssralg]
R:79 [in mathcomp.algebra.ssrnum]
r:79 [in mathcomp.solvable.nilpotent]
r:792 [in mathcomp.algebra.vector]
r:796 [in mathcomp.algebra.polydiv]
r:799 [in mathcomp.algebra.polydiv]
r:8 [in mathcomp.ssreflect.prime]
r:8 [in mathcomp.solvable.gseries]
R:80 [in mathcomp.ssreflect.ssrAC]
R:80 [in mathcomp.field.finfield]
R:80 [in mathcomp.fingroup.morphism]
r:802 [in mathcomp.algebra.polydiv]
r:806 [in mathcomp.algebra.vector]
r:811 [in mathcomp.algebra.poly]
r:814 [in mathcomp.algebra.ssrnum]
r:814 [in mathcomp.algebra.poly]
R:82 [in mathcomp.algebra.ssrnum]
R:82 [in mathcomp.fingroup.morphism]
r:822 [in mathcomp.algebra.ssrnum]
r:827 [in mathcomp.algebra.polydiv]
R:827 [in mathcomp.algebra.ssralg]
r:829 [in mathcomp.algebra.polydiv]
r:830 [in mathcomp.algebra.ssrnum]
r:831 [in mathcomp.algebra.polydiv]
R:834 [in mathcomp.algebra.ssralg]
R:84 [in mathcomp.fingroup.morphism]
r:84 [in mathcomp.solvable.center]
r:840 [in mathcomp.algebra.mxpoly]
r:841 [in mathcomp.algebra.mxpoly]
R:841 [in mathcomp.algebra.ssralg]
r:842 [in mathcomp.algebra.mxpoly]
r:843 [in mathcomp.algebra.ssrnum]
r:844 [in mathcomp.algebra.mxpoly]
r:845 [in mathcomp.algebra.mxpoly]
r:846 [in mathcomp.algebra.mxpoly]
R:846 [in mathcomp.algebra.ssralg]
r:848 [in mathcomp.algebra.mxalgebra]
R:849 [in mathcomp.algebra.ssralg]
R:85 [in mathcomp.algebra.ssrnum]
r:850 [in mathcomp.algebra.mxalgebra]
R:856 [in mathcomp.algebra.ssrint]
r:859 [in mathcomp.algebra.polydiv]
R:859 [in mathcomp.algebra.ssrint]
R:861 [in mathcomp.algebra.matrix]
R:864 [in mathcomp.algebra.ssrint]
R:866 [in mathcomp.character.classfun]
R:868 [in mathcomp.algebra.ssrint]
r:868 [in mathcomp.ssreflect.bigop]
R:87 [in mathcomp.solvable.pgroup]
R:87 [in mathcomp.solvable.hall]
r:873 [in mathcomp.algebra.ssralg]
r:874 [in mathcomp.algebra.polydiv]
r:878 [in mathcomp.algebra.polydiv]
r:88 [in mathcomp.character.inertia]
R:88 [in mathcomp.algebra.ssrnum]
R:88 [in mathcomp.fingroup.morphism]
r:880 [in mathcomp.ssreflect.bigop]
r:882 [in mathcomp.algebra.polydiv]
R:882 [in mathcomp.ssreflect.finset]
r:888 [in mathcomp.ssreflect.ssrnat]
r:89 [in mathcomp.algebra.polydiv]
r:890 [in mathcomp.algebra.ssralg]
r:891 [in mathcomp.ssreflect.bigop]
r:898 [in mathcomp.algebra.matrix]
r:900 [in mathcomp.algebra.poly]
r:901 [in mathcomp.ssreflect.ssrnat]
R:91 [in mathcomp.algebra.ssrnum]
r:91 [in mathcomp.solvable.nilpotent]
r:912 [in mathcomp.ssreflect.ssrnat]
R:917 [in mathcomp.algebra.ssralg]
R:924 [in mathcomp.ssreflect.seq]
r:926 [in mathcomp.ssreflect.ssrnat]
R:926 [in mathcomp.algebra.ssralg]
r:929 [in mathcomp.algebra.polydiv]
R:93 [in mathcomp.fingroup.morphism]
r:932 [in mathcomp.algebra.polydiv]
R:937 [in mathcomp.algebra.ssralg]
R:938 [in mathcomp.algebra.ssralg]
R:94 [in mathcomp.algebra.ssrnum]
R:940 [in mathcomp.algebra.ssralg]
r:944 [in mathcomp.algebra.poly]
R:946 [in mathcomp.algebra.ssralg]
r:949 [in mathcomp.algebra.polydiv]
R:950 [in mathcomp.algebra.ssralg]
r:952 [in mathcomp.algebra.polydiv]
r:955 [in mathcomp.algebra.polydiv]
R:958 [in mathcomp.algebra.ssralg]
r:959 [in mathcomp.algebra.vector]
R:969 [in mathcomp.algebra.ssralg]
R:97 [in mathcomp.fingroup.morphism]
R:976 [in mathcomp.algebra.ssralg]
r:978 [in mathcomp.algebra.poly]
R:98 [in mathcomp.algebra.finalg]
R:986 [in mathcomp.algebra.ssralg]
R:986 [in mathcomp.ssreflect.bigop]
r:987 [in mathcomp.algebra.polydiv]
R:99 [in mathcomp.algebra.finalg]
R:997 [in mathcomp.algebra.ssralg]

Global Index

_

(71649 entries)

Notation Index

H

J

T

W

X

Y

_

(1792 entries)

Binder Index

_

other

(46193 entries)

Module Index

H

J

K

L

W

X

Y

_

other

(266 entries)

Variable Index

J

W

X

Y

_

other

(3623 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(14204 entries)

Constructor Index

J

K

W

Y

_

other

(259 entries)

Axiom Index

B

C

D

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(8 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(134 entries)

Projection Index

H

I

J

K

L

N

O

Q

U

W

X

Y

Z

_

other

(44 entries)

Section Index

J

W

X

Y

_

other

(1276 entries)

Abbreviation Index

Y

_

other

(682 entries)

Definition Index

Y

_

other

(3041 entries)

Record Index

F

H

I

J

K

L

O

Q

U

W

X

Y

Z

_

other

(36 entries)