| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74637 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1852 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48381 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (277 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3804 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (91 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14415 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (132 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1342 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1003 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3033 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
R (binder)
real:2406 [in mathcomp.algebra.ssrnum]recf:552 [in mathcomp.algebra.mxpoly]
redg:1697 [in mathcomp.algebra.ssralg]
repr_ofK_subproof:5 [in mathcomp.ssreflect.generic_quotient]
repr_of:3 [in mathcomp.ssreflect.generic_quotient]
rfG:658 [in mathcomp.character.character]
rGf:1423 [in mathcomp.character.mxrepresentation]
rG0:156 [in mathcomp.character.mxrepresentation]
rG1:109 [in mathcomp.character.character]
rG1:112 [in mathcomp.character.character]
rG1:1264 [in mathcomp.character.mxrepresentation]
rG1:1419 [in mathcomp.character.mxrepresentation]
rG1:168 [in mathcomp.character.character]
rG1:183 [in mathcomp.character.character]
rG1:185 [in mathcomp.character.character]
rG1:312 [in mathcomp.character.character]
rG1:318 [in mathcomp.character.character]
rG1:367 [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:1265 [in mathcomp.character.mxrepresentation]
rG2:1420 [in mathcomp.character.mxrepresentation]
rG2:169 [in mathcomp.character.character]
rG2:184 [in mathcomp.character.character]
rG2:186 [in mathcomp.character.character]
rG2:313 [in mathcomp.character.character]
rG2:319 [in mathcomp.character.character]
rG2:368 [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:1003 [in mathcomp.character.character]
rG:1044 [in mathcomp.character.character]
rG:1422 [in mathcomp.character.mxrepresentation]
rG:1442 [in mathcomp.character.mxrepresentation]
rG:175 [in mathcomp.character.character]
rG:178 [in mathcomp.character.character]
rG:180 [in mathcomp.character.character]
rG:190 [in mathcomp.character.character]
rG:197 [in mathcomp.character.character]
rG:215 [in mathcomp.character.mxabelem]
rG:239 [in mathcomp.character.character]
rG:306 [in mathcomp.character.character]
rG:321 [in mathcomp.character.character]
rG:322 [in mathcomp.character.character]
rG:354 [in mathcomp.character.character]
rG:364 [in mathcomp.character.character]
rG:373 [in mathcomp.character.character]
rG:428 [in mathcomp.character.character]
rG:566 [in mathcomp.character.character]
rG:572 [in mathcomp.character.character]
rG:604 [in mathcomp.character.character]
rG:630 [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:463 [in mathcomp.ssreflect.prime]
rho:466 [in mathcomp.ssreflect.prime]
rho:469 [in mathcomp.ssreflect.prime]
rho:474 [in mathcomp.ssreflect.prime]
rho:519 [in mathcomp.ssreflect.prime]
rho:549 [in mathcomp.ssreflect.prime]
rho:552 [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:581 [in mathcomp.algebra.poly]
ringS:619 [in mathcomp.algebra.poly]
ringS:662 [in mathcomp.algebra.poly]
ringS:803 [in mathcomp.algebra.poly]
rI:1619 [in mathcomp.ssreflect.bigop]
rI:1642 [in mathcomp.ssreflect.bigop]
rI:2255 [in mathcomp.ssreflect.bigop]
rI:2277 [in mathcomp.ssreflect.bigop]
rI:2585 [in mathcomp.ssreflect.bigop]
rI:344 [in mathcomp.algebra.poly]
rI:353 [in mathcomp.algebra.poly]
rI:360 [in mathcomp.algebra.poly]
rJ:1620 [in mathcomp.ssreflect.bigop]
rJ:1643 [in mathcomp.ssreflect.bigop]
rJ:2256 [in mathcomp.ssreflect.bigop]
rJ:2278 [in mathcomp.ssreflect.bigop]
rJ:2586 [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:947 [in mathcomp.algebra.ssralg]
rngS:2341 [in mathcomp.algebra.ssralg]
rngS:2349 [in mathcomp.algebra.ssralg]
row1:718 [in mathcomp.algebra.matrix]
row3:720 [in mathcomp.algebra.matrix]
rpredM:2088 [in mathcomp.algebra.ssralg]
rpredNr:2083 [in mathcomp.algebra.ssralg]
rpredVr:2098 [in mathcomp.algebra.ssralg]
rpredZ:2104 [in mathcomp.algebra.ssralg]
rpred0D:2078 [in mathcomp.algebra.ssralg]
rpred1M:2194 [in mathcomp.algebra.ssralg]
rpred1:2093 [in mathcomp.algebra.ssralg]
rP:12 [in mathcomp.ssreflect.ssrbool]
rP:94 [in mathcomp.ssreflect.ssrbool]
rqT:81 [in mathcomp.algebra.ring_quotient]
rqT:82 [in mathcomp.algebra.ring_quotient]
rr:2020 [in mathcomp.ssreflect.bigop]
rr:208 [in mathcomp.field.closed_field]
rr:214 [in mathcomp.field.closed_field]
rR:255 [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:65 [in mathcomp.field.algnum]
rr:68 [in mathcomp.algebra.polydiv]
rr:77 [in mathcomp.algebra.polydiv]
rR:841 [in mathcomp.algebra.poly]
rs1:289 [in mathcomp.field.falgebra]
rs2:290 [in mathcomp.field.falgebra]
rs:10 [in mathcomp.field.galois]
rs:1193 [in mathcomp.algebra.poly]
rs:1213 [in mathcomp.algebra.poly]
rs:1215 [in mathcomp.algebra.poly]
rs:1244 [in mathcomp.algebra.poly]
rs:1248 [in mathcomp.algebra.poly]
rs:1254 [in mathcomp.algebra.poly]
rs:1256 [in mathcomp.algebra.poly]
rs:1263 [in mathcomp.algebra.poly]
rs:1268 [in mathcomp.algebra.poly]
rs:1269 [in mathcomp.algebra.poly]
rs:188 [in mathcomp.algebra.polydiv]
rs:215 [in mathcomp.solvable.cyclic]
rs:272 [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:782 [in mathcomp.algebra.mxpoly]
rs:843 [in mathcomp.algebra.mxpoly]
rs:844 [in mathcomp.algebra.mxpoly]
rs:848 [in mathcomp.algebra.mxpoly]
rs:862 [in mathcomp.algebra.mxpoly]
rs:863 [in mathcomp.algebra.mxpoly]
RtoK:382 [in mathcomp.algebra.mxpoly]
RtoK:388 [in mathcomp.algebra.mxpoly]
rT':29 [in mathcomp.fingroup.action]
rT:1 [in mathcomp.ssreflect.ssrfun]
rT:10 [in mathcomp.ssreflect.ssrfun]
rT:1019 [in mathcomp.character.character]
rT:102 [in mathcomp.solvable.gfunctor]
rT:1025 [in mathcomp.character.character]
rT:107 [in mathcomp.solvable.gfunctor]
rt:110 [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:1340 [in mathcomp.ssreflect.seq]
rT:1345 [in mathcomp.ssreflect.seq]
rT:148 [in mathcomp.solvable.center]
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:29 [in mathcomp.ssreflect.ssrbool]
rT:32 [in mathcomp.ssreflect.ssrfun]
rT:33 [in mathcomp.ssreflect.finfun]
rT:35 [in mathcomp.ssreflect.ssrbool]
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:517 [in mathcomp.ssreflect.finset]
rT:525 [in mathcomp.ssreflect.finset]
rT:534 [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:623 [in mathcomp.ssreflect.fintype]
rT:63 [in mathcomp.ssreflect.ssrfun]
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.solvable.maximal]
rT:671 [in mathcomp.algebra.vector]
rT:674 [in mathcomp.algebra.vector]
rT:678 [in mathcomp.algebra.vector]
rT:68 [in mathcomp.ssreflect.ssrfun]
rT:69 [in mathcomp.fingroup.presentation]
rT:70 [in mathcomp.solvable.gseries]
rT:71 [in mathcomp.fingroup.presentation]
rT:72 [in mathcomp.ssreflect.ssrfun]
rT:79 [in mathcomp.ssreflect.finfun]
rT:8 [in mathcomp.ssreflect.ssrbool]
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:861 [in mathcomp.character.classfun]
rT:865 [in mathcomp.character.classfun]
rT:867 [in mathcomp.algebra.vector]
rT:869 [in mathcomp.algebra.vector]
rT:87 [in mathcomp.fingroup.presentation]
rT:90 [in mathcomp.ssreflect.ssrbool]
rT:92 [in mathcomp.fingroup.presentation]
rT:950 [in mathcomp.ssreflect.finset]
rT:99 [in mathcomp.fingroup.presentation]
rU:119 [in mathcomp.character.character]
rU:129 [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:151 [in mathcomp.character.character]
rW:158 [in mathcomp.character.character]
rxx:204 [in mathcomp.ssreflect.generic_quotient]
Rx:158 [in mathcomp.field.algebraics_fundamentals]
rX:175 [in mathcomp.solvable.finmodule]
rX:188 [in mathcomp.solvable.finmodule]
rz:222 [in mathcomp.field.galois]
r_a:536 [in mathcomp.field.galois]
R_:3498 [in mathcomp.algebra.matrix]
r_:3309 [in mathcomp.algebra.matrix]
R_:3279 [in mathcomp.algebra.matrix]
R_:3272 [in mathcomp.algebra.matrix]
R_:3260 [in mathcomp.algebra.matrix]
R_:3067 [in mathcomp.algebra.matrix]
R_:3048 [in mathcomp.algebra.matrix]
R_:3022 [in mathcomp.algebra.matrix]
R_:3008 [in mathcomp.algebra.matrix]
R_:3003 [in mathcomp.algebra.matrix]
R_:2996 [in mathcomp.algebra.matrix]
R_:2965 [in mathcomp.algebra.matrix]
r_:912 [in mathcomp.ssreflect.bigop]
r_:901 [in mathcomp.ssreflect.bigop]
R_:1798 [in mathcomp.algebra.mxalgebra]
R_:1607 [in mathcomp.algebra.mxalgebra]
R'_:3009 [in mathcomp.algebra.matrix]
R'_:2997 [in mathcomp.algebra.matrix]
r':1568 [in mathcomp.ssreflect.order]
r':1580 [in mathcomp.ssreflect.order]
r':1592 [in mathcomp.ssreflect.order]
r':1607 [in mathcomp.ssreflect.order]
R':2092 [in mathcomp.ssreflect.seq]
r':2435 [in mathcomp.ssreflect.seq]
r':2443 [in mathcomp.ssreflect.seq]
r':2453 [in mathcomp.ssreflect.seq]
r':2459 [in mathcomp.ssreflect.seq]
r':2497 [in mathcomp.ssreflect.seq]
r':2537 [in mathcomp.ssreflect.seq]
r':2541 [in mathcomp.ssreflect.seq]
r':2546 [in mathcomp.ssreflect.seq]
r':2550 [in mathcomp.ssreflect.seq]
r':2558 [in mathcomp.ssreflect.seq]
R':557 [in mathcomp.algebra.ssrint]
R':759 [in mathcomp.algebra.ssrint]
r1:1142 [in mathcomp.ssreflect.bigop]
r1:12 [in mathcomp.algebra.polydiv]
r1:1256 [in mathcomp.algebra.mxalgebra]
r1:133 [in mathcomp.field.closed_field]
r1:1402 [in mathcomp.ssreflect.bigop]
r1:1420 [in mathcomp.ssreflect.bigop]
r1:1439 [in mathcomp.ssreflect.bigop]
r1:145 [in mathcomp.field.closed_field]
R1:1587 [in mathcomp.algebra.mxalgebra]
R1:1593 [in mathcomp.algebra.mxalgebra]
R1:1600 [in mathcomp.algebra.mxalgebra]
R1:1629 [in mathcomp.algebra.mxalgebra]
R1:1637 [in mathcomp.algebra.mxalgebra]
R1:1642 [in mathcomp.algebra.mxalgebra]
R1:1650 [in mathcomp.algebra.mxalgebra]
R1:1660 [in mathcomp.algebra.mxalgebra]
R1:1669 [in mathcomp.algebra.mxalgebra]
R1:1677 [in mathcomp.algebra.mxalgebra]
r1:1690 [in mathcomp.ssreflect.seq]
R1:1694 [in mathcomp.algebra.mxalgebra]
R1:1701 [in mathcomp.algebra.mxalgebra]
R1:1708 [in mathcomp.algebra.mxalgebra]
R1:1714 [in mathcomp.algebra.mxalgebra]
R1:1722 [in mathcomp.algebra.mxalgebra]
R1:1727 [in mathcomp.algebra.mxalgebra]
R1:1732 [in mathcomp.algebra.mxalgebra]
R1:1792 [in mathcomp.algebra.mxalgebra]
r1:1818 [in mathcomp.ssreflect.bigop]
r1:1836 [in mathcomp.ssreflect.bigop]
r1:1855 [in mathcomp.ssreflect.bigop]
r1:192 [in mathcomp.field.separable]
r1:2063 [in mathcomp.ssreflect.bigop]
r1:286 [in mathcomp.fingroup.gproduct]
R1:3049 [in mathcomp.algebra.ssralg]
R1:3085 [in mathcomp.algebra.ssralg]
r1:366 [in mathcomp.algebra.intdiv]
r1:368 [in mathcomp.algebra.intdiv]
r1:370 [in mathcomp.algebra.intdiv]
R1:48 [in mathcomp.field.cyclotomic]
R1:482 [in mathcomp.character.classfun]
R1:486 [in mathcomp.character.classfun]
r1:511 [in mathcomp.ssreflect.div]
r1:513 [in mathcomp.ssreflect.div]
r1:515 [in mathcomp.ssreflect.div]
r1:585 [in mathcomp.ssreflect.bigop]
r1:652 [in mathcomp.ssreflect.bigop]
r1:666 [in mathcomp.ssreflect.bigop]
r1:676 [in mathcomp.ssreflect.bigop]
r2v:33 [in mathcomp.algebra.vector]
r2:1143 [in mathcomp.ssreflect.bigop]
r2:1257 [in mathcomp.algebra.mxalgebra]
r2:1403 [in mathcomp.ssreflect.bigop]
r2:1422 [in mathcomp.ssreflect.bigop]
r2:1440 [in mathcomp.ssreflect.bigop]
R2:1588 [in mathcomp.algebra.mxalgebra]
R2:1594 [in mathcomp.algebra.mxalgebra]
R2:1601 [in mathcomp.algebra.mxalgebra]
R2:1630 [in mathcomp.algebra.mxalgebra]
R2:1638 [in mathcomp.algebra.mxalgebra]
R2:1643 [in mathcomp.algebra.mxalgebra]
R2:1651 [in mathcomp.algebra.mxalgebra]
R2:1661 [in mathcomp.algebra.mxalgebra]
R2:1670 [in mathcomp.algebra.mxalgebra]
R2:1678 [in mathcomp.algebra.mxalgebra]
r2:1692 [in mathcomp.ssreflect.seq]
R2:1695 [in mathcomp.algebra.mxalgebra]
R2:1702 [in mathcomp.algebra.mxalgebra]
R2:1709 [in mathcomp.algebra.mxalgebra]
R2:1718 [in mathcomp.algebra.mxalgebra]
R2:1723 [in mathcomp.algebra.mxalgebra]
R2:1728 [in mathcomp.algebra.mxalgebra]
R2:1733 [in mathcomp.algebra.mxalgebra]
R2:1793 [in mathcomp.algebra.mxalgebra]
r2:1819 [in mathcomp.ssreflect.bigop]
r2:1838 [in mathcomp.ssreflect.bigop]
r2:1856 [in mathcomp.ssreflect.bigop]
r2:2064 [in mathcomp.ssreflect.bigop]
r2:287 [in mathcomp.fingroup.gproduct]
R2:3050 [in mathcomp.algebra.ssralg]
R2:3086 [in mathcomp.algebra.ssralg]
r2:367 [in mathcomp.algebra.intdiv]
r2:369 [in mathcomp.algebra.intdiv]
r2:371 [in mathcomp.algebra.intdiv]
R2:483 [in mathcomp.character.classfun]
R2:487 [in mathcomp.character.classfun]
R2:49 [in mathcomp.field.cyclotomic]
r2:512 [in mathcomp.ssreflect.div]
r2:514 [in mathcomp.ssreflect.div]
r2:516 [in mathcomp.ssreflect.div]
r2:586 [in mathcomp.ssreflect.bigop]
r2:653 [in mathcomp.ssreflect.bigop]
r2:667 [in mathcomp.ssreflect.bigop]
r2:677 [in mathcomp.ssreflect.bigop]
R3:1662 [in mathcomp.algebra.mxalgebra]
R3:1671 [in mathcomp.algebra.mxalgebra]
R3:1696 [in mathcomp.algebra.mxalgebra]
R3:1703 [in mathcomp.algebra.mxalgebra]
R3:1710 [in mathcomp.algebra.mxalgebra]
R4:1663 [in mathcomp.algebra.mxalgebra]
R4:1672 [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:1008 [in mathcomp.fingroup.fingroup]
r:1009 [in mathcomp.algebra.polydiv]
r:1014 [in mathcomp.algebra.polydiv]
R:1015 [in mathcomp.ssreflect.bigop]
r:1018 [in mathcomp.fingroup.fingroup]
R:1025 [in mathcomp.algebra.ssralg]
R:1027 [in mathcomp.character.character]
r:1029 [in mathcomp.algebra.polydiv]
r:103 [in mathcomp.algebra.polyXY]
r:103 [in mathcomp.solvable.nilpotent]
R:1034 [in mathcomp.algebra.ssralg]
r:1035 [in mathcomp.ssreflect.bigop]
r:104 [in mathcomp.algebra.polyXY]
R:1045 [in mathcomp.algebra.ssralg]
R:1046 [in mathcomp.algebra.ssralg]
R:1048 [in mathcomp.algebra.ssralg]
r:1048 [in mathcomp.algebra.vector]
r:105 [in mathcomp.character.inertia]
r:1050 [in mathcomp.algebra.vector]
R:1054 [in mathcomp.algebra.ssralg]
R:1058 [in mathcomp.algebra.ssralg]
R:106 [in mathcomp.solvable.pgroup]
R:1066 [in mathcomp.algebra.ssralg]
R:107 [in mathcomp.ssreflect.finfun]
R:107 [in mathcomp.algebra.finalg]
R:107 [in mathcomp.fingroup.morphism]
r:1072 [in mathcomp.algebra.poly]
R:1077 [in mathcomp.algebra.ssralg]
r:108 [in mathcomp.algebra.polydiv]
R:108 [in mathcomp.algebra.finalg]
R:108 [in mathcomp.ssreflect.eqtype]
R:1084 [in mathcomp.algebra.ssralg]
R:109 [in mathcomp.algebra.finalg]
R:109 [in mathcomp.fingroup.morphism]
r:1092 [in mathcomp.ssreflect.bigop]
R:1094 [in mathcomp.algebra.ssralg]
r:1097 [in mathcomp.algebra.poly]
r:1098 [in mathcomp.ssreflect.bigop]
R:1099 [in mathcomp.algebra.ssralg]
R:11 [in mathcomp.field.cyclotomic]
R:11 [in mathcomp.algebra.matrix]
R:110 [in mathcomp.solvable.pgroup]
R:110 [in mathcomp.algebra.finalg]
R:110 [in mathcomp.algebra.ssrnum]
r:1100 [in mathcomp.algebra.poly]
R:1104 [in mathcomp.algebra.ssralg]
r:1106 [in mathcomp.ssreflect.bigop]
R:111 [in mathcomp.algebra.finalg]
R:111 [in mathcomp.fingroup.morphism]
R:1115 [in mathcomp.algebra.ssralg]
r:1118 [in mathcomp.ssreflect.bigop]
R:112 [in mathcomp.algebra.finalg]
r:1122 [in mathcomp.ssreflect.finset]
R:113 [in mathcomp.algebra.finalg]
R:113 [in mathcomp.ssreflect.eqtype]
r:1132 [in mathcomp.ssreflect.bigop]
R:114 [in mathcomp.algebra.finalg]
r:1144 [in mathcomp.fingroup.fingroup]
r:1149 [in mathcomp.algebra.ssrnum]
R:115 [in mathcomp.algebra.finalg]
R:115 [in mathcomp.solvable.gfunctor]
r:115 [in mathcomp.solvable.nilpotent]
r:1155 [in mathcomp.fingroup.fingroup]
R:116 [in mathcomp.algebra.ssrnum]
r:1160 [in mathcomp.ssreflect.finset]
r:1163 [in mathcomp.algebra.ssralg]
r:1170 [in mathcomp.ssreflect.finset]
r:1176 [in mathcomp.ssreflect.bigop]
r:118 [in mathcomp.algebra.interval]
r:118 [in mathcomp.ssreflect.tuple]
R:118 [in mathcomp.algebra.ssrnum]
r:1197 [in mathcomp.ssreflect.finset]
r:1197 [in mathcomp.ssreflect.bigop]
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:1207 [in mathcomp.algebra.ssralg]
R:1214 [in mathcomp.algebra.ssralg]
R:1216 [in mathcomp.algebra.poly]
R:1217 [in mathcomp.algebra.poly]
R:1218 [in mathcomp.algebra.poly]
R:1219 [in mathcomp.algebra.poly]
R:122 [in mathcomp.solvable.gseries]
R:122 [in mathcomp.ssreflect.bigop]
R:1220 [in mathcomp.algebra.poly]
R:1221 [in mathcomp.algebra.poly]
R:1222 [in mathcomp.algebra.poly]
R:1223 [in mathcomp.algebra.poly]
R:1224 [in mathcomp.algebra.poly]
R:1225 [in mathcomp.algebra.poly]
R:1228 [in mathcomp.algebra.ssralg]
R:123 [in mathcomp.algebra.mxpoly]
R:1231 [in mathcomp.algebra.ssralg]
R:1234 [in mathcomp.algebra.ssralg]
R:1244 [in mathcomp.algebra.ssralg]
r:1255 [in mathcomp.algebra.ssralg]
r:126 [in mathcomp.field.closed_field]
R:126 [in mathcomp.ssreflect.bigop]
r:1262 [in mathcomp.algebra.poly]
r:1265 [in mathcomp.algebra.ssralg]
r:1266 [in mathcomp.algebra.poly]
r:127 [in mathcomp.solvable.burnside_app]
r:1281 [in mathcomp.algebra.mxalgebra]
R:1282 [in mathcomp.algebra.ssralg]
R:1285 [in mathcomp.algebra.ssralg]
R:1288 [in mathcomp.algebra.ssralg]
R:1290 [in mathcomp.algebra.ssralg]
R:1299 [in mathcomp.algebra.ssralg]
R:13 [in mathcomp.algebra.countalg]
r:13 [in mathcomp.field.algnum]
R:13 [in mathcomp.algebra.finalg]
r:130 [in mathcomp.algebra.polydiv]
r:130 [in mathcomp.field.finfield]
R:130 [in mathcomp.algebra.finalg]
r:131 [in mathcomp.field.finfield]
R:131 [in mathcomp.ssreflect.bigop]
r:1318 [in mathcomp.algebra.matrix]
r:132 [in mathcomp.ssreflect.prime]
R:132 [in mathcomp.algebra.finalg]
r:1325 [in mathcomp.algebra.matrix]
r:1327 [in mathcomp.algebra.matrix]
r:1329 [in mathcomp.ssreflect.seq]
r:133 [in mathcomp.field.finfield]
r:133 [in mathcomp.solvable.burnside_app]
r:1332 [in mathcomp.algebra.poly]
R:1333 [in mathcomp.algebra.ssralg]
r:134 [in mathcomp.algebra.polydiv]
R:134 [in mathcomp.algebra.finalg]
r:134 [in mathcomp.ssreflect.bigop]
R:1341 [in mathcomp.algebra.ssralg]
R:1346 [in mathcomp.algebra.ssralg]
r:1348 [in mathcomp.ssreflect.bigop]
R:1350 [in mathcomp.algebra.ssralg]
R:1357 [in mathcomp.algebra.ssralg]
r:1358 [in mathcomp.ssreflect.bigop]
r:136 [in mathcomp.algebra.polydiv]
R:136 [in mathcomp.algebra.ring_quotient]
R:136 [in mathcomp.algebra.finalg]
r:1369 [in mathcomp.ssreflect.bigop]
r:1377 [in mathcomp.algebra.ssralg]
R:138 [in mathcomp.algebra.finalg]
r:1380 [in mathcomp.ssreflect.bigop]
r:139 [in mathcomp.algebra.polydiv]
R:139 [in mathcomp.algebra.ssrint]
r:1391 [in mathcomp.ssreflect.bigop]
r:14 [in mathcomp.solvable.burnside_app]
R:140 [in mathcomp.algebra.ring_quotient]
r:140 [in mathcomp.field.closed_field]
R:140 [in mathcomp.algebra.finalg]
R:141 [in mathcomp.fingroup.morphism]
R:142 [in mathcomp.algebra.finalg]
R:1421 [in mathcomp.algebra.ssralg]
r:143 [in mathcomp.algebra.polydiv]
R:143 [in mathcomp.algebra.ssrint]
r:143 [in mathcomp.solvable.nilpotent]
R:1431 [in mathcomp.algebra.ssralg]
R:1434 [in mathcomp.algebra.ssralg]
R:1436 [in mathcomp.algebra.ssralg]
R:144 [in mathcomp.ssreflect.finfun]
R:144 [in mathcomp.algebra.ring_quotient]
R:144 [in mathcomp.algebra.finalg]
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:1470 [in mathcomp.ssreflect.bigop]
R:148 [in mathcomp.algebra.finalg]
r:1484 [in mathcomp.ssreflect.bigop]
R:149 [in mathcomp.algebra.ring_quotient]
R:149 [in mathcomp.fingroup.morphism]
r:1494 [in mathcomp.ssreflect.bigop]
r:15 [in mathcomp.solvable.burnside_app]
r:150 [in mathcomp.field.closed_field]
R:150 [in mathcomp.algebra.finalg]
R:151 [in mathcomp.algebra.ring_quotient]
R:1513 [in mathcomp.algebra.ssralg]
R:1516 [in mathcomp.algebra.ssralg]
r:152 [in mathcomp.ssreflect.generic_quotient]
R:152 [in mathcomp.algebra.finalg]
R:152 [in mathcomp.fingroup.morphism]
R:1525 [in mathcomp.algebra.ssralg]
R:1529 [in mathcomp.algebra.ssralg]
R:153 [in mathcomp.field.algebraics_fundamentals]
R:153 [in mathcomp.algebra.ring_quotient]
R:153 [in mathcomp.fingroup.morphism]
R:1534 [in mathcomp.algebra.ssralg]
R:154 [in mathcomp.algebra.finalg]
r:1541 [in mathcomp.ssreflect.order]
R:155 [in mathcomp.algebra.finalg]
R:155 [in mathcomp.fingroup.morphism]
r:1554 [in mathcomp.ssreflect.order]
R:156 [in mathcomp.algebra.finalg]
r:156 [in mathcomp.algebra.mxalgebra]
r:1564 [in mathcomp.algebra.matrix]
r:1567 [in mathcomp.ssreflect.order]
r:157 [in mathcomp.field.closed_field]
R:157 [in mathcomp.algebra.finalg]
r:1578 [in mathcomp.algebra.matrix]
r:1579 [in mathcomp.ssreflect.order]
R:1579 [in mathcomp.algebra.mxalgebra]
r:158 [in mathcomp.ssreflect.binomial]
R:158 [in mathcomp.algebra.ring_quotient]
R:158 [in mathcomp.algebra.finalg]
R:159 [in mathcomp.algebra.finalg]
r:1591 [in mathcomp.ssreflect.order]
R:16 [in mathcomp.algebra.countalg]
R:16 [in mathcomp.algebra.finalg]
r:16 [in mathcomp.solvable.burnside_app]
R:160 [in mathcomp.algebra.finalg]
r:1606 [in mathcomp.ssreflect.order]
r:161 [in mathcomp.ssreflect.generic_quotient]
r:1617 [in mathcomp.algebra.ssralg]
R:162 [in mathcomp.algebra.ring_quotient]
r:162 [in mathcomp.algebra.ssrnum]
r:162 [in mathcomp.algebra.mxalgebra]
r:1621 [in mathcomp.ssreflect.order]
r:1622 [in mathcomp.algebra.ssralg]
r:1623 [in mathcomp.ssreflect.seq]
R:1623 [in mathcomp.algebra.mxalgebra]
r:1626 [in mathcomp.algebra.ssralg]
R:163 [in mathcomp.fingroup.morphism]
r:1634 [in mathcomp.ssreflect.order]
R:164 [in mathcomp.fingroup.morphism]
r:1646 [in mathcomp.algebra.ssralg]
r:165 [in mathcomp.algebra.ssralg]
r:1650 [in mathcomp.algebra.ssralg]
R:1652 [in mathcomp.algebra.mxalgebra]
r:166 [in mathcomp.field.galois]
R:166 [in mathcomp.algebra.ring_quotient]
r:166 [in mathcomp.field.closed_field]
r:1668 [in mathcomp.ssreflect.seq]
r:167 [in mathcomp.solvable.sylow]
r:1678 [in mathcomp.ssreflect.seq]
R:168 [in mathcomp.character.inertia]
r:168 [in mathcomp.fingroup.fingroup]
r:1681 [in mathcomp.ssreflect.seq]
r:1686 [in mathcomp.ssreflect.seq]
r:17 [in mathcomp.fingroup.presentation]
R:170 [in mathcomp.algebra.mxpoly]
r:1705 [in mathcomp.ssreflect.bigop]
r:1709 [in mathcomp.ssreflect.bigop]
R:171 [in mathcomp.algebra.ring_quotient]
r:1715 [in mathcomp.ssreflect.bigop]
R:173 [in mathcomp.fingroup.morphism]
r:1736 [in mathcomp.ssreflect.bigop]
R:1736 [in mathcomp.algebra.mxalgebra]
r:1742 [in mathcomp.ssreflect.bigop]
R:1742 [in mathcomp.algebra.mxalgebra]
R:1744 [in mathcomp.algebra.ssralg]
R:1745 [in mathcomp.algebra.mxalgebra]
R:1747 [in mathcomp.algebra.ssralg]
R:1748 [in mathcomp.algebra.mxalgebra]
R:175 [in mathcomp.algebra.ring_quotient]
r:175 [in mathcomp.algebra.ssralg]
R:1750 [in mathcomp.algebra.ssralg]
r:1750 [in mathcomp.ssreflect.bigop]
r:1755 [in mathcomp.algebra.matrix]
R:1758 [in mathcomp.algebra.mxalgebra]
r:1760 [in mathcomp.algebra.matrix]
r:1762 [in mathcomp.algebra.matrix]
r:1764 [in mathcomp.algebra.matrix]
r:1764 [in mathcomp.ssreflect.bigop]
R:1764 [in mathcomp.algebra.mxalgebra]
r:1766 [in mathcomp.algebra.ssralg]
r:1767 [in mathcomp.algebra.matrix]
R:1769 [in mathcomp.algebra.mxalgebra]
r:177 [in mathcomp.algebra.polydiv]
r:1770 [in mathcomp.algebra.matrix]
R:1772 [in mathcomp.algebra.mxalgebra]
r:1773 [in mathcomp.algebra.matrix]
r:1774 [in mathcomp.ssreflect.bigop]
r:1776 [in mathcomp.algebra.matrix]
R:1776 [in mathcomp.algebra.mxalgebra]
r:178 [in mathcomp.field.closed_field]
R:1780 [in mathcomp.algebra.mxalgebra]
r:1781 [in mathcomp.algebra.matrix]
r:1783 [in mathcomp.algebra.ssralg]
r:1785 [in mathcomp.algebra.matrix]
r:1785 [in mathcomp.ssreflect.bigop]
R:1785 [in mathcomp.algebra.mxalgebra]
R:1788 [in mathcomp.algebra.mxalgebra]
r:1796 [in mathcomp.ssreflect.bigop]
R:1797 [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.ssreflect.finfun]
R:180 [in mathcomp.algebra.ring_quotient]
r:1807 [in mathcomp.ssreflect.bigop]
R:181 [in mathcomp.ssreflect.finfun]
R:1817 [in mathcomp.algebra.ssralg]
R:1819 [in mathcomp.algebra.ssralg]
R:182 [in mathcomp.ssreflect.binomial]
R:1822 [in mathcomp.algebra.ssralg]
R:1827 [in mathcomp.algebra.ssralg]
R:1828 [in mathcomp.algebra.ssralg]
R:183 [in mathcomp.algebra.mxpoly]
r:183 [in mathcomp.field.closed_field]
R:1831 [in mathcomp.algebra.ssralg]
R:1833 [in mathcomp.algebra.ssralg]
R:1839 [in mathcomp.algebra.ssralg]
r:1868 [in mathcomp.algebra.ssralg]
r:1878 [in mathcomp.algebra.ssralg]
r:188 [in mathcomp.ssreflect.prime]
r:188 [in mathcomp.character.character]
r:189 [in mathcomp.field.galois]
R:189 [in mathcomp.algebra.mxpoly]
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:1901 [in mathcomp.algebra.matrix]
r:191 [in mathcomp.field.fieldext]
R:1910 [in mathcomp.algebra.matrix]
R:1915 [in mathcomp.algebra.matrix]
R:1918 [in mathcomp.algebra.matrix]
R:192 [in mathcomp.solvable.cyclic]
r:1920 [in mathcomp.algebra.ssralg]
r:193 [in mathcomp.field.fieldext]
r:1935 [in mathcomp.algebra.matrix]
R:194 [in mathcomp.algebra.mxpoly]
R:194 [in mathcomp.fingroup.morphism]
R:1940 [in mathcomp.algebra.matrix]
R:195 [in mathcomp.fingroup.morphism]
R:1957 [in mathcomp.algebra.ssralg]
R:1961 [in mathcomp.algebra.ssralg]
R:197 [in mathcomp.fingroup.morphism]
R:1978 [in mathcomp.algebra.matrix]
r:199 [in mathcomp.character.classfun]
R:199 [in mathcomp.fingroup.morphism]
r:2 [in mathcomp.ssreflect.prime]
R:2014 [in mathcomp.algebra.matrix]
r:202 [in mathcomp.algebra.ssrint]
r:202 [in mathcomp.solvable.nilpotent]
r:2026 [in mathcomp.ssreflect.bigop]
r:2027 [in mathcomp.ssreflect.bigop]
r:2028 [in mathcomp.ssreflect.bigop]
R:2030 [in mathcomp.algebra.ssralg]
r:2035 [in mathcomp.ssreflect.bigop]
R:204 [in mathcomp.algebra.mxpoly]
R:2046 [in mathcomp.algebra.ssralg]
R:205 [in mathcomp.fingroup.morphism]
r:2052 [in mathcomp.ssreflect.bigop]
R:2058 [in mathcomp.algebra.ssralg]
r:206 [in mathcomp.algebra.poly]
R:2065 [in mathcomp.algebra.ssralg]
R:207 [in mathcomp.fingroup.morphism]
r:2074 [in mathcomp.ssreflect.bigop]
r:208 [in mathcomp.field.separable]
R:208 [in mathcomp.algebra.mxpoly]
r:2084 [in mathcomp.ssreflect.order]
r:2084 [in mathcomp.ssreflect.bigop]
R:2086 [in mathcomp.algebra.ssralg]
R:2091 [in mathcomp.ssreflect.seq]
R:2091 [in mathcomp.algebra.ssralg]
r:2092 [in mathcomp.ssreflect.order]
R:2096 [in mathcomp.algebra.ssralg]
r:2098 [in mathcomp.ssreflect.bigop]
R:21 [in mathcomp.algebra.mxpoly]
R:2101 [in mathcomp.algebra.ssralg]
R:211 [in mathcomp.fingroup.morphism]
r:2112 [in mathcomp.ssreflect.bigop]
r:2116 [in mathcomp.ssreflect.order]
R:212 [in mathcomp.algebra.mxpoly]
R:212 [in mathcomp.fingroup.morphism]
R:212 [in mathcomp.algebra.ssralg]
R:2123 [in mathcomp.algebra.ssralg]
R:2124 [in mathcomp.ssreflect.seq]
r:2125 [in mathcomp.ssreflect.order]
R:2128 [in mathcomp.algebra.ssralg]
r:213 [in mathcomp.algebra.ssrint]
R:2133 [in mathcomp.algebra.ssralg]
R:2138 [in mathcomp.algebra.ssralg]
r:214 [in mathcomp.solvable.nilpotent]
R:2143 [in mathcomp.algebra.ssralg]
R:2148 [in mathcomp.algebra.ssralg]
R:215 [in mathcomp.solvable.maximal]
R:2153 [in mathcomp.algebra.ssralg]
R:2158 [in mathcomp.algebra.ssralg]
r:216 [in mathcomp.character.mxrepresentation]
r:216 [in mathcomp.algebra.vector]
R:2163 [in mathcomp.algebra.ssralg]
R:2168 [in mathcomp.algebra.ssralg]
R:217 [in mathcomp.solvable.maximal]
R:2173 [in mathcomp.algebra.ssralg]
r:2175 [in mathcomp.ssreflect.order]
R:2178 [in mathcomp.algebra.ssralg]
r:2184 [in mathcomp.algebra.matrix]
r:2187 [in mathcomp.algebra.matrix]
r:2190 [in mathcomp.algebra.matrix]
r:2192 [in mathcomp.algebra.matrix]
R:2192 [in mathcomp.algebra.ssralg]
r:2196 [in mathcomp.ssreflect.order]
R:2197 [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:220 [in mathcomp.field.separable]
R:2201 [in mathcomp.algebra.ssralg]
r:2204 [in mathcomp.ssreflect.order]
R:2206 [in mathcomp.algebra.ssralg]
R:2210 [in mathcomp.algebra.ssralg]
R:2215 [in mathcomp.algebra.ssralg]
R:2219 [in mathcomp.algebra.ssralg]
R:2224 [in mathcomp.algebra.ssralg]
r:2228 [in mathcomp.ssreflect.order]
R:2228 [in mathcomp.algebra.ssralg]
R:2233 [in mathcomp.algebra.ssralg]
r:2237 [in mathcomp.ssreflect.order]
R:2237 [in mathcomp.algebra.ssralg]
R:224 [in mathcomp.fingroup.morphism]
R:224 [in mathcomp.algebra.ssralg]
R:2242 [in mathcomp.algebra.ssralg]
R:2245 [in mathcomp.algebra.matrix]
R:2246 [in mathcomp.algebra.ssralg]
R:2250 [in mathcomp.algebra.matrix]
R:2253 [in mathcomp.algebra.matrix]
R:2253 [in mathcomp.algebra.ssralg]
R:2259 [in mathcomp.algebra.ssralg]
r:226 [in mathcomp.algebra.polydiv]
R:2266 [in mathcomp.algebra.ssralg]
R:227 [in mathcomp.algebra.ssralg]
r:2270 [in mathcomp.algebra.matrix]
R:2272 [in mathcomp.algebra.ssralg]
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:2281 [in mathcomp.algebra.ssralg]
R:2284 [in mathcomp.algebra.matrix]
r:2287 [in mathcomp.ssreflect.order]
R:2288 [in mathcomp.algebra.ssralg]
r:2299 [in mathcomp.algebra.ssralg]
R:2300 [in mathcomp.ssreflect.seq]
r:233 [in mathcomp.algebra.polydiv]
R:233 [in mathcomp.character.classfun]
r:2330 [in mathcomp.algebra.ssralg]
r:235 [in mathcomp.field.fieldext]
R:236 [in mathcomp.solvable.maximal]
R:2362 [in mathcomp.algebra.ssrnum]
R:238 [in mathcomp.algebra.ssrnum]
R:2389 [in mathcomp.algebra.ssrnum]
r:239 [in mathcomp.fingroup.gproduct]
R:24 [in mathcomp.algebra.ssrnum]
r:240 [in mathcomp.algebra.mxpoly]
R:240 [in mathcomp.solvable.maximal]
R:2405 [in mathcomp.algebra.ssrnum]
R:2408 [in mathcomp.algebra.ssrnum]
r:241 [in mathcomp.algebra.mxpoly]
R:2410 [in mathcomp.algebra.ssrnum]
r:242 [in mathcomp.algebra.mxpoly]
r:243 [in mathcomp.field.galois]
r:2434 [in mathcomp.ssreflect.seq]
R:2435 [in mathcomp.algebra.ssrnum]
R:244 [in mathcomp.algebra.ssralg]
r:2442 [in mathcomp.ssreflect.seq]
R:2450 [in mathcomp.algebra.ssrnum]
r:2452 [in mathcomp.ssreflect.seq]
r:2458 [in mathcomp.ssreflect.seq]
R:246 [in mathcomp.algebra.ssralg]
r:2462 [in mathcomp.ssreflect.seq]
r:2470 [in mathcomp.ssreflect.seq]
R:2475 [in mathcomp.algebra.ssrnum]
r:2478 [in mathcomp.ssreflect.seq]
R:2479 [in mathcomp.algebra.ssralg]
R:2483 [in mathcomp.algebra.matrix]
r:2485 [in mathcomp.ssreflect.seq]
R:2486 [in mathcomp.algebra.ssralg]
R:249 [in mathcomp.algebra.ssralg]
r:2490 [in mathcomp.ssreflect.order]
R:2491 [in mathcomp.algebra.ssralg]
r:2496 [in mathcomp.ssreflect.seq]
R:2498 [in mathcomp.algebra.ssralg]
R:25 [in mathcomp.algebra.countalg]
R:25 [in mathcomp.algebra.finalg]
R:25 [in mathcomp.algebra.vector]
r:2500 [in mathcomp.ssreflect.order]
R:2505 [in mathcomp.algebra.ssralg]
r:2514 [in mathcomp.ssreflect.bigop]
R:2515 [in mathcomp.algebra.ssralg]
R:2516 [in mathcomp.algebra.matrix]
R:252 [in mathcomp.algebra.ssralg]
R:2520 [in mathcomp.algebra.ssralg]
R:2521 [in mathcomp.algebra.matrix]
R:2526 [in mathcomp.algebra.matrix]
R:2526 [in mathcomp.algebra.ssralg]
r:2527 [in mathcomp.ssreflect.bigop]
R:2529 [in mathcomp.algebra.matrix]
R:2532 [in mathcomp.algebra.ssralg]
r:2536 [in mathcomp.ssreflect.seq]
R:2536 [in mathcomp.algebra.matrix]
R:2537 [in mathcomp.algebra.ssralg]
R:254 [in mathcomp.algebra.ssralg]
r:2540 [in mathcomp.ssreflect.seq]
R:2544 [in mathcomp.algebra.ssralg]
r:2544 [in mathcomp.ssreflect.bigop]
r:2545 [in mathcomp.ssreflect.seq]
r:2549 [in mathcomp.ssreflect.seq]
r:2554 [in mathcomp.ssreflect.seq]
R:2554 [in mathcomp.algebra.ssralg]
r:2557 [in mathcomp.ssreflect.seq]
R:2559 [in mathcomp.algebra.ssralg]
r:2562 [in mathcomp.ssreflect.bigop]
R:2565 [in mathcomp.algebra.ssralg]
R:2571 [in mathcomp.algebra.ssralg]
r:2573 [in mathcomp.ssreflect.bigop]
R:2580 [in mathcomp.algebra.ssralg]
R:2586 [in mathcomp.algebra.ssralg]
R:2590 [in mathcomp.algebra.ssralg]
R:2599 [in mathcomp.algebra.ssralg]
R:26 [in mathcomp.algebra.zmodp]
R:2611 [in mathcomp.algebra.ssralg]
R:262 [in mathcomp.fingroup.quotient]
R:2620 [in mathcomp.algebra.ssralg]
R:2628 [in mathcomp.algebra.ssralg]
R:2639 [in mathcomp.algebra.ssralg]
R:264 [in mathcomp.algebra.interval]
R:2648 [in mathcomp.algebra.ssralg]
r:265 [in mathcomp.field.closed_field]
R:2650 [in mathcomp.algebra.matrix]
R:2656 [in mathcomp.algebra.ssralg]
R:2667 [in mathcomp.algebra.ssralg]
r:2669 [in mathcomp.algebra.matrix]
R:2672 [in mathcomp.algebra.matrix]
R:2672 [in mathcomp.algebra.ssralg]
R:2679 [in mathcomp.algebra.ssralg]
R:2689 [in mathcomp.algebra.ssralg]
R:2694 [in mathcomp.algebra.ssralg]
R:2699 [in mathcomp.algebra.ssralg]
r:27 [in mathcomp.fingroup.presentation]
R:270 [in mathcomp.algebra.ssralg]
R:2705 [in mathcomp.algebra.ssralg]
R:272 [in mathcomp.algebra.ssralg]
R:2731 [in mathcomp.algebra.ssralg]
R:2734 [in mathcomp.ssreflect.bigop]
R:2738 [in mathcomp.algebra.ssralg]
r:274 [in mathcomp.fingroup.gproduct]
R:2744 [in mathcomp.algebra.ssralg]
r:275 [in mathcomp.algebra.ssralg]
R:2751 [in mathcomp.algebra.ssralg]
R:2757 [in mathcomp.algebra.ssralg]
R:2764 [in mathcomp.algebra.ssralg]
R:277 [in mathcomp.fingroup.morphism]
R:2770 [in mathcomp.algebra.ssralg]
r:2770 [in mathcomp.ssreflect.bigop]
r:2776 [in mathcomp.ssreflect.bigop]
R:2777 [in mathcomp.algebra.ssralg]
R:2783 [in mathcomp.algebra.ssralg]
R:2792 [in mathcomp.algebra.ssralg]
R:28 [in mathcomp.algebra.countalg]
R:28 [in mathcomp.algebra.finalg]
r:280 [in mathcomp.solvable.extremal]
R:280 [in mathcomp.fingroup.morphism]
R:2800 [in mathcomp.algebra.ssralg]
R:2809 [in mathcomp.algebra.ssralg]
R:2817 [in mathcomp.algebra.ssralg]
r:2825 [in mathcomp.ssreflect.bigop]
R:2826 [in mathcomp.algebra.ssralg]
R:2834 [in mathcomp.algebra.ssralg]
R:284 [in mathcomp.fingroup.morphism]
R:2841 [in mathcomp.algebra.ssralg]
R:2847 [in mathcomp.algebra.ssralg]
r:2850 [in mathcomp.ssreflect.bigop]
R:2854 [in mathcomp.algebra.ssralg]
r:286 [in mathcomp.algebra.ssralg]
R:2860 [in mathcomp.algebra.ssralg]
r:2862 [in mathcomp.ssreflect.bigop]
R:2867 [in mathcomp.algebra.ssralg]
R:2873 [in mathcomp.algebra.ssralg]
R:2875 [in mathcomp.algebra.ssralg]
R:2877 [in mathcomp.algebra.ssralg]
R:2879 [in mathcomp.algebra.ssralg]
r:288 [in mathcomp.character.classfun]
r:2886 [in mathcomp.ssreflect.bigop]
r:2898 [in mathcomp.ssreflect.bigop]
r:29 [in mathcomp.field.separable]
r:2906 [in mathcomp.ssreflect.bigop]
r:2914 [in mathcomp.ssreflect.bigop]
r:2943 [in mathcomp.ssreflect.bigop]
R:295 [in mathcomp.ssreflect.bigop]
r:2960 [in mathcomp.ssreflect.bigop]
r:298 [in mathcomp.algebra.ssrint]
r:3003 [in mathcomp.ssreflect.bigop]
r:301 [in mathcomp.ssreflect.bigop]
r:305 [in mathcomp.character.classfun]
R:3057 [in mathcomp.algebra.matrix]
r:306 [in mathcomp.algebra.poly]
r:308 [in mathcomp.algebra.ssrint]
R:3087 [in mathcomp.algebra.ssralg]
R:31 [in mathcomp.algebra.countalg]
R:31 [in mathcomp.algebra.finalg]
R:3144 [in mathcomp.algebra.matrix]
r:315 [in mathcomp.solvable.abelian]
r:3159 [in mathcomp.ssreflect.order]
r:316 [in mathcomp.algebra.mxalgebra]
r:3171 [in mathcomp.ssreflect.order]
r:322 [in mathcomp.field.fieldext]
R:3246 [in mathcomp.algebra.matrix]
r:325 [in mathcomp.ssreflect.bigop]
r:328 [in mathcomp.algebra.ssrnum]
R:33 [in mathcomp.algebra.zmodp]
R:3303 [in mathcomp.algebra.matrix]
r:3306 [in mathcomp.algebra.matrix]
r:337 [in mathcomp.algebra.ssrnum]
R:34 [in mathcomp.algebra.countalg]
R:34 [in mathcomp.fingroup.morphism]
R:340 [in mathcomp.solvable.extremal]
r:345 [in mathcomp.character.character]
R:3459 [in mathcomp.algebra.matrix]
R:3493 [in mathcomp.algebra.matrix]
r:350 [in mathcomp.ssreflect.tuple]
R:3504 [in mathcomp.algebra.matrix]
R:3519 [in mathcomp.algebra.matrix]
r:352 [in mathcomp.ssreflect.tuple]
r:352 [in mathcomp.ssreflect.bigop]
R:3534 [in mathcomp.algebra.matrix]
r:354 [in mathcomp.algebra.polydiv]
R:3540 [in mathcomp.algebra.matrix]
r:357 [in mathcomp.algebra.polydiv]
R:36 [in mathcomp.algebra.finalg]
r:36 [in mathcomp.algebra.vector]
r:365 [in mathcomp.fingroup.gproduct]
R:37 [in mathcomp.algebra.countalg]
R:37 [in mathcomp.field.separable]
R:37 [in mathcomp.algebra.polyXY]
r:37 [in mathcomp.algebra.vector]
r:376 [in mathcomp.fingroup.gproduct]
r:378 [in mathcomp.ssreflect.bigop]
R:38 [in mathcomp.algebra.countalg]
R:380 [in mathcomp.algebra.mxpoly]
r:381 [in mathcomp.algebra.vector]
r:382 [in mathcomp.algebra.poly]
r:383 [in mathcomp.character.classfun]
R:386 [in mathcomp.algebra.mxpoly]
r:387 [in mathcomp.fingroup.gproduct]
R:39 [in mathcomp.algebra.countalg]
R:393 [in mathcomp.fingroup.morphism]
R:396 [in mathcomp.fingroup.morphism]
r:397 [in mathcomp.character.character]
r:398 [in mathcomp.ssreflect.bigop]
R:4 [in mathcomp.algebra.ssrnum]
R:40 [in mathcomp.algebra.countalg]
R:40 [in mathcomp.algebra.ssrnum]
R:408 [in mathcomp.field.closed_field]
R:41 [in mathcomp.algebra.finalg]
r:41 [in mathcomp.fingroup.morphism]
R:412 [in mathcomp.field.closed_field]
r:414 [in mathcomp.algebra.intdiv]
r:415 [in mathcomp.algebra.mxpoly]
r:416 [in mathcomp.character.classfun]
r:417 [in mathcomp.ssreflect.bigop]
R:42 [in mathcomp.algebra.matrix]
r:426 [in mathcomp.field.galois]
r:426 [in mathcomp.fingroup.gproduct]
r:426 [in mathcomp.algebra.ssralg]
R:43 [in mathcomp.algebra.ssrnum]
r:431 [in mathcomp.algebra.intdiv]
r:433 [in mathcomp.algebra.polydiv]
r:434 [in mathcomp.ssreflect.bigop]
r:436 [in mathcomp.algebra.polydiv]
r:436 [in mathcomp.algebra.poly]
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:444 [in mathcomp.algebra.polydiv]
r:446 [in mathcomp.algebra.mxpoly]
r:447 [in mathcomp.algebra.mxpoly]
r:447 [in mathcomp.ssreflect.bigop]
R:45 [in mathcomp.algebra.matrix]
r:45 [in mathcomp.algebra.rat]
R:455 [in mathcomp.algebra.mxpoly]
r:458 [in mathcomp.field.galois]
r:459 [in mathcomp.field.galois]
r:459 [in mathcomp.ssreflect.bigop]
R:46 [in mathcomp.algebra.finalg]
R:460 [in mathcomp.algebra.mxpoly]
R:462 [in mathcomp.fingroup.action]
r:462 [in mathcomp.fingroup.fingroup]
r:464 [in mathcomp.algebra.ssralg]
R:465 [in mathcomp.fingroup.action]
R:467 [in mathcomp.algebra.mxpoly]
R:468 [in mathcomp.character.classfun]
r:469 [in mathcomp.algebra.mxpoly]
R:47 [in mathcomp.algebra.mxpoly]
R:473 [in mathcomp.character.classfun]
R:474 [in mathcomp.character.character]
r:475 [in mathcomp.field.galois]
r:476 [in mathcomp.fingroup.fingroup]
r:477 [in mathcomp.ssreflect.bigop]
R:48 [in mathcomp.algebra.matrix]
r:480 [in mathcomp.field.galois]
R:483 [in mathcomp.algebra.ssrint]
R:489 [in mathcomp.character.classfun]
r:496 [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:506 [in mathcomp.algebra.polydiv]
r:506 [in mathcomp.field.galois]
r:506 [in mathcomp.ssreflect.bigop]
r:507 [in mathcomp.field.galois]
R:508 [in mathcomp.character.classfun]
r:51 [in mathcomp.field.cyclotomic]
R:51 [in mathcomp.algebra.matrix]
R:51 [in mathcomp.algebra.finalg]
R:51 [in mathcomp.algebra.fraction]
R:511 [in mathcomp.character.classfun]
R:511 [in mathcomp.algebra.ssralg]
r:512 [in mathcomp.fingroup.gproduct]
R:513 [in mathcomp.character.classfun]
R:514 [in mathcomp.algebra.ssralg]
R:517 [in mathcomp.character.classfun]
R:519 [in mathcomp.character.classfun]
r:519 [in mathcomp.ssreflect.bigop]
r:52 [in mathcomp.field.separable]
R:52 [in mathcomp.algebra.finalg]
r:523 [in mathcomp.ssreflect.bigop]
R:524 [in mathcomp.algebra.ssralg]
r:526 [in mathcomp.algebra.ssrnum]
R:526 [in mathcomp.algebra.ssralg]
r:53 [in mathcomp.field.separable]
R:53 [in mathcomp.algebra.finalg]
R:530 [in mathcomp.character.classfun]
R:532 [in mathcomp.character.classfun]
r:532 [in mathcomp.ssreflect.bigop]
r:533 [in mathcomp.field.galois]
r:534 [in mathcomp.algebra.ssrnum]
R:536 [in mathcomp.ssreflect.finset]
r:538 [in mathcomp.algebra.polydiv]
r:539 [in mathcomp.algebra.polydiv]
r:540 [in mathcomp.algebra.mxpoly]
r:542 [in mathcomp.ssreflect.bigop]
R:543 [in mathcomp.algebra.ssralg]
R:55 [in mathcomp.field.finfield]
r:552 [in mathcomp.character.character]
r:552 [in mathcomp.ssreflect.bigop]
r:553 [in mathcomp.algebra.mxpoly]
r:557 [in mathcomp.algebra.ssrnum]
r:558 [in mathcomp.algebra.mxpoly]
r:558 [in mathcomp.character.character]
r:56 [in mathcomp.field.separable]
r:562 [in mathcomp.ssreflect.bigop]
r:567 [in mathcomp.ssreflect.prime]
R:57 [in mathcomp.field.finfield]
r:573 [in mathcomp.ssreflect.bigop]
r:574 [in mathcomp.algebra.ssrnum]
r:575 [in mathcomp.algebra.mxpoly]
r:576 [in mathcomp.algebra.mxpoly]
r:577 [in mathcomp.algebra.mxpoly]
R:584 [in mathcomp.algebra.ssrint]
r:585 [in mathcomp.algebra.polydiv]
r:588 [in mathcomp.algebra.polydiv]
R:59 [in mathcomp.field.finfield]
r:597 [in mathcomp.algebra.polydiv]
R:6 [in mathcomp.algebra.vector]
r:60 [in mathcomp.algebra.ssralg]
r:600 [in mathcomp.algebra.polydiv]
R:602 [in mathcomp.solvable.pgroup]
r:604 [in mathcomp.ssreflect.bigop]
R:61 [in mathcomp.field.finfield]
r:616 [in mathcomp.ssreflect.bigop]
r:624 [in mathcomp.fingroup.fingroup]
r:626 [in mathcomp.ssreflect.bigop]
R:63 [in mathcomp.field.finfield]
R:63 [in mathcomp.algebra.finalg]
r:635 [in mathcomp.ssreflect.bigop]
r:64 [in mathcomp.field.cyclotomic]
R:64 [in mathcomp.algebra.finalg]
r:641 [in mathcomp.ssreflect.bigop]
R:643 [in mathcomp.algebra.ssralg]
r:646 [in mathcomp.algebra.polydiv]
r:646 [in mathcomp.ssreflect.bigop]
r:649 [in mathcomp.algebra.polydiv]
r:65 [in mathcomp.field.cyclotomic]
R:65 [in mathcomp.algebra.finalg]
R:659 [in mathcomp.algebra.ssralg]
r:66 [in mathcomp.field.cyclotomic]
R:66 [in mathcomp.algebra.finalg]
R:66 [in mathcomp.algebra.ssrnum]
R:66 [in mathcomp.fingroup.morphism]
r:667 [in mathcomp.algebra.polydiv]
r:669 [in mathcomp.algebra.polydiv]
R:67 [in mathcomp.field.cyclotomic]
r:673 [in mathcomp.algebra.polydiv]
R:674 [in mathcomp.algebra.ssralg]
r:676 [in mathcomp.algebra.polydiv]
R:677 [in mathcomp.solvable.abelian]
R:68 [in mathcomp.algebra.finalg]
R:682 [in mathcomp.solvable.abelian]
r:688 [in mathcomp.ssreflect.bigop]
R:69 [in mathcomp.algebra.ssrnum]
R:69 [in mathcomp.fingroup.morphism]
r:69 [in mathcomp.solvable.center]
R:691 [in mathcomp.algebra.ssralg]
r:697 [in mathcomp.ssreflect.bigop]
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.fingroup.morphism]
R:700 [in mathcomp.ssreflect.finset]
r:707 [in mathcomp.ssreflect.bigop]
r:71 [in mathcomp.character.mxabelem]
r:712 [in mathcomp.algebra.polydiv]
r:716 [in mathcomp.ssreflect.bigop]
R:719 [in mathcomp.character.classfun]
R:72 [in mathcomp.field.finfield]
r:72 [in mathcomp.algebra.ssralg]
r:727 [in mathcomp.algebra.ssralg]
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:738 [in mathcomp.algebra.ssralg]
R:74 [in mathcomp.field.finfield]
R:74 [in mathcomp.fingroup.morphism]
r:741 [in mathcomp.algebra.polydiv]
R:75 [in mathcomp.ssreflect.ssrAC]
r:750 [in mathcomp.algebra.matrix]
R:753 [in mathcomp.algebra.ssralg]
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:761 [in mathcomp.algebra.ssralg]
R:762 [in mathcomp.algebra.ssrint]
R:766 [in mathcomp.algebra.ssralg]
r:771 [in mathcomp.algebra.matrix]
R:78 [in mathcomp.field.finfield]
r:783 [in mathcomp.algebra.mxpoly]
r:784 [in mathcomp.algebra.mxpoly]
r:785 [in mathcomp.algebra.mxpoly]
R:79 [in mathcomp.algebra.finalg]
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.algebra.finalg]
R:80 [in mathcomp.fingroup.morphism]
r:802 [in mathcomp.algebra.polydiv]
r:806 [in mathcomp.algebra.vector]
R:81 [in mathcomp.algebra.finalg]
r:814 [in mathcomp.algebra.ssrnum]
r:816 [in mathcomp.algebra.poly]
r:819 [in mathcomp.algebra.poly]
R:82 [in mathcomp.algebra.finalg]
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:829 [in mathcomp.algebra.polydiv]
R:83 [in mathcomp.algebra.finalg]
r:830 [in mathcomp.algebra.ssrnum]
r:831 [in mathcomp.algebra.polydiv]
R:84 [in mathcomp.algebra.finalg]
R:84 [in mathcomp.fingroup.morphism]
r:84 [in mathcomp.solvable.center]
r:843 [in mathcomp.algebra.ssrnum]
r:845 [in mathcomp.algebra.mxpoly]
r:846 [in mathcomp.algebra.mxpoly]
r:847 [in mathcomp.algebra.mxpoly]
r:848 [in mathcomp.algebra.mxalgebra]
r:849 [in mathcomp.algebra.mxpoly]
R:85 [in mathcomp.algebra.ssrnum]
r:850 [in mathcomp.algebra.mxpoly]
r:850 [in mathcomp.algebra.mxalgebra]
r:851 [in mathcomp.algebra.mxpoly]
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:867 [in mathcomp.character.classfun]
R:868 [in mathcomp.algebra.ssrint]
R:87 [in mathcomp.solvable.pgroup]
R:87 [in mathcomp.solvable.hall]
r:874 [in mathcomp.algebra.polydiv]
r:874 [in mathcomp.algebra.ssralg]
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:882 [in mathcomp.algebra.polydiv]
R:883 [in mathcomp.algebra.matrix]
r:89 [in mathcomp.algebra.polydiv]
R:892 [in mathcomp.ssreflect.finset]
r:897 [in mathcomp.ssreflect.bigop]
r:905 [in mathcomp.algebra.poly]
r:909 [in mathcomp.ssreflect.bigop]
R:91 [in mathcomp.algebra.ssrnum]
r:91 [in mathcomp.solvable.nilpotent]
r:92 [in mathcomp.algebra.poly]
r:920 [in mathcomp.ssreflect.bigop]
r:929 [in mathcomp.algebra.polydiv]
R:93 [in mathcomp.fingroup.morphism]
R:931 [in mathcomp.ssreflect.seq]
r:932 [in mathcomp.algebra.polydiv]
R:937 [in mathcomp.algebra.ssralg]
R:94 [in mathcomp.algebra.ssrnum]
R:940 [in mathcomp.algebra.matrix]
r:943 [in mathcomp.ssreflect.ssrnat]
R:944 [in mathcomp.algebra.ssralg]
r:949 [in mathcomp.algebra.polydiv]
r:949 [in mathcomp.algebra.poly]
R:951 [in mathcomp.algebra.ssralg]
r:952 [in mathcomp.algebra.polydiv]
R:952 [in mathcomp.ssreflect.finset]
r:955 [in mathcomp.algebra.polydiv]
r:956 [in mathcomp.ssreflect.ssrnat]
r:959 [in mathcomp.algebra.vector]
r:967 [in mathcomp.ssreflect.ssrnat]
r:968 [in mathcomp.algebra.ssralg]
R:97 [in mathcomp.fingroup.morphism]
r:981 [in mathcomp.ssreflect.ssrnat]
r:982 [in mathcomp.algebra.ssralg]
r:987 [in mathcomp.algebra.polydiv]
r:998 [in mathcomp.algebra.matrix]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74637 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1852 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48381 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (277 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3804 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (91 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14415 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (132 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1342 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1003 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3033 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |