| 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 | (78577 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 | (1807 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 | (48032 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 | (375 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 | (3995 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 | (14468 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 | (223 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 | (45 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 | (133 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 | (451 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 | (1387 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 | (1144 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 | (6179 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 | (247 entries) |
R (binder)
rc:108 [in mathcomp.algebra.ring_quotient]rc:114 [in mathcomp.algebra.ring_quotient]
rc:145 [in mathcomp.algebra.ring_quotient]
rc:180 [in mathcomp.algebra.ring_quotient]
rc:186 [in mathcomp.algebra.ring_quotient]
rc:77 [in mathcomp.algebra.ring_quotient]
recf:552 [in mathcomp.algebra.mxpoly]
redg:2006 [in mathcomp.algebra.ssralg]
rfG:656 [in mathcomp.character.character]
rGf:1418 [in mathcomp.character.mxrepresentation]
rG0:156 [in mathcomp.character.mxrepresentation]
rG1:109 [in mathcomp.character.character]
rG1:112 [in mathcomp.character.character]
rG1:1259 [in mathcomp.character.mxrepresentation]
rG1:1414 [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:825 [in mathcomp.character.mxrepresentation]
rG1:834 [in mathcomp.character.mxrepresentation]
rG1:840 [in mathcomp.character.mxrepresentation]
rG1:845 [in mathcomp.character.mxrepresentation]
rG1:850 [in mathcomp.character.mxrepresentation]
rG1:864 [in mathcomp.character.mxrepresentation]
rG1:868 [in mathcomp.character.mxrepresentation]
rG1:873 [in mathcomp.character.mxrepresentation]
rG1:877 [in mathcomp.character.mxrepresentation]
rG1:887 [in mathcomp.character.mxrepresentation]
rG1:892 [in mathcomp.character.mxrepresentation]
rG2:110 [in mathcomp.character.character]
rG2:113 [in mathcomp.character.character]
rG2:1260 [in mathcomp.character.mxrepresentation]
rG2:1415 [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:827 [in mathcomp.character.mxrepresentation]
rG2:835 [in mathcomp.character.mxrepresentation]
rG2:841 [in mathcomp.character.mxrepresentation]
rG2:846 [in mathcomp.character.mxrepresentation]
rG2:851 [in mathcomp.character.mxrepresentation]
rG2:865 [in mathcomp.character.mxrepresentation]
rG2:869 [in mathcomp.character.mxrepresentation]
rG2:874 [in mathcomp.character.mxrepresentation]
rG2:878 [in mathcomp.character.mxrepresentation]
rG2:888 [in mathcomp.character.mxrepresentation]
rG2:893 [in mathcomp.character.mxrepresentation]
rG3:847 [in mathcomp.character.mxrepresentation]
rG:1038 [in mathcomp.character.character]
rG:1417 [in mathcomp.character.mxrepresentation]
rG:1437 [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:795 [in mathcomp.character.mxrepresentation]
rG:806 [in mathcomp.character.mxrepresentation]
rG:808 [in mathcomp.character.mxrepresentation]
rG:811 [in mathcomp.character.mxrepresentation]
rG:813 [in mathcomp.character.mxrepresentation]
rG:816 [in mathcomp.character.mxrepresentation]
rG:837 [in mathcomp.character.mxrepresentation]
rG:857 [in mathcomp.character.mxrepresentation]
rG:87 [in mathcomp.character.integral_char]
rG:880 [in mathcomp.character.mxrepresentation]
rG:91 [in mathcomp.character.integral_char]
rG:997 [in mathcomp.character.character]
rho:112 [in mathcomp.solvable.pgroup]
rho:116 [in mathcomp.solvable.pgroup]
rho:120 [in mathcomp.solvable.pgroup]
rho:127 [in mathcomp.solvable.pgroup]
rho:31 [in mathcomp.solvable.pgroup]
rho:34 [in mathcomp.solvable.pgroup]
rho:37 [in mathcomp.solvable.pgroup]
rho: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:117 [in mathcomp.ssreflect.choice]
rhs:124 [in mathcomp.ssreflect.choice]
rid:102 [in mathcomp.ssreflect.ssrAC]
ringS:1588 [in mathcomp.algebra.ssralg]
ringS:1594 [in mathcomp.algebra.ssralg]
ringS:1597 [in mathcomp.algebra.ssralg]
ringS:160 [in mathcomp.field.algC]
ringS:1607 [in mathcomp.algebra.ssralg]
ringS:186 [in mathcomp.field.algC]
ringS:256 [in mathcomp.algebra.rat]
ringS:2598 [in mathcomp.algebra.matrix]
ringS:331 [in mathcomp.field.algC]
ringS:594 [in mathcomp.algebra.poly]
ringS:634 [in mathcomp.algebra.poly]
ringS:680 [in mathcomp.algebra.poly]
ringS:828 [in mathcomp.algebra.poly]
ringS:859 [in mathcomp.algebra.ssrint]
rI:1583 [in mathcomp.ssreflect.bigop]
rI:1606 [in mathcomp.ssreflect.bigop]
rI:2457 [in mathcomp.ssreflect.bigop]
rI:2479 [in mathcomp.ssreflect.bigop]
rI:2787 [in mathcomp.ssreflect.bigop]
rI:344 [in mathcomp.algebra.poly]
rI:353 [in mathcomp.algebra.poly]
rI:360 [in mathcomp.algebra.poly]
rJ:1584 [in mathcomp.ssreflect.bigop]
rJ:1607 [in mathcomp.ssreflect.bigop]
rJ:2458 [in mathcomp.ssreflect.bigop]
rJ:2480 [in mathcomp.ssreflect.bigop]
rJ:2788 [in mathcomp.ssreflect.bigop]
rk:191 [in mathcomp.algebra.vector]
rngS:1819 [in mathcomp.algebra.ssralg]
Rorder:14 [in mathcomp.algebra.ssrnum]
Rorder:3 [in mathcomp.algebra.ssrnum]
RoverFp:172 [in mathcomp.field.finfield]
row1:731 [in mathcomp.algebra.matrix]
row3:733 [in mathcomp.algebra.matrix]
rP:12 [in mathcomp.ssreflect.ssrbool]
rP:94 [in mathcomp.ssreflect.ssrbool]
rqc:162 [in mathcomp.algebra.ring_quotient]
rqc:164 [in mathcomp.algebra.ring_quotient]
rqc:166 [in mathcomp.algebra.ring_quotient]
rqc:94 [in mathcomp.algebra.ring_quotient]
rqc:96 [in mathcomp.algebra.ring_quotient]
rqT:100 [in mathcomp.algebra.ring_quotient]
rqT:101 [in mathcomp.algebra.ring_quotient]
rqT:102 [in mathcomp.algebra.ring_quotient]
rqT:103 [in mathcomp.algebra.ring_quotient]
rqT:121 [in mathcomp.algebra.ring_quotient]
rqT:122 [in mathcomp.algebra.ring_quotient]
rqT:123 [in mathcomp.algebra.ring_quotient]
rqT:128 [in mathcomp.algebra.ring_quotient]
rqT:129 [in mathcomp.algebra.ring_quotient]
rqT:159 [in mathcomp.algebra.ring_quotient]
rqT:161 [in mathcomp.algebra.ring_quotient]
rqT:163 [in mathcomp.algebra.ring_quotient]
rqT:165 [in mathcomp.algebra.ring_quotient]
rqT:167 [in mathcomp.algebra.ring_quotient]
rqT:168 [in mathcomp.algebra.ring_quotient]
rqT:169 [in mathcomp.algebra.ring_quotient]
rqT:170 [in mathcomp.algebra.ring_quotient]
rqT:171 [in mathcomp.algebra.ring_quotient]
rqT:172 [in mathcomp.algebra.ring_quotient]
rqT:173 [in mathcomp.algebra.ring_quotient]
rqT:174 [in mathcomp.algebra.ring_quotient]
rqT:175 [in mathcomp.algebra.ring_quotient]
rqT:193 [in mathcomp.algebra.ring_quotient]
rqT:194 [in mathcomp.algebra.ring_quotient]
rqT:197 [in mathcomp.algebra.ring_quotient]
rqT:200 [in mathcomp.algebra.ring_quotient]
rqT:201 [in mathcomp.algebra.ring_quotient]
rqT:91 [in mathcomp.algebra.ring_quotient]
rqT:93 [in mathcomp.algebra.ring_quotient]
rqT:95 [in mathcomp.algebra.ring_quotient]
rqT:97 [in mathcomp.algebra.ring_quotient]
rqT:98 [in mathcomp.algebra.ring_quotient]
rqT:99 [in mathcomp.algebra.ring_quotient]
rQ:2476 [in mathcomp.algebra.ssralg]
rr:1984 [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:68 [in mathcomp.algebra.polydiv]
rR:74 [in mathcomp.field.algnum]
rr:77 [in mathcomp.algebra.polydiv]
rR:868 [in mathcomp.algebra.poly]
rs1:299 [in mathcomp.field.falgebra]
rs2:300 [in mathcomp.field.falgebra]
rs:10 [in mathcomp.field.galois]
rs:1226 [in mathcomp.algebra.poly]
rs:1246 [in mathcomp.algebra.poly]
rs:1248 [in mathcomp.algebra.poly]
rs:1273 [in mathcomp.algebra.poly]
rs:1277 [in mathcomp.algebra.poly]
rs:1283 [in mathcomp.algebra.poly]
rs:1285 [in mathcomp.algebra.poly]
rs:1292 [in mathcomp.algebra.poly]
rs:1297 [in mathcomp.algebra.poly]
rs:1298 [in mathcomp.algebra.poly]
rs:188 [in mathcomp.algebra.polydiv]
rs:215 [in mathcomp.solvable.cyclic]
rs:264 [in mathcomp.field.separable]
rs:283 [in mathcomp.field.falgebra]
rs:285 [in mathcomp.field.falgebra]
rs:297 [in mathcomp.field.falgebra]
rs:388 [in mathcomp.algebra.polydiv]
rs:57 [in mathcomp.field.fieldext]
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:1013 [in mathcomp.character.character]
rT:1019 [in mathcomp.character.character]
rT:102 [in mathcomp.solvable.gfunctor]
rT:107 [in mathcomp.solvable.gfunctor]
rt:110 [in mathcomp.field.closed_field]
rT:112 [in mathcomp.solvable.gfunctor]
rT:113 [in mathcomp.algebra.ring_quotient]
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: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:178 [in mathcomp.algebra.ring_quotient]
rT:185 [in mathcomp.algebra.ring_quotient]
rT:19 [in mathcomp.ssreflect.ssrfun]
rT:215 [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.finfun]
rT:32 [in mathcomp.ssreflect.ssrfun]
rT:35 [in mathcomp.ssreflect.finfun]
rT:35 [in mathcomp.ssreflect.ssrbool]
rT:38 [in mathcomp.ssreflect.ssrfun]
rT:39 [in mathcomp.solvable.maximal]
rT:40 [in mathcomp.field.fieldext]
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:43 [in mathcomp.field.fieldext]
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:46 [in mathcomp.field.fieldext]
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:521 [in mathcomp.ssreflect.finset]
rT:529 [in mathcomp.ssreflect.finset]
rT:540 [in mathcomp.ssreflect.finset]
rT:544 [in mathcomp.ssreflect.finset]
rT:549 [in mathcomp.ssreflect.finset]
rT:57 [in mathcomp.fingroup.presentation]
rT:59 [in mathcomp.solvable.center]
rT:595 [in mathcomp.algebra.vector]
rT:599 [in mathcomp.solvable.pgroup]
rT:63 [in mathcomp.ssreflect.ssrfun]
rT:644 [in mathcomp.ssreflect.fintype]
rT:67 [in mathcomp.solvable.maximal]
rT:671 [in mathcomp.algebra.vector]
rT:674 [in mathcomp.algebra.vector]
rT:679 [in mathcomp.algebra.vector]
rT:68 [in mathcomp.ssreflect.ssrfun]
rT:684 [in mathcomp.algebra.vector]
rT:687 [in mathcomp.algebra.vector]
rT:69 [in mathcomp.fingroup.presentation]
rT:690 [in mathcomp.algebra.vector]
rT:694 [in mathcomp.algebra.vector]
rT:70 [in mathcomp.solvable.gseries]
rT:71 [in mathcomp.fingroup.presentation]
rT:72 [in mathcomp.ssreflect.ssrfun]
rT:8 [in mathcomp.ssreflect.ssrbool]
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:865 [in mathcomp.character.classfun]
rT:869 [in mathcomp.character.classfun]
rT:87 [in mathcomp.ssreflect.finfun]
rT:87 [in mathcomp.fingroup.presentation]
rT:88 [in mathcomp.ssreflect.finfun]
rT:884 [in mathcomp.algebra.vector]
rT:886 [in mathcomp.algebra.vector]
rT:89 [in mathcomp.ssreflect.finfun]
rT:90 [in mathcomp.ssreflect.finfun]
rT:90 [in mathcomp.ssreflect.ssrbool]
rT:91 [in mathcomp.ssreflect.finfun]
rT:92 [in mathcomp.ssreflect.finfun]
rT:92 [in mathcomp.fingroup.presentation]
rT:93 [in mathcomp.ssreflect.finfun]
rT:967 [in mathcomp.ssreflect.finset]
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:178 [in mathcomp.algebra.vector]
rv:19 [in mathcomp.field.finfield]
rV:288 [in mathcomp.algebra.ssrint]
rw:1039 [in mathcomp.algebra.vector]
rw:1043 [in mathcomp.algebra.vector]
rW:149 [in mathcomp.character.character]
rW:156 [in mathcomp.character.character]
rxx:227 [in mathcomp.ssreflect.generic_quotient]
Rx:160 [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:528 [in mathcomp.field.galois]
R_:3422 [in mathcomp.algebra.matrix]
r_:3233 [in mathcomp.algebra.matrix]
R_:3203 [in mathcomp.algebra.matrix]
R_:3196 [in mathcomp.algebra.matrix]
R_:3184 [in mathcomp.algebra.matrix]
R_:2991 [in mathcomp.algebra.matrix]
R_:2972 [in mathcomp.algebra.matrix]
R_:2946 [in mathcomp.algebra.matrix]
R_:2932 [in mathcomp.algebra.matrix]
R_:2927 [in mathcomp.algebra.matrix]
R_:2920 [in mathcomp.algebra.matrix]
R_:2889 [in mathcomp.algebra.matrix]
r_:848 [in mathcomp.ssreflect.bigop]
r_:837 [in mathcomp.ssreflect.bigop]
R_:1777 [in mathcomp.algebra.mxalgebra]
R_:1586 [in mathcomp.algebra.mxalgebra]
R'_:2933 [in mathcomp.algebra.matrix]
R'_:2921 [in mathcomp.algebra.matrix]
r':1702 [in mathcomp.ssreflect.order]
r':1714 [in mathcomp.ssreflect.order]
r':1726 [in mathcomp.ssreflect.order]
r':1741 [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:1079 [in mathcomp.ssreflect.bigop]
r1:12 [in mathcomp.algebra.polydiv]
r1:1235 [in mathcomp.algebra.mxalgebra]
r1:133 [in mathcomp.field.closed_field]
r1:1366 [in mathcomp.ssreflect.bigop]
r1:1384 [in mathcomp.ssreflect.bigop]
r1:1403 [in mathcomp.ssreflect.bigop]
r1:145 [in mathcomp.field.closed_field]
R1:1566 [in mathcomp.algebra.mxalgebra]
R1:1572 [in mathcomp.algebra.mxalgebra]
R1:1579 [in mathcomp.algebra.mxalgebra]
R1:1608 [in mathcomp.algebra.mxalgebra]
R1:1616 [in mathcomp.algebra.mxalgebra]
R1:1621 [in mathcomp.algebra.mxalgebra]
R1:1629 [in mathcomp.algebra.mxalgebra]
R1:1639 [in mathcomp.algebra.mxalgebra]
R1:1648 [in mathcomp.algebra.mxalgebra]
R1:1656 [in mathcomp.algebra.mxalgebra]
R1:1673 [in mathcomp.algebra.mxalgebra]
R1:1680 [in mathcomp.algebra.mxalgebra]
R1:1687 [in mathcomp.algebra.mxalgebra]
r1:1690 [in mathcomp.ssreflect.seq]
R1:1693 [in mathcomp.algebra.mxalgebra]
R1:1701 [in mathcomp.algebra.mxalgebra]
R1:1706 [in mathcomp.algebra.mxalgebra]
R1:1711 [in mathcomp.algebra.mxalgebra]
R1:1771 [in mathcomp.algebra.mxalgebra]
r1:1782 [in mathcomp.ssreflect.bigop]
r1:1800 [in mathcomp.ssreflect.bigop]
r1:1819 [in mathcomp.ssreflect.bigop]
r1:184 [in mathcomp.field.separable]
r1:2016 [in mathcomp.ssreflect.bigop]
r1:2082 [in mathcomp.ssreflect.bigop]
R1:2714 [in mathcomp.algebra.ssralg]
r1:286 [in mathcomp.fingroup.gproduct]
r1:370 [in mathcomp.algebra.intdiv]
r1:372 [in mathcomp.algebra.intdiv]
r1:374 [in mathcomp.algebra.intdiv]
R1:48 [in mathcomp.field.cyclotomic]
R1:483 [in mathcomp.character.classfun]
R1:487 [in mathcomp.character.classfun]
r1:511 [in mathcomp.ssreflect.div]
r1:513 [in mathcomp.ssreflect.div]
r1:515 [in mathcomp.ssreflect.div]
r1:521 [in mathcomp.ssreflect.bigop]
r1:588 [in mathcomp.ssreflect.bigop]
r1:602 [in mathcomp.ssreflect.bigop]
r1:612 [in mathcomp.ssreflect.bigop]
r2v:41 [in mathcomp.algebra.vector]
r2:1080 [in mathcomp.ssreflect.bigop]
r2:1236 [in mathcomp.algebra.mxalgebra]
r2:1367 [in mathcomp.ssreflect.bigop]
r2:1386 [in mathcomp.ssreflect.bigop]
r2:1404 [in mathcomp.ssreflect.bigop]
R2:1567 [in mathcomp.algebra.mxalgebra]
R2:1573 [in mathcomp.algebra.mxalgebra]
R2:1580 [in mathcomp.algebra.mxalgebra]
R2:1609 [in mathcomp.algebra.mxalgebra]
R2:1617 [in mathcomp.algebra.mxalgebra]
R2:1622 [in mathcomp.algebra.mxalgebra]
R2:1630 [in mathcomp.algebra.mxalgebra]
R2:1640 [in mathcomp.algebra.mxalgebra]
R2:1649 [in mathcomp.algebra.mxalgebra]
R2:1657 [in mathcomp.algebra.mxalgebra]
R2:1674 [in mathcomp.algebra.mxalgebra]
R2:1681 [in mathcomp.algebra.mxalgebra]
R2:1688 [in mathcomp.algebra.mxalgebra]
r2:1692 [in mathcomp.ssreflect.seq]
R2:1697 [in mathcomp.algebra.mxalgebra]
R2:1702 [in mathcomp.algebra.mxalgebra]
R2:1707 [in mathcomp.algebra.mxalgebra]
R2:1712 [in mathcomp.algebra.mxalgebra]
R2:1772 [in mathcomp.algebra.mxalgebra]
r2:1783 [in mathcomp.ssreflect.bigop]
r2:1802 [in mathcomp.ssreflect.bigop]
r2:1820 [in mathcomp.ssreflect.bigop]
r2:2017 [in mathcomp.ssreflect.bigop]
r2:2083 [in mathcomp.ssreflect.bigop]
R2:2715 [in mathcomp.algebra.ssralg]
r2:287 [in mathcomp.fingroup.gproduct]
r2:371 [in mathcomp.algebra.intdiv]
r2:373 [in mathcomp.algebra.intdiv]
r2:375 [in mathcomp.algebra.intdiv]
R2:484 [in mathcomp.character.classfun]
R2:488 [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:522 [in mathcomp.ssreflect.bigop]
r2:589 [in mathcomp.ssreflect.bigop]
r2:603 [in mathcomp.ssreflect.bigop]
r2:613 [in mathcomp.ssreflect.bigop]
R3:1641 [in mathcomp.algebra.mxalgebra]
R3:1650 [in mathcomp.algebra.mxalgebra]
R3:1675 [in mathcomp.algebra.mxalgebra]
R3:1682 [in mathcomp.algebra.mxalgebra]
R3:1689 [in mathcomp.algebra.mxalgebra]
R4:1642 [in mathcomp.algebra.mxalgebra]
R4:1651 [in mathcomp.algebra.mxalgebra]
R:1 [in mathcomp.algebra.ssrnum]
r:1009 [in mathcomp.algebra.polydiv]
r:1009 [in mathcomp.fingroup.fingroup]
r:1011 [in mathcomp.algebra.matrix]
r:1014 [in mathcomp.algebra.polydiv]
r:1019 [in mathcomp.fingroup.fingroup]
R:102 [in mathcomp.algebra.countalg]
R:1021 [in mathcomp.character.character]
r:1029 [in mathcomp.algebra.polydiv]
r:1029 [in mathcomp.ssreflect.bigop]
r:103 [in mathcomp.algebra.polyXY]
r:103 [in mathcomp.solvable.nilpotent]
r:1035 [in mathcomp.ssreflect.bigop]
r:104 [in mathcomp.algebra.polyXY]
r:104 [in mathcomp.algebra.poly]
r:1043 [in mathcomp.ssreflect.bigop]
r:1045 [in mathcomp.algebra.ssralg]
r:1055 [in mathcomp.ssreflect.bigop]
R:106 [in mathcomp.solvable.pgroup]
r:1065 [in mathcomp.algebra.vector]
r:1067 [in mathcomp.algebra.vector]
r:1069 [in mathcomp.ssreflect.bigop]
r:107 [in mathcomp.character.inertia]
R:107 [in mathcomp.algebra.ssrnum]
R:107 [in mathcomp.fingroup.morphism]
r:108 [in mathcomp.algebra.polydiv]
R:108 [in mathcomp.algebra.finalg]
R:109 [in mathcomp.fingroup.morphism]
R:11 [in mathcomp.field.cyclotomic]
R:110 [in mathcomp.solvable.pgroup]
r:1101 [in mathcomp.algebra.poly]
R:111 [in mathcomp.fingroup.morphism]
R:111 [in mathcomp.ssreflect.eqtype]
r:1113 [in mathcomp.ssreflect.bigop]
R:112 [in mathcomp.algebra.finalg]
R:112 [in mathcomp.algebra.ssrnum]
R:1126 [in mathcomp.algebra.ssralg]
r:1128 [in mathcomp.algebra.poly]
r:1131 [in mathcomp.algebra.poly]
r:1134 [in mathcomp.ssreflect.bigop]
R:1135 [in mathcomp.algebra.ssralg]
r:1139 [in mathcomp.ssreflect.finset]
R:114 [in mathcomp.ssreflect.finfun]
R:114 [in mathcomp.algebra.finalg]
R:1142 [in mathcomp.algebra.poly]
R:1143 [in mathcomp.algebra.poly]
r:1145 [in mathcomp.fingroup.fingroup]
R:115 [in mathcomp.solvable.gfunctor]
r:115 [in mathcomp.solvable.nilpotent]
r:1156 [in mathcomp.fingroup.fingroup]
r:1159 [in mathcomp.algebra.ssralg]
R:116 [in mathcomp.algebra.finalg]
R:116 [in mathcomp.ssreflect.eqtype]
r:1169 [in mathcomp.algebra.ssralg]
r:1177 [in mathcomp.ssreflect.finset]
r:118 [in mathcomp.ssreflect.tuple]
R:118 [in mathcomp.algebra.ssrnum]
r:118 [in mathcomp.algebra.ssralg]
r:1187 [in mathcomp.ssreflect.finset]
r:12 [in mathcomp.ssreflect.div]
r:12 [in mathcomp.field.algnum]
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:1214 [in mathcomp.ssreflect.finset]
R:122 [in mathcomp.algebra.finalg]
R:122 [in mathcomp.solvable.gseries]
R:123 [in mathcomp.algebra.mxpoly]
r:123 [in mathcomp.field.finfield]
r:124 [in mathcomp.field.finfield]
R:1245 [in mathcomp.algebra.ssralg]
R:1249 [in mathcomp.algebra.poly]
r:125 [in mathcomp.algebra.interval]
R:1250 [in mathcomp.algebra.poly]
R:1251 [in mathcomp.algebra.poly]
R:1252 [in mathcomp.algebra.poly]
R:1253 [in mathcomp.algebra.poly]
R:1254 [in mathcomp.algebra.poly]
r:126 [in mathcomp.field.closed_field]
r:126 [in mathcomp.field.finfield]
R:126 [in mathcomp.algebra.finalg]
r:1260 [in mathcomp.algebra.mxalgebra]
r:127 [in mathcomp.solvable.burnside_app]
r:1271 [in mathcomp.algebra.ssrnum]
r:1274 [in mathcomp.algebra.ssralg]
R:128 [in mathcomp.algebra.finalg]
r:128 [in mathcomp.algebra.ssralg]
r:1291 [in mathcomp.algebra.poly]
r:1295 [in mathcomp.algebra.poly]
r:13 [in mathcomp.field.algnum]
R:13 [in mathcomp.algebra.ssrnum]
r:130 [in mathcomp.algebra.polydiv]
r:1312 [in mathcomp.ssreflect.bigop]
R:1318 [in mathcomp.algebra.ssralg]
r:132 [in mathcomp.ssreflect.prime]
R:132 [in mathcomp.algebra.ssrnum]
r:1322 [in mathcomp.ssreflect.bigop]
R:1324 [in mathcomp.algebra.ssralg]
r:1329 [in mathcomp.ssreflect.seq]
r:133 [in mathcomp.solvable.burnside_app]
r:133 [in mathcomp.algebra.mxalgebra]
R:1331 [in mathcomp.algebra.ssralg]
r:1333 [in mathcomp.ssreflect.bigop]
r:134 [in mathcomp.algebra.polydiv]
R:134 [in mathcomp.algebra.finalg]
r:134 [in mathcomp.algebra.poly]
r:1344 [in mathcomp.ssreflect.bigop]
R:1346 [in mathcomp.algebra.ssralg]
R:1348 [in mathcomp.algebra.ssralg]
r:1349 [in mathcomp.algebra.matrix]
R:1349 [in mathcomp.algebra.ssralg]
R:1350 [in mathcomp.algebra.ssralg]
r:1355 [in mathcomp.ssreflect.bigop]
r:1356 [in mathcomp.algebra.matrix]
r:1358 [in mathcomp.algebra.matrix]
r:136 [in mathcomp.algebra.polydiv]
r:1361 [in mathcomp.algebra.poly]
R:138 [in mathcomp.algebra.finalg]
r:139 [in mathcomp.algebra.polydiv]
R:139 [in mathcomp.algebra.ssrint]
r:139 [in mathcomp.algebra.mxalgebra]
r:14 [in mathcomp.solvable.burnside_app]
r:140 [in mathcomp.field.closed_field]
R:140 [in mathcomp.algebra.finalg]
R:141 [in mathcomp.fingroup.morphism]
r:142 [in mathcomp.algebra.ssralg]
r:143 [in mathcomp.algebra.polydiv]
R:143 [in mathcomp.algebra.ssrint]
r:143 [in mathcomp.solvable.nilpotent]
R:1433 [in mathcomp.algebra.ssralg]
r:1434 [in mathcomp.ssreflect.bigop]
R:1437 [in mathcomp.algebra.ssralg]
r:1448 [in mathcomp.ssreflect.bigop]
R:1453 [in mathcomp.algebra.ssralg]
r:1458 [in mathcomp.ssreflect.bigop]
R:146 [in mathcomp.algebra.ssrint]
R:146 [in mathcomp.fingroup.morphism]
r:147 [in mathcomp.algebra.polydiv]
R:1471 [in mathcomp.algebra.ssralg]
R:1473 [in mathcomp.algebra.ssralg]
R:149 [in mathcomp.fingroup.morphism]
r:15 [in mathcomp.solvable.burnside_app]
r:150 [in mathcomp.field.closed_field]
R:151 [in mathcomp.ssreflect.finfun]
R:151 [in mathcomp.algebra.ssrnum]
R:1515 [in mathcomp.algebra.ssralg]
R:152 [in mathcomp.fingroup.morphism]
R:1523 [in mathcomp.algebra.ssralg]
R:1527 [in mathcomp.algebra.ssralg]
R:153 [in mathcomp.fingroup.morphism]
R:1531 [in mathcomp.algebra.ssralg]
R:1535 [in mathcomp.algebra.ssralg]
r:154 [in mathcomp.algebra.ssralg]
R:1540 [in mathcomp.algebra.ssralg]
R:1544 [in mathcomp.algebra.ssralg]
R:1548 [in mathcomp.algebra.ssralg]
R:155 [in mathcomp.field.algebraics_fundamentals]
R:155 [in mathcomp.fingroup.morphism]
R:1553 [in mathcomp.algebra.ssralg]
R:1557 [in mathcomp.algebra.ssralg]
R:1558 [in mathcomp.algebra.mxalgebra]
R:1562 [in mathcomp.algebra.ssralg]
R:1564 [in mathcomp.algebra.ssralg]
R:1566 [in mathcomp.algebra.ssralg]
R:1568 [in mathcomp.algebra.ssralg]
r:157 [in mathcomp.field.closed_field]
R:157 [in mathcomp.algebra.ssrnum]
R:1571 [in mathcomp.algebra.ssralg]
R:1573 [in mathcomp.algebra.ssralg]
R:1575 [in mathcomp.algebra.ssralg]
R:1578 [in mathcomp.algebra.ssralg]
r:158 [in mathcomp.ssreflect.binomial]
R:1580 [in mathcomp.algebra.ssralg]
R:1583 [in mathcomp.algebra.ssralg]
R:1586 [in mathcomp.algebra.ssralg]
R:1589 [in mathcomp.algebra.ssralg]
R:1592 [in mathcomp.algebra.ssralg]
R:1595 [in mathcomp.algebra.ssralg]
R:1598 [in mathcomp.algebra.ssralg]
r:16 [in mathcomp.solvable.burnside_app]
R:1601 [in mathcomp.algebra.ssralg]
R:1602 [in mathcomp.algebra.mxalgebra]
R:1605 [in mathcomp.algebra.ssralg]
R:1608 [in mathcomp.algebra.ssralg]
R:1620 [in mathcomp.algebra.ssralg]
r:1623 [in mathcomp.ssreflect.seq]
R:1624 [in mathcomp.algebra.ssralg]
R:1629 [in mathcomp.algebra.ssralg]
R:163 [in mathcomp.algebra.finalg]
R:163 [in mathcomp.fingroup.morphism]
R:1631 [in mathcomp.algebra.mxalgebra]
R:1639 [in mathcomp.algebra.ssralg]
R:164 [in mathcomp.fingroup.morphism]
R:1646 [in mathcomp.algebra.ssralg]
R:1650 [in mathcomp.algebra.ssralg]
R:1654 [in mathcomp.algebra.ssralg]
r:1657 [in mathcomp.algebra.matrix]
R:1658 [in mathcomp.algebra.ssralg]
r:166 [in mathcomp.field.closed_field]
R:1664 [in mathcomp.algebra.ssralg]
r:1668 [in mathcomp.ssreflect.seq]
R:1669 [in mathcomp.algebra.ssralg]
r:1669 [in mathcomp.ssreflect.bigop]
r:167 [in mathcomp.solvable.sylow]
r:1671 [in mathcomp.algebra.matrix]
r:1673 [in mathcomp.ssreflect.bigop]
R:1674 [in mathcomp.algebra.ssralg]
r:1675 [in mathcomp.ssreflect.order]
r:1678 [in mathcomp.ssreflect.seq]
r:1679 [in mathcomp.ssreflect.bigop]
r:1681 [in mathcomp.ssreflect.seq]
R:1681 [in mathcomp.algebra.ssralg]
r:1686 [in mathcomp.ssreflect.seq]
R:1687 [in mathcomp.algebra.ssralg]
r:1688 [in mathcomp.ssreflect.order]
r:17 [in mathcomp.fingroup.presentation]
R:170 [in mathcomp.algebra.mxpoly]
R:170 [in mathcomp.character.inertia]
R:170 [in mathcomp.algebra.ssrnum]
r:1700 [in mathcomp.ssreflect.bigop]
r:1701 [in mathcomp.ssreflect.order]
R:1705 [in mathcomp.algebra.ssralg]
r:1706 [in mathcomp.ssreflect.bigop]
r:1713 [in mathcomp.ssreflect.order]
r:1714 [in mathcomp.ssreflect.bigop]
R:1715 [in mathcomp.algebra.ssralg]
R:1715 [in mathcomp.algebra.mxalgebra]
R:1720 [in mathcomp.algebra.ssralg]
R:1721 [in mathcomp.algebra.mxalgebra]
R:1724 [in mathcomp.algebra.mxalgebra]
r:1725 [in mathcomp.ssreflect.order]
R:1725 [in mathcomp.algebra.ssralg]
R:1727 [in mathcomp.algebra.mxalgebra]
r:1728 [in mathcomp.ssreflect.bigop]
R:173 [in mathcomp.fingroup.morphism]
R:1730 [in mathcomp.algebra.ssralg]
R:1736 [in mathcomp.algebra.ssralg]
R:1737 [in mathcomp.algebra.mxalgebra]
r:1738 [in mathcomp.ssreflect.bigop]
r:174 [in mathcomp.field.galois]
r:174 [in mathcomp.fingroup.fingroup]
r:1740 [in mathcomp.ssreflect.order]
R:1741 [in mathcomp.algebra.ssralg]
R:1743 [in mathcomp.algebra.mxalgebra]
R:1746 [in mathcomp.algebra.ssralg]
R:1748 [in mathcomp.algebra.mxalgebra]
r:1749 [in mathcomp.ssreflect.bigop]
r:175 [in mathcomp.ssreflect.generic_quotient]
R:1751 [in mathcomp.algebra.mxalgebra]
R:1752 [in mathcomp.algebra.ssralg]
r:1755 [in mathcomp.ssreflect.order]
R:1755 [in mathcomp.algebra.mxalgebra]
R:1757 [in mathcomp.algebra.ssralg]
R:1759 [in mathcomp.algebra.mxalgebra]
r:1760 [in mathcomp.ssreflect.bigop]
R:1764 [in mathcomp.algebra.mxalgebra]
R:1767 [in mathcomp.algebra.mxalgebra]
r:1768 [in mathcomp.ssreflect.order]
r:177 [in mathcomp.algebra.polydiv]
r:1770 [in mathcomp.algebra.ssralg]
r:1771 [in mathcomp.ssreflect.bigop]
R:1776 [in mathcomp.algebra.mxalgebra]
r:178 [in mathcomp.field.closed_field]
r:18 [in mathcomp.ssreflect.div]
r:18 [in mathcomp.algebra.mxpoly]
r:18 [in mathcomp.solvable.burnside_app]
r:1810 [in mathcomp.algebra.ssralg]
R:182 [in mathcomp.ssreflect.binomial]
R:183 [in mathcomp.algebra.mxpoly]
r:183 [in mathcomp.field.closed_field]
r:184 [in mathcomp.ssreflect.generic_quotient]
R:185 [in mathcomp.algebra.ssrnum]
r:186 [in mathcomp.character.character]
r:1865 [in mathcomp.algebra.matrix]
R:187 [in mathcomp.ssreflect.finfun]
r:1870 [in mathcomp.algebra.matrix]
r:1872 [in mathcomp.algebra.matrix]
r:1874 [in mathcomp.algebra.matrix]
r:1877 [in mathcomp.algebra.matrix]
R:188 [in mathcomp.ssreflect.finfun]
r:188 [in mathcomp.ssreflect.prime]
r:1880 [in mathcomp.algebra.matrix]
r:1883 [in mathcomp.algebra.matrix]
r:1886 [in mathcomp.algebra.matrix]
R:189 [in mathcomp.algebra.mxpoly]
r:1891 [in mathcomp.algebra.matrix]
r:1895 [in mathcomp.algebra.matrix]
r:1897 [in mathcomp.algebra.matrix]
r:19 [in mathcomp.solvable.burnside_app]
r:1900 [in mathcomp.algebra.matrix]
r:1903 [in mathcomp.algebra.matrix]
r:1905 [in mathcomp.algebra.matrix]
R:192 [in mathcomp.solvable.cyclic]
r:1926 [in mathcomp.algebra.ssralg]
r:1931 [in mathcomp.algebra.ssralg]
r:1935 [in mathcomp.algebra.ssralg]
R:194 [in mathcomp.algebra.mxpoly]
R:194 [in mathcomp.fingroup.morphism]
R:195 [in mathcomp.fingroup.morphism]
r:1955 [in mathcomp.algebra.ssralg]
r:1959 [in mathcomp.algebra.ssralg]
R:197 [in mathcomp.fingroup.morphism]
r:199 [in mathcomp.character.classfun]
R:199 [in mathcomp.fingroup.morphism]
r:1990 [in mathcomp.ssreflect.bigop]
r:1991 [in mathcomp.ssreflect.bigop]
r:1992 [in mathcomp.ssreflect.bigop]
r:1999 [in mathcomp.ssreflect.bigop]
r:2 [in mathcomp.ssreflect.prime]
r:200 [in mathcomp.field.separable]
R:202 [in mathcomp.algebra.ring_quotient]
r:202 [in mathcomp.algebra.ssrint]
r:202 [in mathcomp.solvable.nilpotent]
R:203 [in mathcomp.algebra.ssralg]
R:204 [in mathcomp.algebra.mxpoly]
R:205 [in mathcomp.fingroup.morphism]
r:2050 [in mathcomp.ssreflect.bigop]
R:2053 [in mathcomp.algebra.ssralg]
R:2056 [in mathcomp.algebra.ssralg]
R:206 [in mathcomp.algebra.ring_quotient]
r:2061 [in mathcomp.ssreflect.bigop]
R:2069 [in mathcomp.algebra.matrix]
R:207 [in mathcomp.fingroup.morphism]
R:207 [in mathcomp.algebra.ssralg]
r:2072 [in mathcomp.ssreflect.bigop]
R:2078 [in mathcomp.algebra.matrix]
R:208 [in mathcomp.algebra.mxpoly]
R:2080 [in mathcomp.algebra.matrix]
R:2083 [in mathcomp.algebra.matrix]
r:2083 [in mathcomp.algebra.ssralg]
R:2085 [in mathcomp.algebra.matrix]
R:2091 [in mathcomp.ssreflect.seq]
r:2093 [in mathcomp.ssreflect.bigop]
R:21 [in mathcomp.algebra.mxpoly]
R:210 [in mathcomp.algebra.ring_quotient]
r:2100 [in mathcomp.algebra.ssralg]
r:2103 [in mathcomp.ssreflect.bigop]
r:2104 [in mathcomp.algebra.matrix]
R:211 [in mathcomp.fingroup.morphism]
r:2113 [in mathcomp.algebra.matrix]
r:2117 [in mathcomp.ssreflect.bigop]
r:212 [in mathcomp.field.separable]
R:212 [in mathcomp.algebra.mxpoly]
R:212 [in mathcomp.fingroup.morphism]
R:2124 [in mathcomp.ssreflect.seq]
R:2129 [in mathcomp.algebra.matrix]
r:213 [in mathcomp.algebra.ssrint]
r:2131 [in mathcomp.ssreflect.bigop]
R:2133 [in mathcomp.algebra.ssralg]
R:2135 [in mathcomp.algebra.ssralg]
R:2136 [in mathcomp.algebra.ssralg]
r:214 [in mathcomp.solvable.nilpotent]
R:215 [in mathcomp.algebra.ring_quotient]
R:215 [in mathcomp.solvable.maximal]
r:216 [in mathcomp.character.mxrepresentation]
R:216 [in mathcomp.algebra.ssralg]
R:217 [in mathcomp.algebra.ring_quotient]
R:217 [in mathcomp.solvable.maximal]
R:2173 [in mathcomp.algebra.matrix]
r:2175 [in mathcomp.ssreflect.bigop]
r:2183 [in mathcomp.algebra.ssralg]
R:219 [in mathcomp.algebra.ring_quotient]
r:2193 [in mathcomp.algebra.ssralg]
r:22 [in mathcomp.fingroup.presentation]
r:2218 [in mathcomp.ssreflect.order]
r:2226 [in mathcomp.ssreflect.order]
R:223 [in mathcomp.algebra.ring_quotient]
r:2235 [in mathcomp.algebra.ssralg]
R:224 [in mathcomp.fingroup.morphism]
r:2250 [in mathcomp.ssreflect.order]
r:2259 [in mathcomp.ssreflect.order]
r:226 [in mathcomp.algebra.polydiv]
R:227 [in mathcomp.algebra.ring_quotient]
r:228 [in mathcomp.algebra.polydiv]
r:228 [in mathcomp.field.fieldext]
r:228 [in mathcomp.character.mxrepresentation]
r:228 [in mathcomp.fingroup.gproduct]
R:2288 [in mathcomp.algebra.ssralg]
r:229 [in mathcomp.algebra.vector]
R:2292 [in mathcomp.algebra.ssralg]
r:230 [in mathcomp.field.fieldext]
R:2300 [in mathcomp.ssreflect.seq]
r:2309 [in mathcomp.ssreflect.order]
R:231 [in mathcomp.algebra.ssrnum]
R:231 [in mathcomp.algebra.ssralg]
R:231 [in mathcomp.ssreflect.bigop]
R:232 [in mathcomp.algebra.ssralg]
r:233 [in mathcomp.algebra.polydiv]
R:233 [in mathcomp.character.classfun]
R:233 [in mathcomp.algebra.ssrnum]
R:233 [in mathcomp.algebra.ssralg]
r:2330 [in mathcomp.ssreflect.order]
r:2338 [in mathcomp.ssreflect.order]
r:235 [in mathcomp.field.galois]
R:236 [in mathcomp.algebra.ssralg]
R:236 [in mathcomp.solvable.maximal]
r:2362 [in mathcomp.ssreflect.order]
R:2365 [in mathcomp.algebra.ssralg]
r:237 [in mathcomp.ssreflect.bigop]
r:2371 [in mathcomp.ssreflect.order]
R:238 [in mathcomp.algebra.ssrnum]
r:239 [in mathcomp.fingroup.gproduct]
R:239 [in mathcomp.algebra.ssralg]
R:2396 [in mathcomp.algebra.matrix]
R:24 [in mathcomp.field.finfield]
r:240 [in mathcomp.algebra.mxpoly]
R:240 [in mathcomp.algebra.ssrnum]
R:240 [in mathcomp.solvable.maximal]
r:241 [in mathcomp.algebra.mxpoly]
R:241 [in mathcomp.algebra.ssralg]
r:242 [in mathcomp.algebra.mxpoly]
r:2421 [in mathcomp.ssreflect.order]
R:2429 [in mathcomp.algebra.matrix]
r:2434 [in mathcomp.ssreflect.seq]
R:2434 [in mathcomp.algebra.matrix]
R:2439 [in mathcomp.algebra.matrix]
r:2442 [in mathcomp.ssreflect.seq]
R:2449 [in mathcomp.algebra.ssralg]
r:2452 [in mathcomp.ssreflect.seq]
r:2458 [in mathcomp.ssreflect.seq]
R:2458 [in mathcomp.algebra.ssralg]
r:2462 [in mathcomp.ssreflect.seq]
R:2465 [in mathcomp.algebra.ssralg]
r:2470 [in mathcomp.ssreflect.seq]
r:2478 [in mathcomp.ssreflect.seq]
r:2485 [in mathcomp.ssreflect.seq]
r:2496 [in mathcomp.ssreflect.seq]
R:2499 [in mathcomp.algebra.ssralg]
R:25 [in mathcomp.algebra.finalg]
R:2511 [in mathcomp.algebra.ssralg]
R:2513 [in mathcomp.algebra.ssralg]
R:2515 [in mathcomp.algebra.ssralg]
R:2517 [in mathcomp.algebra.ssralg]
r:2536 [in mathcomp.ssreflect.seq]
r:2540 [in mathcomp.ssreflect.seq]
r:2545 [in mathcomp.ssreflect.seq]
r:2549 [in mathcomp.ssreflect.seq]
r:2554 [in mathcomp.ssreflect.seq]
r:2557 [in mathcomp.ssreflect.seq]
R:2566 [in mathcomp.algebra.matrix]
R:257 [in mathcomp.algebra.ssralg]
R:2572 [in mathcomp.algebra.ssrnum]
R:2574 [in mathcomp.algebra.ssrnum]
r:2589 [in mathcomp.algebra.matrix]
R:259 [in mathcomp.algebra.ssralg]
R:2592 [in mathcomp.algebra.matrix]
R:26 [in mathcomp.algebra.countalg]
R:26 [in mathcomp.algebra.zmodp]
r:261 [in mathcomp.ssreflect.bigop]
R:262 [in mathcomp.fingroup.quotient]
R:2621 [in mathcomp.algebra.ssrnum]
r:2622 [in mathcomp.ssreflect.order]
R:2623 [in mathcomp.algebra.ssrnum]
r:2632 [in mathcomp.ssreflect.order]
r:265 [in mathcomp.field.closed_field]
r:27 [in mathcomp.fingroup.presentation]
r:270 [in mathcomp.algebra.ssralg]
R:271 [in mathcomp.algebra.interval]
R:2716 [in mathcomp.algebra.ssralg]
r:2716 [in mathcomp.ssreflect.bigop]
r:272 [in mathcomp.field.fieldext]
r:2729 [in mathcomp.ssreflect.bigop]
r:273 [in mathcomp.solvable.extremal]
r:274 [in mathcomp.fingroup.gproduct]
r:2746 [in mathcomp.ssreflect.bigop]
r:2764 [in mathcomp.ssreflect.bigop]
R:277 [in mathcomp.fingroup.morphism]
r:2775 [in mathcomp.ssreflect.bigop]
r:28 [in mathcomp.field.separable]
R:280 [in mathcomp.fingroup.morphism]
r:281 [in mathcomp.algebra.ssralg]
r:284 [in mathcomp.algebra.ssrnum]
R:284 [in mathcomp.fingroup.morphism]
r:288 [in mathcomp.character.classfun]
r:288 [in mathcomp.ssreflect.bigop]
r:293 [in mathcomp.algebra.mxalgebra]
R:2936 [in mathcomp.ssreflect.bigop]
r:2972 [in mathcomp.ssreflect.bigop]
r:2978 [in mathcomp.ssreflect.bigop]
r:298 [in mathcomp.algebra.ssrint]
R:2981 [in mathcomp.algebra.matrix]
R:30 [in mathcomp.algebra.countalg]
r:3027 [in mathcomp.ssreflect.bigop]
r:305 [in mathcomp.character.classfun]
r:3052 [in mathcomp.ssreflect.bigop]
r:3064 [in mathcomp.ssreflect.bigop]
R:3068 [in mathcomp.algebra.matrix]
r:307 [in mathcomp.algebra.poly]
r:308 [in mathcomp.algebra.ssrint]
r:3088 [in mathcomp.ssreflect.bigop]
r:3100 [in mathcomp.ssreflect.bigop]
r:3108 [in mathcomp.ssreflect.bigop]
r:3116 [in mathcomp.ssreflect.bigop]
r:314 [in mathcomp.ssreflect.bigop]
r:3145 [in mathcomp.ssreflect.bigop]
r:315 [in mathcomp.solvable.abelian]
r:3162 [in mathcomp.ssreflect.bigop]
R:3170 [in mathcomp.algebra.matrix]
R:32 [in mathcomp.field.falgebra]
r:3205 [in mathcomp.ssreflect.bigop]
R:3227 [in mathcomp.algebra.matrix]
r:3230 [in mathcomp.algebra.matrix]
R:33 [in mathcomp.algebra.zmodp]
R:33 [in mathcomp.algebra.vector]
R:333 [in mathcomp.solvable.extremal]
r:334 [in mathcomp.ssreflect.bigop]
R:3383 [in mathcomp.algebra.matrix]
R:34 [in mathcomp.fingroup.morphism]
R:3417 [in mathcomp.algebra.matrix]
R:3428 [in mathcomp.algebra.matrix]
r:343 [in mathcomp.character.character]
R:3443 [in mathcomp.algebra.matrix]
R:3458 [in mathcomp.algebra.matrix]
R:3464 [in mathcomp.algebra.matrix]
r:352 [in mathcomp.field.fieldext]
r:353 [in mathcomp.ssreflect.bigop]
r:354 [in mathcomp.algebra.polydiv]
r:356 [in mathcomp.ssreflect.tuple]
r:357 [in mathcomp.algebra.polydiv]
r:358 [in mathcomp.ssreflect.tuple]
R:36 [in mathcomp.algebra.countalg]
R:36 [in mathcomp.field.separable]
R:360 [in mathcomp.algebra.ssrnum]
r:365 [in mathcomp.fingroup.gproduct]
R:37 [in mathcomp.algebra.matrix]
R:37 [in mathcomp.algebra.polyXY]
r:370 [in mathcomp.ssreflect.bigop]
r:376 [in mathcomp.fingroup.gproduct]
R:380 [in mathcomp.algebra.mxpoly]
r:382 [in mathcomp.algebra.poly]
r:383 [in mathcomp.ssreflect.bigop]
r:384 [in mathcomp.character.classfun]
R:386 [in mathcomp.algebra.mxpoly]
r:387 [in mathcomp.fingroup.gproduct]
R:393 [in mathcomp.fingroup.morphism]
r:393 [in mathcomp.character.character]
r:394 [in mathcomp.algebra.vector]
r:395 [in mathcomp.ssreflect.bigop]
R:396 [in mathcomp.fingroup.morphism]
R:399 [in mathcomp.field.closed_field]
R:40 [in mathcomp.algebra.countalg]
R:40 [in mathcomp.algebra.matrix]
R:40 [in mathcomp.algebra.finalg]
R:403 [in mathcomp.field.closed_field]
r:41 [in mathcomp.fingroup.morphism]
r:413 [in mathcomp.ssreflect.bigop]
r:415 [in mathcomp.algebra.mxpoly]
r:417 [in mathcomp.character.classfun]
r:418 [in mathcomp.algebra.intdiv]
r:418 [in mathcomp.field.galois]
r:426 [in mathcomp.fingroup.gproduct]
R:43 [in mathcomp.algebra.matrix]
r:432 [in mathcomp.ssreflect.bigop]
r:433 [in mathcomp.algebra.polydiv]
r:435 [in mathcomp.algebra.intdiv]
r:436 [in mathcomp.algebra.polydiv]
r:436 [in mathcomp.algebra.poly]
r:437 [in mathcomp.fingroup.gproduct]
r:439 [in mathcomp.algebra.polydiv]
R:44 [in mathcomp.algebra.finalg]
r:44 [in mathcomp.algebra.vector]
R:441 [in mathcomp.algebra.intdiv]
R:442 [in mathcomp.algebra.intdiv]
r:442 [in mathcomp.ssreflect.bigop]
r:444 [in mathcomp.algebra.polydiv]
r:446 [in mathcomp.algebra.mxpoly]
r:447 [in mathcomp.algebra.mxpoly]
r:45 [in mathcomp.algebra.rat]
r:45 [in mathcomp.algebra.vector]
r:450 [in mathcomp.field.galois]
r:450 [in mathcomp.algebra.ssrnum]
r:451 [in mathcomp.field.galois]
R:455 [in mathcomp.algebra.mxpoly]
r:455 [in mathcomp.ssreflect.bigop]
r:458 [in mathcomp.algebra.ssralg]
r:459 [in mathcomp.algebra.ssrnum]
r:459 [in mathcomp.ssreflect.bigop]
R:46 [in mathcomp.algebra.countalg]
R:46 [in mathcomp.algebra.matrix]
R:46 [in mathcomp.algebra.finalg]
R:460 [in mathcomp.algebra.mxpoly]
R:462 [in mathcomp.fingroup.action]
R:465 [in mathcomp.fingroup.action]
r:467 [in mathcomp.field.galois]
R:467 [in mathcomp.algebra.mxpoly]
r:468 [in mathcomp.ssreflect.bigop]
r:469 [in mathcomp.algebra.mxpoly]
R:469 [in mathcomp.character.classfun]
R:47 [in mathcomp.algebra.mxpoly]
r:471 [in mathcomp.fingroup.fingroup]
r:472 [in mathcomp.field.galois]
R:472 [in mathcomp.character.character]
R:474 [in mathcomp.character.classfun]
r:478 [in mathcomp.ssreflect.bigop]
R:48 [in mathcomp.field.finfield]
R:483 [in mathcomp.algebra.ssrint]
r:485 [in mathcomp.fingroup.fingroup]
r:488 [in mathcomp.ssreflect.bigop]
R:49 [in mathcomp.algebra.matrix]
R:490 [in mathcomp.character.classfun]
r:497 [in mathcomp.character.mxrepresentation]
r:498 [in mathcomp.field.galois]
r:498 [in mathcomp.ssreflect.bigop]
r:499 [in mathcomp.field.galois]
r:5 [in mathcomp.ssreflect.choice]
r:5 [in mathcomp.character.mxrepresentation]
R:50 [in mathcomp.algebra.countalg]
R:50 [in mathcomp.field.finfield]
r:501 [in mathcomp.fingroup.gproduct]
r:506 [in mathcomp.algebra.polydiv]
R:509 [in mathcomp.character.classfun]
r:509 [in mathcomp.algebra.ssralg]
r:509 [in mathcomp.ssreflect.bigop]
r:51 [in mathcomp.field.cyclotomic]
r:51 [in mathcomp.field.separable]
R:512 [in mathcomp.character.classfun]
r:512 [in mathcomp.fingroup.gproduct]
R:514 [in mathcomp.character.classfun]
R:518 [in mathcomp.character.classfun]
r:52 [in mathcomp.field.separable]
R:52 [in mathcomp.algebra.matrix]
R:52 [in mathcomp.field.finfield]
R:520 [in mathcomp.character.classfun]
r:525 [in mathcomp.field.galois]
R:531 [in mathcomp.character.classfun]
R:533 [in mathcomp.character.classfun]
r:538 [in mathcomp.algebra.polydiv]
r:539 [in mathcomp.algebra.polydiv]
R:54 [in mathcomp.field.finfield]
R:54 [in mathcomp.ssreflect.bigop]
r:540 [in mathcomp.algebra.mxpoly]
r:540 [in mathcomp.ssreflect.bigop]
r:55 [in mathcomp.field.separable]
R:55 [in mathcomp.algebra.matrix]
r:550 [in mathcomp.character.character]
R:551 [in mathcomp.ssreflect.finset]
r:552 [in mathcomp.ssreflect.bigop]
r:553 [in mathcomp.algebra.mxpoly]
r:556 [in mathcomp.character.character]
r:558 [in mathcomp.algebra.mxpoly]
R:56 [in mathcomp.algebra.countalg]
R:56 [in mathcomp.field.finfield]
r:562 [in mathcomp.ssreflect.bigop]
r:567 [in mathcomp.ssreflect.prime]
r:571 [in mathcomp.ssreflect.bigop]
r:575 [in mathcomp.algebra.mxpoly]
r:576 [in mathcomp.algebra.mxpoly]
r:577 [in mathcomp.algebra.mxpoly]
r:577 [in mathcomp.ssreflect.bigop]
R:58 [in mathcomp.algebra.matrix]
R:58 [in mathcomp.ssreflect.bigop]
r:582 [in mathcomp.ssreflect.bigop]
R:584 [in mathcomp.algebra.ssrint]
r:585 [in mathcomp.algebra.polydiv]
r:588 [in mathcomp.algebra.polydiv]
r:597 [in mathcomp.algebra.polydiv]
R:6 [in mathcomp.algebra.poly]
R:60 [in mathcomp.algebra.countalg]
r:600 [in mathcomp.algebra.polydiv]
R:602 [in mathcomp.solvable.pgroup]
R:61 [in mathcomp.algebra.matrix]
R:615 [in mathcomp.algebra.ssralg]
R:62 [in mathcomp.algebra.countalg]
R:62 [in mathcomp.algebra.finalg]
r:624 [in mathcomp.ssreflect.bigop]
r:626 [in mathcomp.fingroup.fingroup]
R:63 [in mathcomp.field.finfield]
R:63 [in mathcomp.ssreflect.bigop]
r:633 [in mathcomp.ssreflect.bigop]
r:64 [in mathcomp.field.cyclotomic]
R:64 [in mathcomp.algebra.matrix]
r:643 [in mathcomp.ssreflect.bigop]
R:645 [in mathcomp.algebra.ssralg]
r:646 [in mathcomp.algebra.polydiv]
r:648 [in mathcomp.algebra.ssrnum]
r:649 [in mathcomp.algebra.polydiv]
r:65 [in mathcomp.field.cyclotomic]
R:65 [in mathcomp.field.finfield]
r:652 [in mathcomp.ssreflect.bigop]
r:656 [in mathcomp.algebra.ssrnum]
r:66 [in mathcomp.field.cyclotomic]
R:66 [in mathcomp.algebra.finalg]
R:66 [in mathcomp.fingroup.morphism]
r:66 [in mathcomp.ssreflect.bigop]
r:667 [in mathcomp.algebra.polydiv]
r:669 [in mathcomp.algebra.polydiv]
R:67 [in mathcomp.field.cyclotomic]
R:67 [in mathcomp.field.finfield]
r:673 [in mathcomp.algebra.polydiv]
r:676 [in mathcomp.algebra.polydiv]
R:677 [in mathcomp.solvable.abelian]
r:679 [in mathcomp.algebra.ssrnum]
R:68 [in mathcomp.algebra.countalg]
R:68 [in mathcomp.algebra.finalg]
R:68 [in mathcomp.ssreflect.bigop]
R:682 [in mathcomp.solvable.abelian]
r:688 [in mathcomp.algebra.ssralg]
R:69 [in mathcomp.field.finfield]
R:69 [in mathcomp.fingroup.morphism]
r:69 [in mathcomp.solvable.center]
r:696 [in mathcomp.algebra.ssrnum]
r:699 [in mathcomp.algebra.ssralg]
r:7 [in mathcomp.algebra.polydiv]
R:7 [in mathcomp.algebra.poly]
R:70 [in mathcomp.algebra.ssrnum]
R:70 [in mathcomp.fingroup.morphism]
r:71 [in mathcomp.character.mxabelem]
R:71 [in mathcomp.field.finfield]
r:712 [in mathcomp.algebra.polydiv]
R:714 [in mathcomp.algebra.ssralg]
R:715 [in mathcomp.ssreflect.finset]
r:716 [in mathcomp.algebra.vector]
R:72 [in mathcomp.algebra.countalg]
R:72 [in mathcomp.algebra.ssrnum]
R:720 [in mathcomp.character.classfun]
R:726 [in mathcomp.algebra.ssralg]
R:73 [in mathcomp.field.finfield]
r:730 [in mathcomp.algebra.polydiv]
r:733 [in mathcomp.algebra.polydiv]
r:736 [in mathcomp.algebra.polydiv]
R:739 [in mathcomp.algebra.poly]
R:74 [in mathcomp.algebra.finalg]
R:74 [in mathcomp.fingroup.morphism]
R:740 [in mathcomp.algebra.poly]
r:741 [in mathcomp.algebra.polydiv]
R:741 [in mathcomp.algebra.poly]
R:742 [in mathcomp.algebra.poly]
R:744 [in mathcomp.algebra.ssralg]
r:749 [in mathcomp.algebra.matrix]
R:75 [in mathcomp.ssreflect.ssrAC]
R:758 [in mathcomp.algebra.ssrint]
r:76 [in mathcomp.character.classfun]
r:760 [in mathcomp.algebra.polydiv]
R:762 [in mathcomp.algebra.ssrint]
r:763 [in mathcomp.algebra.matrix]
r:774 [in mathcomp.algebra.matrix]
R:78 [in mathcomp.algebra.countalg]
R:78 [in mathcomp.algebra.finalg]
r:783 [in mathcomp.algebra.mxpoly]
r:784 [in mathcomp.algebra.matrix]
r:784 [in mathcomp.algebra.mxpoly]
r:785 [in mathcomp.algebra.mxpoly]
r:79 [in mathcomp.solvable.nilpotent]
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:8 [in mathcomp.algebra.poly]
R:80 [in mathcomp.ssreflect.ssrAC]
R:80 [in mathcomp.algebra.finalg]
R:80 [in mathcomp.fingroup.morphism]
r:802 [in mathcomp.algebra.polydiv]
r:809 [in mathcomp.algebra.vector]
R:82 [in mathcomp.algebra.countalg]
R:82 [in mathcomp.fingroup.morphism]
r:823 [in mathcomp.algebra.vector]
r:826 [in mathcomp.algebra.mxalgebra]
r:827 [in mathcomp.algebra.polydiv]
r:828 [in mathcomp.algebra.mxalgebra]
r:829 [in mathcomp.algebra.polydiv]
r:829 [in mathcomp.algebra.ssralg]
r:831 [in mathcomp.algebra.polydiv]
r:833 [in mathcomp.ssreflect.bigop]
R:84 [in mathcomp.fingroup.morphism]
r:84 [in mathcomp.solvable.center]
r:843 [in mathcomp.algebra.poly]
r:845 [in mathcomp.algebra.mxpoly]
r:845 [in mathcomp.ssreflect.bigop]
r:846 [in mathcomp.algebra.mxpoly]
r:846 [in mathcomp.algebra.poly]
r:847 [in mathcomp.algebra.mxpoly]
r:849 [in mathcomp.algebra.mxpoly]
r:850 [in mathcomp.algebra.mxpoly]
r:851 [in mathcomp.algebra.mxpoly]
r:856 [in mathcomp.ssreflect.bigop]
R:857 [in mathcomp.algebra.ssrint]
r:859 [in mathcomp.algebra.polydiv]
R:862 [in mathcomp.algebra.ssrint]
R:869 [in mathcomp.algebra.ssrint]
R:87 [in mathcomp.solvable.pgroup]
R:87 [in mathcomp.solvable.hall]
R:871 [in mathcomp.character.classfun]
r:874 [in mathcomp.algebra.polydiv]
R:874 [in mathcomp.algebra.matrix]
R:875 [in mathcomp.algebra.ssrint]
r:878 [in mathcomp.algebra.polydiv]
R:88 [in mathcomp.algebra.countalg]
R:88 [in mathcomp.fingroup.morphism]
r:882 [in mathcomp.algebra.polydiv]
r:89 [in mathcomp.algebra.polydiv]
R:896 [in mathcomp.algebra.matrix]
r:90 [in mathcomp.character.inertia]
R:909 [in mathcomp.ssreflect.finset]
r:91 [in mathcomp.solvable.nilpotent]
r:914 [in mathcomp.algebra.ssralg]
R:92 [in mathcomp.algebra.countalg]
R:92 [in mathcomp.algebra.ssrnum]
r:929 [in mathcomp.algebra.polydiv]
R:93 [in mathcomp.fingroup.morphism]
R:931 [in mathcomp.ssreflect.seq]
r:931 [in mathcomp.algebra.ssralg]
r:932 [in mathcomp.algebra.polydiv]
r:933 [in mathcomp.algebra.poly]
r:936 [in mathcomp.algebra.ssrnum]
r:943 [in mathcomp.ssreflect.ssrnat]
r:944 [in mathcomp.algebra.ssrnum]
r:949 [in mathcomp.algebra.polydiv]
R:951 [in mathcomp.ssreflect.bigop]
r:952 [in mathcomp.algebra.polydiv]
r:952 [in mathcomp.algebra.ssrnum]
R:953 [in mathcomp.algebra.matrix]
r:955 [in mathcomp.algebra.polydiv]
r:956 [in mathcomp.ssreflect.ssrnat]
R:96 [in mathcomp.algebra.ssrnum]
R:960 [in mathcomp.algebra.ssralg]
r:965 [in mathcomp.algebra.ssrnum]
R:966 [in mathcomp.algebra.ssralg]
r:967 [in mathcomp.ssreflect.ssrnat]
R:967 [in mathcomp.algebra.ssralg]
R:969 [in mathcomp.ssreflect.finset]
R:97 [in mathcomp.fingroup.morphism]
r:971 [in mathcomp.ssreflect.bigop]
r:976 [in mathcomp.algebra.vector]
r:978 [in mathcomp.algebra.poly]
R:98 [in mathcomp.algebra.countalg]
r:981 [in mathcomp.ssreflect.ssrnat]
r:987 [in mathcomp.algebra.polydiv]
| 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 | (78577 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 | (1807 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 | (48032 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 | (375 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 | (3995 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 | (14468 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 | (223 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 | (45 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 | (133 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 | (451 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 | (1387 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 | (1144 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 | (6179 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 | (247 entries) |