mathcomp.ssreflect.tuple

Global Index

_

(76754 entries)

Notation Index

H

J

T

W

X

Y

_

(1892 entries)

Binder Index

_

other

(49588 entries)

Module Index

H

J

K

L

W

X

Y

_

other

(305 entries)

Variable Index

J

W

X

Y

_

other

(4034 entries)

Library Index

K

L

U

W

X

Y

_

other

(94 entries)

Lemma Index

Y

_

other

(14802 entries)

Constructor Index

J

K

W

Y

_

other

(222 entries)

Axiom Index

B

C

D

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(131 entries)

Projection Index

D

H

I

J

K

L

N

O

Q

U

W

X

Y

Z

_

other

(43 entries)

Section Index

J

W

X

Y

_

other

(1392 entries)

Abbreviation Index

Y

_

other

(1140 entries)

Definition Index

Y

_

other

(3066 entries)

Record Index

D

F

H

I

J

K

L

O

Q

U

W

X

Y

Z

_

other

(36 entries)

P (binder)

parse_pos:36 [in mathcomp.algebra.rat]
parse:42 [in mathcomp.algebra.rat]
pat:104 [in mathcomp.algebra.rat]
pat:107 [in mathcomp.algebra.rat]
pat:115 [in mathcomp.algebra.rat]
pat:134 [in mathcomp.algebra.rat]
pat:137 [in mathcomp.algebra.rat]
pat:145 [in mathcomp.algebra.rat]
pat:19 [in mathcomp.algebra.interval]
pat:195 [in mathcomp.algebra.rat]
pat:197 [in mathcomp.algebra.rat]
pat:199 [in mathcomp.algebra.rat]
pat:201 [in mathcomp.algebra.rat]
pat:203 [in mathcomp.algebra.rat]
pat:22 [in mathcomp.algebra.interval]
pat:23 [in mathcomp.algebra.rat]
pat:65 [in mathcomp.algebra.rat]
pat:76 [in mathcomp.algebra.qpoly]
pat:77 [in mathcomp.algebra.qpoly]
pat:78 [in mathcomp.algebra.qpoly]
pA:187 [in mathcomp.ssreflect.finset]
pA:191 [in mathcomp.ssreflect.finset]
pA:228 [in mathcomp.ssreflect.fintype]
pA:26 [in mathcomp.ssreflect.finset]
pA:340 [in mathcomp.ssreflect.finset]
pA:344 [in mathcomp.ssreflect.finset]
pA:349 [in mathcomp.ssreflect.finset]
pA:35 [in mathcomp.ssreflect.finset]
pB:188 [in mathcomp.ssreflect.finset]
pB:192 [in mathcomp.ssreflect.finset]
pB:196 [in mathcomp.ssreflect.finset]
pB:36 [in mathcomp.ssreflect.finset]
pC:193 [in mathcomp.ssreflect.finset]
pd_ok:92 [in mathcomp.ssreflect.prime]
pd_ord:88 [in mathcomp.ssreflect.prime]
pd_val:79 [in mathcomp.ssreflect.prime]
pd:45 [in mathcomp.ssreflect.prime]
pd:75 [in mathcomp.ssreflect.prime]
pd:87 [in mathcomp.ssreflect.prime]
pd:91 [in mathcomp.ssreflect.prime]
perms_rec:2688 [in mathcomp.ssreflect.seq]
perms:2714 [in mathcomp.ssreflect.seq]
pEx:102 [in mathcomp.algebra.polyXY]
pEx:109 [in mathcomp.algebra.polyXY]
pfunF0:58 [in mathcomp.solvable.gfunctor]
pfunF:60 [in mathcomp.solvable.gfunctor]
pf_ok:85 [in mathcomp.ssreflect.prime]
pf:20 [in mathcomp.field.closed_field]
pf:55 [in mathcomp.field.closed_field]
phAB:1201 [in mathcomp.algebra.ssralg]
phi_i:378 [in mathcomp.character.vcharacter]
phi1:360 [in mathcomp.character.classfun]
phi1:399 [in mathcomp.character.vcharacter]
phi1:414 [in mathcomp.character.vcharacter]
phi1:494 [in mathcomp.character.classfun]
phi1:770 [in mathcomp.character.classfun]
phi2:361 [in mathcomp.character.classfun]
phi2:400 [in mathcomp.character.vcharacter]
phi2:415 [in mathcomp.character.vcharacter]
phi2:495 [in mathcomp.character.classfun]
phi2:771 [in mathcomp.character.classfun]
phi:10 [in mathcomp.solvable.gfunctor]
phi:100 [in mathcomp.character.inertia]
phi:100 [in mathcomp.character.classfun]
phi:1000 [in mathcomp.character.character]
phi:1001 [in mathcomp.character.character]
phi:1004 [in mathcomp.character.classfun]
phi:1006 [in mathcomp.character.classfun]
phi:1008 [in mathcomp.character.classfun]
phi:1009 [in mathcomp.character.classfun]
phi:101 [in mathcomp.character.inertia]
phi:1010 [in mathcomp.character.classfun]
phi:1011 [in mathcomp.character.character]
phi:1013 [in mathcomp.character.classfun]
phi:1013 [in mathcomp.character.character]
phi:1014 [in mathcomp.character.classfun]
phi:1016 [in mathcomp.character.classfun]
phi:1017 [in mathcomp.character.classfun]
phi:1017 [in mathcomp.character.character]
phi:102 [in mathcomp.character.inertia]
phi:1020 [in mathcomp.character.classfun]
phi:1021 [in mathcomp.character.classfun]
phi:1023 [in mathcomp.character.character]
phi:1025 [in mathcomp.character.classfun]
phi:1027 [in mathcomp.character.classfun]
phi:103 [in mathcomp.character.classfun]
phi:1030 [in mathcomp.character.character]
phi:1034 [in mathcomp.character.character]
phi:1037 [in mathcomp.character.character]
phi:1045 [in mathcomp.character.character]
phi:1051 [in mathcomp.character.character]
phi:1052 [in mathcomp.character.character]
phi:1053 [in mathcomp.character.character]
Phi:107 [in mathcomp.character.inertia]
phi:1074 [in mathcomp.character.character]
phi:108 [in mathcomp.character.classfun]
phi:1095 [in mathcomp.character.character]
phi:11 [in mathcomp.character.inertia]
phi:110 [in mathcomp.character.classfun]
phi:111 [in mathcomp.character.classfun]
phi:114 [in mathcomp.character.classfun]
phi:116 [in mathcomp.character.classfun]
phi:118 [in mathcomp.character.vcharacter]
phi:119 [in mathcomp.character.inertia]
phi:120 [in mathcomp.character.vcharacter]
phi:122 [in mathcomp.character.vcharacter]
phi:123 [in mathcomp.character.vcharacter]
phi:126 [in mathcomp.algebra.mxpoly]
phi:128 [in mathcomp.character.vcharacter]
phi:128 [in mathcomp.character.classfun]
phi:130 [in mathcomp.character.vcharacter]
phi:132 [in mathcomp.character.vcharacter]
phi:136 [in mathcomp.character.classfun]
phi:137 [in mathcomp.character.classfun]
phi:138 [in mathcomp.character.classfun]
phi:139 [in mathcomp.character.classfun]
phi:14 [in mathcomp.character.vcharacter]
phi:14 [in mathcomp.character.inertia]
phi:14 [in mathcomp.solvable.gfunctor]
phi:140 [in mathcomp.character.inertia]
phi:141 [in mathcomp.character.vcharacter]
phi:146 [in mathcomp.character.inertia]
phi:149 [in mathcomp.character.classfun]
phi:15 [in mathcomp.character.integral_char]
phi:15 [in mathcomp.character.vcharacter]
phi:150 [in mathcomp.character.inertia]
phi:151 [in mathcomp.character.inertia]
phi:152 [in mathcomp.character.inertia]
phi:154 [in mathcomp.character.inertia]
phi:156 [in mathcomp.character.inertia]
phi:156 [in mathcomp.character.classfun]
phi:157 [in mathcomp.character.inertia]
phi:159 [in mathcomp.character.classfun]
phi:16 [in mathcomp.character.inertia]
phi:168 [in mathcomp.character.classfun]
phi:17 [in mathcomp.character.vcharacter]
phi:173 [in mathcomp.character.classfun]
phi:176 [in mathcomp.character.vcharacter]
phi:180 [in mathcomp.character.classfun]
phi:182 [in mathcomp.character.classfun]
phi:183 [in mathcomp.character.classfun]
phi:186 [in mathcomp.character.classfun]
phi:188 [in mathcomp.character.vcharacter]
phi:188 [in mathcomp.character.classfun]
phi:189 [in mathcomp.field.algnum]
phi:19 [in mathcomp.character.inertia]
phi:19 [in mathcomp.solvable.gfunctor]
phi:190 [in mathcomp.character.vcharacter]
phi:194 [in mathcomp.character.classfun]
phi:195 [in mathcomp.character.inertia]
phi:201 [in mathcomp.character.inertia]
phi:201 [in mathcomp.character.classfun]
phi:203 [in mathcomp.character.inertia]
phi:205 [in mathcomp.character.inertia]
phi:206 [in mathcomp.character.inertia]
phi:208 [in mathcomp.character.inertia]
phi:209 [in mathcomp.character.classfun]
phi:210 [in mathcomp.character.inertia]
phi:22 [in mathcomp.character.inertia]
phi:221 [in mathcomp.character.vcharacter]
phi:221 [in mathcomp.character.inertia]
phi:223 [in mathcomp.character.inertia]
phi:223 [in mathcomp.character.classfun]
phi:224 [in mathcomp.character.inertia]
phi:224 [in mathcomp.character.character]
phi:225 [in mathcomp.character.character]
phi:227 [in mathcomp.character.character]
phi:230 [in mathcomp.character.character]
phi:231 [in mathcomp.character.classfun]
phi:233 [in mathcomp.character.inertia]
phi:235 [in mathcomp.character.inertia]
phi:236 [in mathcomp.character.mxabelem]
phi:236 [in mathcomp.character.character]
phi:239 [in mathcomp.character.inertia]
phi:242 [in mathcomp.character.vcharacter]
phi:244 [in mathcomp.character.inertia]
phi:245 [in mathcomp.character.vcharacter]
phi:248 [in mathcomp.character.inertia]
phi:25 [in mathcomp.character.inertia]
phi:253 [in mathcomp.character.inertia]
phi:253 [in mathcomp.character.classfun]
phi:254 [in mathcomp.character.classfun]
phi:256 [in mathcomp.character.vcharacter]
phi:256 [in mathcomp.character.classfun]
phi:257 [in mathcomp.character.classfun]
phi:258 [in mathcomp.character.inertia]
phi:259 [in mathcomp.character.classfun]
phi:260 [in mathcomp.character.classfun]
phi:262 [in mathcomp.character.inertia]
phi:263 [in mathcomp.character.classfun]
phi:266 [in mathcomp.character.inertia]
phi:269 [in mathcomp.character.classfun]
phi:271 [in mathcomp.character.classfun]
phi:272 [in mathcomp.character.inertia]
phi:272 [in mathcomp.character.classfun]
phi:273 [in mathcomp.character.classfun]
phi:274 [in mathcomp.character.classfun]
phi:275 [in mathcomp.character.inertia]
phi:275 [in mathcomp.character.classfun]
phi:276 [in mathcomp.character.classfun]
phi:277 [in mathcomp.character.classfun]
phi:28 [in mathcomp.character.inertia]
phi:280 [in mathcomp.character.classfun]
phi:281 [in mathcomp.character.inertia]
phi:283 [in mathcomp.character.classfun]
phi:285 [in mathcomp.character.inertia]
phi:285 [in mathcomp.character.classfun]
phi:285 [in mathcomp.character.character]
phi:286 [in mathcomp.character.vcharacter]
phi:289 [in mathcomp.character.inertia]
phi:29 [in mathcomp.character.classfun]
Phi:290 [in mathcomp.character.classfun]
phi:293 [in mathcomp.character.vcharacter]
phi:293 [in mathcomp.character.inertia]
phi:295 [in mathcomp.character.vcharacter]
phi:296 [in mathcomp.character.vcharacter]
phi:298 [in mathcomp.character.vcharacter]
phi:298 [in mathcomp.character.classfun]
phi:300 [in mathcomp.character.classfun]
phi:300 [in mathcomp.character.character]
phi:301 [in mathcomp.character.classfun]
phi:302 [in mathcomp.character.classfun]
Phi:307 [in mathcomp.character.classfun]
phi:31 [in mathcomp.character.vcharacter]
phi:31 [in mathcomp.character.inertia]
phi:311 [in mathcomp.character.inertia]
phi:312 [in mathcomp.character.inertia]
phi:314 [in mathcomp.character.classfun]
phi:317 [in mathcomp.character.classfun]
phi:318 [in mathcomp.character.inertia]
phi:319 [in mathcomp.character.inertia]
phi:320 [in mathcomp.character.vcharacter]
Phi:320 [in mathcomp.character.inertia]
phi:323 [in mathcomp.character.vcharacter]
phi:325 [in mathcomp.character.vcharacter]
phi:326 [in mathcomp.character.inertia]
phi:326 [in mathcomp.character.classfun]
phi:331 [in mathcomp.character.character]
phi:334 [in mathcomp.character.vcharacter]
phi:334 [in mathcomp.character.classfun]
phi:336 [in mathcomp.character.character]
phi:339 [in mathcomp.character.character]
phi:34 [in mathcomp.character.vcharacter]
phi:342 [in mathcomp.character.classfun]
phi:35 [in mathcomp.character.classfun]
phi:350 [in mathcomp.character.classfun]
phi:353 [in mathcomp.character.classfun]
phi:353 [in mathcomp.character.character]
phi:356 [in mathcomp.character.vcharacter]
phi:358 [in mathcomp.character.vcharacter]
phi:360 [in mathcomp.character.vcharacter]
phi:363 [in mathcomp.character.vcharacter]
phi:364 [in mathcomp.character.vcharacter]
phi:365 [in mathcomp.character.vcharacter]
phi:365 [in mathcomp.character.inertia]
phi:366 [in mathcomp.character.classfun]
phi:368 [in mathcomp.character.vcharacter]
phi:37 [in mathcomp.character.classfun]
phi:371 [in mathcomp.character.classfun]
phi:372 [in mathcomp.character.vcharacter]
phi:373 [in mathcomp.character.classfun]
phi:374 [in mathcomp.character.vcharacter]
phi:375 [in mathcomp.character.vcharacter]
phi:376 [in mathcomp.character.vcharacter]
phi:376 [in mathcomp.character.classfun]
phi:379 [in mathcomp.character.vcharacter]
phi:379 [in mathcomp.character.classfun]
phi:38 [in mathcomp.character.vcharacter]
phi:385 [in mathcomp.character.vcharacter]
phi:385 [in mathcomp.character.classfun]
phi:387 [in mathcomp.character.character]
phi:389 [in mathcomp.character.character]
phi:39 [in mathcomp.character.classfun]
phi:391 [in mathcomp.character.vcharacter]
phi:394 [in mathcomp.character.classfun]
phi:395 [in mathcomp.character.classfun]
phi:398 [in mathcomp.character.classfun]
phi:402 [in mathcomp.character.classfun]
phi:407 [in mathcomp.character.classfun]
phi:409 [in mathcomp.character.classfun]
phi:41 [in mathcomp.character.vcharacter]
phi:41 [in mathcomp.character.classfun]
phi:412 [in mathcomp.character.vcharacter]
phi:412 [in mathcomp.character.classfun]
phi:418 [in mathcomp.character.classfun]
phi:42 [in mathcomp.character.inertia]
phi:427 [in mathcomp.character.classfun]
phi:429 [in mathcomp.character.classfun]
phi:433 [in mathcomp.character.classfun]
phi:435 [in mathcomp.character.classfun]
phi:437 [in mathcomp.character.classfun]
phi:439 [in mathcomp.character.classfun]
phi:44 [in mathcomp.character.inertia]
phi:440 [in mathcomp.character.classfun]
phi:441 [in mathcomp.character.classfun]
phi:442 [in mathcomp.character.classfun]
phi:443 [in mathcomp.character.classfun]
phi:444 [in mathcomp.character.classfun]
phi:446 [in mathcomp.character.classfun]
phi:447 [in mathcomp.character.classfun]
phi:449 [in mathcomp.character.classfun]
phi:45 [in mathcomp.character.classfun]
phi:450 [in mathcomp.character.classfun]
phi:453 [in mathcomp.character.classfun]
phi:456 [in mathcomp.character.classfun]
phi:458 [in mathcomp.character.classfun]
phi:460 [in mathcomp.character.classfun]
phi:461 [in mathcomp.character.classfun]
phi:463 [in mathcomp.character.classfun]
phi:465 [in mathcomp.character.classfun]
phi:467 [in mathcomp.character.classfun]
phi:47 [in mathcomp.character.inertia]
phi:470 [in mathcomp.character.classfun]
phi:474 [in mathcomp.character.classfun]
phi:476 [in mathcomp.character.classfun]
phi:481 [in mathcomp.character.classfun]
phi:49 [in mathcomp.character.inertia]
phi:49 [in mathcomp.character.classfun]
phi:5 [in mathcomp.character.vcharacter]
phi:50 [in mathcomp.character.classfun]
phi:51 [in mathcomp.character.vcharacter]
phi:51 [in mathcomp.character.inertia]
phi:510 [in mathcomp.character.character]
phi:512 [in mathcomp.character.character]
phi:515 [in mathcomp.character.classfun]
phi:516 [in mathcomp.character.character]
phi:522 [in mathcomp.character.character]
phi:523 [in mathcomp.character.character]
phi:528 [in mathcomp.character.classfun]
phi:53 [in mathcomp.character.classfun]
phi:536 [in mathcomp.character.classfun]
phi:540 [in mathcomp.character.classfun]
phi:544 [in mathcomp.character.classfun]
phi:548 [in mathcomp.character.classfun]
phi:55 [in mathcomp.character.inertia]
phi:560 [in mathcomp.character.classfun]
phi:561 [in mathcomp.character.classfun]
phi:575 [in mathcomp.character.character]
phi:578 [in mathcomp.character.character]
phi:583 [in mathcomp.character.character]
phi:585 [in mathcomp.character.classfun]
phi:587 [in mathcomp.character.classfun]
phi:588 [in mathcomp.character.classfun]
phi:589 [in mathcomp.character.classfun]
phi:59 [in mathcomp.character.classfun]
phi:592 [in mathcomp.character.character]
phi:593 [in mathcomp.character.classfun]
phi:595 [in mathcomp.character.classfun]
phi:597 [in mathcomp.character.character]
phi:599 [in mathcomp.character.classfun]
phi:6 [in mathcomp.character.vcharacter]
phi:60 [in mathcomp.character.vcharacter]
phi:60 [in mathcomp.character.inertia]
phi:600 [in mathcomp.character.classfun]
phi:601 [in mathcomp.character.classfun]
phi:602 [in mathcomp.character.classfun]
phi:608 [in mathcomp.character.classfun]
phi:610 [in mathcomp.character.classfun]
phi:611 [in mathcomp.character.classfun]
phi:613 [in mathcomp.character.classfun]
phi:614 [in mathcomp.character.classfun]
phi:616 [in mathcomp.character.classfun]
phi:617 [in mathcomp.character.classfun]
phi:618 [in mathcomp.character.classfun]
phi:619 [in mathcomp.character.classfun]
phi:62 [in mathcomp.character.inertia]
phi:62 [in mathcomp.character.classfun]
phi:621 [in mathcomp.character.classfun]
phi:623 [in mathcomp.character.classfun]
phi:626 [in mathcomp.character.classfun]
phi:633 [in mathcomp.character.classfun]
phi:633 [in mathcomp.character.character]
phi:635 [in mathcomp.character.classfun]
phi:636 [in mathcomp.character.classfun]
phi:64 [in mathcomp.character.classfun]
phi:643 [in mathcomp.character.classfun]
phi:644 [in mathcomp.character.classfun]
phi:648 [in mathcomp.character.classfun]
phi:65 [in mathcomp.character.inertia]
phi:650 [in mathcomp.character.classfun]
phi:651 [in mathcomp.character.classfun]
phi:652 [in mathcomp.character.classfun]
phi:654 [in mathcomp.character.classfun]
phi:655 [in mathcomp.character.classfun]
phi:656 [in mathcomp.character.classfun]
phi:658 [in mathcomp.character.classfun]
phi:660 [in mathcomp.character.classfun]
phi:661 [in mathcomp.character.classfun]
phi:662 [in mathcomp.character.classfun]
phi:664 [in mathcomp.character.classfun]
phi:67 [in mathcomp.character.inertia]
phi:677 [in mathcomp.character.classfun]
phi:678 [in mathcomp.character.classfun]
phi:680 [in mathcomp.character.classfun]
phi:683 [in mathcomp.character.classfun]
phi:685 [in mathcomp.character.classfun]
phi:689 [in mathcomp.character.classfun]
phi:694 [in mathcomp.character.classfun]
phi:697 [in mathcomp.character.classfun]
phi:698 [in mathcomp.character.character]
phi:7 [in mathcomp.character.vcharacter]
phi:70 [in mathcomp.character.inertia]
phi:70 [in mathcomp.character.classfun]
phi:704 [in mathcomp.character.classfun]
phi:705 [in mathcomp.character.classfun]
phi:706 [in mathcomp.character.classfun]
phi:707 [in mathcomp.character.classfun]
phi:708 [in mathcomp.character.character]
phi:71 [in mathcomp.character.inertia]
phi:710 [in mathcomp.character.classfun]
phi:710 [in mathcomp.character.character]
phi:711 [in mathcomp.character.classfun]
phi:712 [in mathcomp.character.classfun]
phi:712 [in mathcomp.character.character]
phi:713 [in mathcomp.character.classfun]
phi:714 [in mathcomp.character.character]
phi:716 [in mathcomp.character.character]
phi:72 [in mathcomp.character.inertia]
phi:72 [in mathcomp.character.classfun]
phi:73 [in mathcomp.character.inertia]
phi:738 [in mathcomp.character.classfun]
phi:74 [in mathcomp.character.inertia]
phi:740 [in mathcomp.character.classfun]
phi:742 [in mathcomp.character.classfun]
phi:744 [in mathcomp.character.classfun]
phi:746 [in mathcomp.character.classfun]
phi:748 [in mathcomp.character.classfun]
phi:75 [in mathcomp.character.inertia]
phi:750 [in mathcomp.character.classfun]
phi:752 [in mathcomp.character.classfun]
phi:758 [in mathcomp.character.classfun]
phi:76 [in mathcomp.character.inertia]
phi:762 [in mathcomp.character.classfun]
phi:764 [in mathcomp.character.classfun]
phi:767 [in mathcomp.character.classfun]
phi:768 [in mathcomp.character.classfun]
phi:768 [in mathcomp.character.character]
phi:77 [in mathcomp.character.inertia]
phi:770 [in mathcomp.character.character]
phi:771 [in mathcomp.character.character]
phi:774 [in mathcomp.character.classfun]
phi:774 [in mathcomp.character.character]
phi:776 [in mathcomp.character.character]
phi:777 [in mathcomp.character.character]
phi:78 [in mathcomp.character.classfun]
phi:783 [in mathcomp.character.character]
phi:790 [in mathcomp.character.character]
phi:795 [in mathcomp.character.character]
phi:8 [in mathcomp.character.inertia]
phi:80 [in mathcomp.character.inertia]
phi:801 [in mathcomp.character.classfun]
phi:803 [in mathcomp.character.classfun]
phi:806 [in mathcomp.character.character]
phi:807 [in mathcomp.character.classfun]
phi:809 [in mathcomp.character.character]
phi:81 [in mathcomp.character.inertia]
phi:816 [in mathcomp.character.classfun]
phi:82 [in mathcomp.character.inertia]
phi:820 [in mathcomp.character.classfun]
phi:829 [in mathcomp.character.classfun]
phi:83 [in mathcomp.character.inertia]
phi:833 [in mathcomp.character.classfun]
Phi:834 [in mathcomp.character.classfun]
phi:840 [in mathcomp.character.classfun]
phi:85 [in mathcomp.character.inertia]
phi:86 [in mathcomp.character.classfun]
phi:874 [in mathcomp.character.classfun]
phi:877 [in mathcomp.character.classfun]
phi:885 [in mathcomp.character.classfun]
phi:89 [in mathcomp.character.classfun]
phi:892 [in mathcomp.character.classfun]
phi:893 [in mathcomp.character.classfun]
phi:896 [in mathcomp.character.classfun]
phi:9 [in mathcomp.character.vcharacter]
Phi:90 [in mathcomp.character.inertia]
phi:906 [in mathcomp.character.classfun]
phi:907 [in mathcomp.character.classfun]
phi:917 [in mathcomp.character.classfun]
phi:918 [in mathcomp.character.classfun]
phi:919 [in mathcomp.character.classfun]
phi:92 [in mathcomp.character.vcharacter]
phi:920 [in mathcomp.character.classfun]
phi:921 [in mathcomp.character.classfun]
phi:93 [in mathcomp.character.classfun]
phi:936 [in mathcomp.character.character]
phi:94 [in mathcomp.character.classfun]
phi:942 [in mathcomp.character.classfun]
phi:975 [in mathcomp.character.classfun]
phi:976 [in mathcomp.character.classfun]
phi:98 [in mathcomp.character.inertia]
phi:986 [in mathcomp.character.classfun]
phi:988 [in mathcomp.character.character]
phi:993 [in mathcomp.character.classfun]
phi:994 [in mathcomp.character.classfun]
phi:994 [in mathcomp.character.character]
phi:995 [in mathcomp.character.character]
phi:997 [in mathcomp.character.character]
phUV:1113 [in mathcomp.algebra.ssralg]
phUV:816 [in mathcomp.algebra.ssralg]
ph:22 [in mathcomp.ssreflect.finfun]
ph:25 [in mathcomp.ssreflect.finfun]
ph:26 [in mathcomp.ssreflect.finfun]
pickleK:186 [in mathcomp.ssreflect.choice]
pickleK:193 [in mathcomp.ssreflect.choice]
pickle:184 [in mathcomp.ssreflect.choice]
pickle:191 [in mathcomp.ssreflect.choice]
pis:480 [in mathcomp.solvable.pgroup]
pis:483 [in mathcomp.solvable.pgroup]
pis:484 [in mathcomp.solvable.pgroup]
pis:485 [in mathcomp.solvable.pgroup]
pis:486 [in mathcomp.solvable.pgroup]
pis:487 [in mathcomp.solvable.pgroup]
pis:488 [in mathcomp.solvable.pgroup]
pis:489 [in mathcomp.solvable.pgroup]
pis:490 [in mathcomp.solvable.pgroup]
pis:493 [in mathcomp.solvable.pgroup]
pis:496 [in mathcomp.solvable.pgroup]
pis:504 [in mathcomp.solvable.pgroup]
pis:515 [in mathcomp.solvable.pgroup]
pis:563 [in mathcomp.solvable.pgroup]
pis:623 [in mathcomp.solvable.pgroup]
pis:631 [in mathcomp.solvable.pgroup]
pi_eq_quot:106 [in mathcomp.ssreflect.generic_quotient]
pi_invr:100 [in mathcomp.algebra.ring_quotient]
pi_unitr:97 [in mathcomp.algebra.ring_quotient]
pi_mulr:54 [in mathcomp.algebra.ring_quotient]
pi_oner:49 [in mathcomp.algebra.ring_quotient]
pi_addr:15 [in mathcomp.algebra.ring_quotient]
pi_oppr:10 [in mathcomp.algebra.ring_quotient]
pi_zeror:7 [in mathcomp.algebra.ring_quotient]
Pi0:1175 [in mathcomp.algebra.ssrnum]
Pi0:1412 [in mathcomp.ssreflect.order]
Pi0:782 [in mathcomp.ssreflect.order]
pi1s:511 [in mathcomp.solvable.pgroup]
pi1s:519 [in mathcomp.solvable.pgroup]
pi1s:523 [in mathcomp.solvable.pgroup]
pi1s:531 [in mathcomp.solvable.pgroup]
pi1s:535 [in mathcomp.solvable.pgroup]
pi1s:539 [in mathcomp.solvable.pgroup]
pi1s:543 [in mathcomp.solvable.pgroup]
pi1s:547 [in mathcomp.solvable.pgroup]
pi1:227 [in mathcomp.solvable.pgroup]
pi1:230 [in mathcomp.solvable.pgroup]
pi1:235 [in mathcomp.solvable.pgroup]
pi1:267 [in mathcomp.solvable.pgroup]
pi1:343 [in mathcomp.ssreflect.prime]
pi1:349 [in mathcomp.ssreflect.prime]
pi1:356 [in mathcomp.ssreflect.prime]
pi1:359 [in mathcomp.ssreflect.prime]
pi1:507 [in mathcomp.solvable.pgroup]
pi1:527 [in mathcomp.solvable.pgroup]
pi1:938 [in mathcomp.algebra.vector]
pi2s:512 [in mathcomp.solvable.pgroup]
pi2s:520 [in mathcomp.solvable.pgroup]
pi2s:524 [in mathcomp.solvable.pgroup]
pi2s:532 [in mathcomp.solvable.pgroup]
pi2s:536 [in mathcomp.solvable.pgroup]
pi2s:540 [in mathcomp.solvable.pgroup]
pi2s:544 [in mathcomp.solvable.pgroup]
pi2s:548 [in mathcomp.solvable.pgroup]
pi2:228 [in mathcomp.solvable.pgroup]
pi2:231 [in mathcomp.solvable.pgroup]
pi2:236 [in mathcomp.solvable.pgroup]
pi2:268 [in mathcomp.solvable.pgroup]
pi2:344 [in mathcomp.ssreflect.prime]
pi2:350 [in mathcomp.ssreflect.prime]
pi2:357 [in mathcomp.ssreflect.prime]
pi2:360 [in mathcomp.ssreflect.prime]
pi2:508 [in mathcomp.solvable.pgroup]
pi2:528 [in mathcomp.solvable.pgroup]
pi2:945 [in mathcomp.algebra.vector]
pi:100 [in mathcomp.solvable.sylow]
pi:100 [in mathcomp.solvable.pgroup]
pi:103 [in mathcomp.solvable.pgroup]
pi:106 [in mathcomp.solvable.hall]
pi:107 [in mathcomp.solvable.sylow]
pi:107 [in mathcomp.solvable.pgroup]
pi:11 [in mathcomp.solvable.pgroup]
pi:111 [in mathcomp.solvable.pgroup]
pi:113 [in mathcomp.solvable.sylow]
pi:115 [in mathcomp.solvable.pgroup]
pi:119 [in mathcomp.solvable.pgroup]
pi:123 [in mathcomp.solvable.pgroup]
pi:126 [in mathcomp.solvable.pgroup]
pi:129 [in mathcomp.solvable.sylow]
pi:131 [in mathcomp.solvable.pgroup]
pi:135 [in mathcomp.solvable.sylow]
pi:136 [in mathcomp.solvable.pgroup]
pi:138 [in mathcomp.solvable.sylow]
pi:1390 [in mathcomp.algebra.ssrnum]
pi:14 [in mathcomp.solvable.pgroup]
pi:140 [in mathcomp.solvable.sylow]
pi:143 [in mathcomp.solvable.pgroup]
pi:153 [in mathcomp.solvable.pgroup]
pi:157 [in mathcomp.solvable.pgroup]
pi:161 [in mathcomp.solvable.pgroup]
pi:165 [in mathcomp.solvable.pgroup]
pi:169 [in mathcomp.solvable.pgroup]
pi:173 [in mathcomp.solvable.pgroup]
pi:177 [in mathcomp.solvable.pgroup]
pi:178 [in mathcomp.solvable.maximal]
pi:184 [in mathcomp.solvable.pgroup]
pi:196 [in mathcomp.solvable.pgroup]
pi:2 [in mathcomp.solvable.pgroup]
pi:206 [in mathcomp.solvable.pgroup]
pi:209 [in mathcomp.solvable.pgroup]
pi:212 [in mathcomp.solvable.pgroup]
pi:215 [in mathcomp.solvable.pgroup]
pi:218 [in mathcomp.solvable.pgroup]
pi:219 [in mathcomp.solvable.pgroup]
pi:22 [in mathcomp.solvable.hall]
pi:221 [in mathcomp.solvable.pgroup]
pi:224 [in mathcomp.solvable.pgroup]
pi:233 [in mathcomp.solvable.pgroup]
pi:238 [in mathcomp.solvable.pgroup]
pi:240 [in mathcomp.solvable.pgroup]
pi:242 [in mathcomp.solvable.pgroup]
pi:244 [in mathcomp.solvable.pgroup]
pi:245 [in mathcomp.solvable.pgroup]
pi:248 [in mathcomp.solvable.pgroup]
pi:250 [in mathcomp.solvable.pgroup]
pi:252 [in mathcomp.solvable.pgroup]
pi:254 [in mathcomp.solvable.pgroup]
pi:256 [in mathcomp.solvable.pgroup]
pI:2594 [in mathcomp.ssreflect.bigop]
pi:260 [in mathcomp.solvable.pgroup]
pi:263 [in mathcomp.solvable.pgroup]
pi:265 [in mathcomp.solvable.pgroup]
pi:276 [in mathcomp.solvable.pgroup]
pi:28 [in mathcomp.solvable.pgroup]
pi:284 [in mathcomp.solvable.pgroup]
pi:291 [in mathcomp.solvable.pgroup]
pi:298 [in mathcomp.solvable.pgroup]
pi:30 [in mathcomp.solvable.pgroup]
pi:305 [in mathcomp.solvable.pgroup]
pi:309 [in mathcomp.solvable.pgroup]
pi:310 [in mathcomp.solvable.abelian]
pi:315 [in mathcomp.solvable.pgroup]
pi:318 [in mathcomp.solvable.pgroup]
pi:33 [in mathcomp.solvable.pgroup]
pi:332 [in mathcomp.solvable.pgroup]
pi:336 [in mathcomp.solvable.pgroup]
pi:34 [in mathcomp.solvable.hall]
pi:340 [in mathcomp.solvable.pgroup]
pi:342 [in mathcomp.ssreflect.prime]
pi:347 [in mathcomp.ssreflect.prime]
pi:36 [in mathcomp.solvable.pgroup]
pi:361 [in mathcomp.solvable.pgroup]
pi:362 [in mathcomp.ssreflect.prime]
pi:364 [in mathcomp.solvable.pgroup]
pi:365 [in mathcomp.ssreflect.prime]
pi:366 [in mathcomp.solvable.pgroup]
pi:369 [in mathcomp.solvable.pgroup]
pi:37 [in mathcomp.solvable.hall]
pi:372 [in mathcomp.solvable.pgroup]
pi:372 [in mathcomp.ssreflect.prime]
pi:373 [in mathcomp.ssreflect.prime]
pi:374 [in mathcomp.ssreflect.prime]
pi:375 [in mathcomp.ssreflect.prime]
pi:380 [in mathcomp.ssreflect.prime]
pi:383 [in mathcomp.solvable.pgroup]
pi:383 [in mathcomp.ssreflect.prime]
pi:385 [in mathcomp.solvable.pgroup]
pi:39 [in mathcomp.solvable.pgroup]
pi:392 [in mathcomp.ssreflect.prime]
pi:4 [in mathcomp.solvable.pgroup]
pi:400 [in mathcomp.ssreflect.prime]
pi:402 [in mathcomp.ssreflect.prime]
pi:406 [in mathcomp.ssreflect.prime]
pi:411 [in mathcomp.solvable.pgroup]
pi:411 [in mathcomp.ssreflect.prime]
pi:413 [in mathcomp.solvable.pgroup]
pi:419 [in mathcomp.ssreflect.prime]
pi:42 [in mathcomp.solvable.pgroup]
pi:439 [in mathcomp.ssreflect.prime]
pi:445 [in mathcomp.solvable.pgroup]
pi:446 [in mathcomp.solvable.pgroup]
pi:45 [in mathcomp.solvable.pgroup]
pi:450 [in mathcomp.solvable.pgroup]
pi:451 [in mathcomp.solvable.pgroup]
pi:452 [in mathcomp.solvable.pgroup]
pi:453 [in mathcomp.solvable.pgroup]
pi:457 [in mathcomp.solvable.pgroup]
pi:46 [in mathcomp.solvable.hall]
pi:460 [in mathcomp.solvable.pgroup]
pi:462 [in mathcomp.ssreflect.prime]
pi:464 [in mathcomp.solvable.pgroup]
pi:465 [in mathcomp.ssreflect.prime]
pi:468 [in mathcomp.ssreflect.prime]
pi:471 [in mathcomp.solvable.pgroup]
pi:471 [in mathcomp.ssreflect.prime]
pi:473 [in mathcomp.ssreflect.prime]
pi:476 [in mathcomp.solvable.pgroup]
pi:476 [in mathcomp.ssreflect.prime]
pi:479 [in mathcomp.solvable.pgroup]
pi:479 [in mathcomp.ssreflect.prime]
pi:48 [in mathcomp.solvable.pgroup]
pi:482 [in mathcomp.ssreflect.prime]
pi:484 [in mathcomp.ssreflect.prime]
pi:494 [in mathcomp.ssreflect.prime]
pi:500 [in mathcomp.solvable.pgroup]
pi:503 [in mathcomp.solvable.pgroup]
pi:503 [in mathcomp.ssreflect.prime]
pi:508 [in mathcomp.ssreflect.prime]
pi:51 [in mathcomp.solvable.hall]
pi:511 [in mathcomp.ssreflect.prime]
pi:512 [in mathcomp.ssreflect.prime]
pi:515 [in mathcomp.ssreflect.prime]
pi:516 [in mathcomp.solvable.pgroup]
pi:518 [in mathcomp.ssreflect.prime]
pi:522 [in mathcomp.ssreflect.prime]
pi:525 [in mathcomp.ssreflect.prime]
pi:527 [in mathcomp.ssreflect.prime]
pi:529 [in mathcomp.ssreflect.prime]
pi:53 [in mathcomp.solvable.pgroup]
pi:531 [in mathcomp.ssreflect.prime]
pi:533 [in mathcomp.ssreflect.prime]
pi:536 [in mathcomp.ssreflect.prime]
pi:542 [in mathcomp.ssreflect.prime]
pi:546 [in mathcomp.ssreflect.prime]
pi:548 [in mathcomp.ssreflect.prime]
pi:55 [in mathcomp.solvable.pgroup]
pi:551 [in mathcomp.solvable.pgroup]
pi:551 [in mathcomp.ssreflect.prime]
pi:556 [in mathcomp.solvable.pgroup]
pi:560 [in mathcomp.solvable.pgroup]
pi:564 [in mathcomp.solvable.pgroup]
pi:568 [in mathcomp.solvable.pgroup]
pi:57 [in mathcomp.solvable.hall]
pi:571 [in mathcomp.solvable.pgroup]
pi:574 [in mathcomp.solvable.pgroup]
pi:577 [in mathcomp.solvable.pgroup]
pi:58 [in mathcomp.solvable.pgroup]
pi:580 [in mathcomp.solvable.pgroup]
pi:582 [in mathcomp.solvable.pgroup]
pi:585 [in mathcomp.solvable.pgroup]
pi:588 [in mathcomp.solvable.pgroup]
pi:59 [in mathcomp.solvable.pgroup]
pi:591 [in mathcomp.solvable.pgroup]
pi:594 [in mathcomp.solvable.pgroup]
pi:600 [in mathcomp.solvable.pgroup]
pi:603 [in mathcomp.solvable.pgroup]
pi:606 [in mathcomp.solvable.pgroup]
pi:614 [in mathcomp.solvable.pgroup]
pi:616 [in mathcomp.solvable.pgroup]
pi:618 [in mathcomp.solvable.pgroup]
pi:621 [in mathcomp.solvable.pgroup]
pi:629 [in mathcomp.solvable.pgroup]
pi:63 [in mathcomp.solvable.hall]
pi:630 [in mathcomp.solvable.pgroup]
pi:71 [in mathcomp.solvable.pgroup]
pi:74 [in mathcomp.solvable.pgroup]
pi:8 [in mathcomp.solvable.pgroup]
pi:80 [in mathcomp.solvable.abelian]
pi:88 [in mathcomp.solvable.pgroup]
pi:88 [in mathcomp.solvable.maximal]
pi:91 [in mathcomp.solvable.pgroup]
pi:91 [in mathcomp.solvable.abelian]
pi:923 [in mathcomp.algebra.vector]
pi:94 [in mathcomp.solvable.pgroup]
pi:94 [in mathcomp.solvable.abelian]
pi:97 [in mathcomp.solvable.pgroup]
pJ:2595 [in mathcomp.ssreflect.bigop]
PK:132 [in mathcomp.ssreflect.generic_quotient]
poly_ivt_subproof:96 [in mathcomp.algebra.ssrnum]
pos_lit:1653 [in mathcomp.algebra.ssralg]
pp:205 [in mathcomp.field.closed_field]
pp:211 [in mathcomp.field.closed_field]
PP:400 [in mathcomp.ssreflect.fintype]
PP:444 [in mathcomp.ssreflect.fintype]
pp:492 [in mathcomp.algebra.polydiv]
pp:501 [in mathcomp.algebra.polydiv]
pp:65 [in mathcomp.algebra.polydiv]
pp:74 [in mathcomp.algebra.polydiv]
pqs:328 [in mathcomp.field.closed_field]
pqs:333 [in mathcomp.field.closed_field]
prime_idealr_closed_subproof:163 [in mathcomp.algebra.ring_quotient]
prim_r:227 [in mathcomp.solvable.cyclic]
print_IRat:56 [in mathcomp.algebra.rat]
print_pos:53 [in mathcomp.algebra.rat]
proj:1991 [in mathcomp.algebra.ssralg]
properVU:1361 [in mathcomp.character.mxrepresentation]
proper_ideal_subproof:152 [in mathcomp.algebra.ring_quotient]
pr:248 [in mathcomp.field.closed_field]
psi1:399 [in mathcomp.character.classfun]
psi1:772 [in mathcomp.character.classfun]
psi2:400 [in mathcomp.character.classfun]
psi2:773 [in mathcomp.character.classfun]
psi:101 [in mathcomp.character.classfun]
psi:1018 [in mathcomp.character.classfun]
psi:1022 [in mathcomp.character.classfun]
psi:1023 [in mathcomp.character.classfun]
psi:1026 [in mathcomp.character.classfun]
psi:1028 [in mathcomp.character.classfun]
psi:103 [in mathcomp.character.inertia]
psi:104 [in mathcomp.character.classfun]
psi:118 [in mathcomp.character.inertia]
psi:124 [in mathcomp.character.vcharacter]
psi:129 [in mathcomp.character.vcharacter]
psi:129 [in mathcomp.character.classfun]
psi:133 [in mathcomp.character.vcharacter]
psi:135 [in mathcomp.character.classfun]
psi:147 [in mathcomp.character.inertia]
psi:153 [in mathcomp.character.inertia]
psi:155 [in mathcomp.character.inertia]
psi:160 [in mathcomp.character.classfun]
psi:166 [in mathcomp.character.classfun]
psi:169 [in mathcomp.character.classfun]
psi:189 [in mathcomp.character.classfun]
psi:190 [in mathcomp.character.inertia]
psi:196 [in mathcomp.character.inertia]
psi:278 [in mathcomp.character.vcharacter]
psi:280 [in mathcomp.character.vcharacter]
psi:283 [in mathcomp.character.vcharacter]
psi:283 [in mathcomp.character.inertia]
psi:286 [in mathcomp.character.inertia]
psi:286 [in mathcomp.character.classfun]
psi:291 [in mathcomp.character.inertia]
psi:294 [in mathcomp.character.inertia]
psi:303 [in mathcomp.character.classfun]
psi:318 [in mathcomp.character.classfun]
psi:327 [in mathcomp.character.classfun]
psi:335 [in mathcomp.character.classfun]
psi:337 [in mathcomp.character.inertia]
psi:340 [in mathcomp.character.inertia]
psi:343 [in mathcomp.character.inertia]
psi:343 [in mathcomp.character.classfun]
psi:351 [in mathcomp.character.classfun]
psi:36 [in mathcomp.character.classfun]
psi:362 [in mathcomp.character.classfun]
psi:365 [in mathcomp.character.classfun]
psi:366 [in mathcomp.character.inertia]
psi:374 [in mathcomp.character.classfun]
psi:377 [in mathcomp.character.classfun]
psi:396 [in mathcomp.character.classfun]
psi:40 [in mathcomp.character.classfun]
psi:403 [in mathcomp.character.classfun]
psi:410 [in mathcomp.character.classfun]
psi:413 [in mathcomp.character.vcharacter]
psi:416 [in mathcomp.character.vcharacter]
psi:430 [in mathcomp.character.classfun]
psi:434 [in mathcomp.character.classfun]
psi:436 [in mathcomp.character.classfun]
psi:438 [in mathcomp.character.classfun]
psi:451 [in mathcomp.character.classfun]
psi:454 [in mathcomp.character.classfun]
psi:457 [in mathcomp.character.classfun]
psi:459 [in mathcomp.character.classfun]
psi:462 [in mathcomp.character.classfun]
psi:464 [in mathcomp.character.classfun]
psi:466 [in mathcomp.character.classfun]
psi:471 [in mathcomp.character.classfun]
psi:475 [in mathcomp.character.classfun]
psi:478 [in mathcomp.character.classfun]
psi:480 [in mathcomp.character.classfun]
psi:51 [in mathcomp.character.classfun]
psi:516 [in mathcomp.character.classfun]
psi:517 [in mathcomp.character.character]
psi:537 [in mathcomp.character.classfun]
psi:54 [in mathcomp.character.classfun]
psi:541 [in mathcomp.character.classfun]
psi:545 [in mathcomp.character.classfun]
psi:597 [in mathcomp.character.classfun]
psi:598 [in mathcomp.character.character]
psi:60 [in mathcomp.character.classfun]
psi:63 [in mathcomp.character.classfun]
psi:649 [in mathcomp.character.character]
psi:651 [in mathcomp.character.character]
psi:663 [in mathcomp.character.classfun]
psi:669 [in mathcomp.character.classfun]
psi:672 [in mathcomp.character.classfun]
psi:675 [in mathcomp.character.classfun]
psi:687 [in mathcomp.character.classfun]
psi:695 [in mathcomp.character.classfun]
psi:698 [in mathcomp.character.classfun]
psi:709 [in mathcomp.character.character]
psi:711 [in mathcomp.character.character]
psi:713 [in mathcomp.character.character]
psi:715 [in mathcomp.character.character]
psi:717 [in mathcomp.character.character]
psi:739 [in mathcomp.character.classfun]
psi:741 [in mathcomp.character.classfun]
psi:743 [in mathcomp.character.classfun]
psi:745 [in mathcomp.character.classfun]
psi:747 [in mathcomp.character.classfun]
psi:749 [in mathcomp.character.classfun]
psi:751 [in mathcomp.character.classfun]
psi:755 [in mathcomp.character.classfun]
psi:759 [in mathcomp.character.classfun]
psi:763 [in mathcomp.character.classfun]
psi:765 [in mathcomp.character.classfun]
psi:766 [in mathcomp.character.classfun]
psi:769 [in mathcomp.character.classfun]
psi:775 [in mathcomp.character.classfun]
psi:783 [in mathcomp.character.classfun]
psi:841 [in mathcomp.character.classfun]
psi:86 [in mathcomp.character.inertia]
psi:90 [in mathcomp.character.classfun]
psi:943 [in mathcomp.character.classfun]
psi:974 [in mathcomp.character.classfun]
psi:977 [in mathcomp.character.classfun]
psi:996 [in mathcomp.character.character]
psi:998 [in mathcomp.character.character]
ps:1009 [in mathcomp.algebra.poly]
ps:1039 [in mathcomp.algebra.poly]
ps:210 [in mathcomp.field.galois]
ps:211 [in mathcomp.field.galois]
ps:245 [in mathcomp.field.closed_field]
ps:252 [in mathcomp.field.closed_field]
ps:257 [in mathcomp.field.closed_field]
Ps:2763 [in mathcomp.ssreflect.seq]
Ps:2770 [in mathcomp.ssreflect.seq]
Ps:2779 [in mathcomp.ssreflect.seq]
ps:288 [in mathcomp.field.closed_field]
ps:293 [in mathcomp.field.closed_field]
ps:300 [in mathcomp.field.closed_field]
ps:337 [in mathcomp.field.closed_field]
ps:342 [in mathcomp.field.closed_field]
ps:418 [in mathcomp.algebra.polydiv]
ps:721 [in mathcomp.algebra.polydiv]
ps:8 [in mathcomp.field.algnum]
ps:96 [in mathcomp.ssreflect.ssrAC]
ps:977 [in mathcomp.algebra.poly]
Pt:1229 [in mathcomp.algebra.mxalgebra]
Pt:1230 [in mathcomp.algebra.mxalgebra]
pT:133 [in mathcomp.ssreflect.finfun]
pT:227 [in mathcomp.ssreflect.fintype]
pT:26 [in mathcomp.ssreflect.fintype]
pT:65 [in mathcomp.ssreflect.prime]
pu:299 [in mathcomp.field.algebraics_fundamentals]
pval:4 [in mathcomp.fingroup.perm]
Px:102 [in mathcomp.solvable.finmodule]
Px:103 [in mathcomp.solvable.finmodule]
Px:104 [in mathcomp.solvable.finmodule]
Px:105 [in mathcomp.solvable.finmodule]
Px:106 [in mathcomp.solvable.finmodule]
px:124 [in mathcomp.ssreflect.generic_quotient]
Px:124 [in mathcomp.solvable.finmodule]
Px:125 [in mathcomp.solvable.finmodule]
Px:126 [in mathcomp.ssreflect.generic_quotient]
Px:126 [in mathcomp.solvable.finmodule]
Px:127 [in mathcomp.solvable.finmodule]
Px:128 [in mathcomp.solvable.finmodule]
Px:131 [in mathcomp.ssreflect.generic_quotient]
Px:251 [in mathcomp.ssreflect.eqtype]
Px:255 [in mathcomp.ssreflect.eqtype]
Px:273 [in mathcomp.ssreflect.eqtype]
Px:277 [in mathcomp.ssreflect.eqtype]
Px:288 [in mathcomp.ssreflect.eqtype]
Px:300 [in mathcomp.ssreflect.eqtype]
Px:307 [in mathcomp.ssreflect.eqtype]
px:798 [in mathcomp.ssreflect.path]
p_gt1:59 [in mathcomp.algebra.zmodp]
p_gt1:57 [in mathcomp.algebra.zmodp]
p_i:283 [in mathcomp.field.algebraics_fundamentals]
p_j:66 [in mathcomp.field.algC]
p_j:65 [in mathcomp.field.algC]
p_:3521 [in mathcomp.algebra.matrix]
p_:3506 [in mathcomp.algebra.matrix]
p_:3494 [in mathcomp.algebra.matrix]
p_:3460 [in mathcomp.algebra.matrix]
p_:3453 [in mathcomp.algebra.matrix]
p_:3326 [in mathcomp.algebra.matrix]
p_:3306 [in mathcomp.algebra.matrix]
p_:3248 [in mathcomp.algebra.matrix]
p_:3164 [in mathcomp.algebra.matrix]
p_:3145 [in mathcomp.algebra.matrix]
p_:3076 [in mathcomp.algebra.matrix]
p_:2969 [in mathcomp.algebra.matrix]
p_:2949 [in mathcomp.algebra.matrix]
p_:2937 [in mathcomp.algebra.matrix]
p_:2925 [in mathcomp.algebra.matrix]
p_:2916 [in mathcomp.algebra.matrix]
p_:2899 [in mathcomp.algebra.matrix]
p_:2874 [in mathcomp.algebra.matrix]
p_:2863 [in mathcomp.algebra.matrix]
p_:2678 [in mathcomp.algebra.matrix]
p_:790 [in mathcomp.algebra.mxpoly]
p_:324 [in mathcomp.algebra.mxpoly]
p_:308 [in mathcomp.algebra.mxpoly]
p_x:745 [in mathcomp.ssreflect.path]
p_:4917 [in mathcomp.ssreflect.order]
p_:1916 [in mathcomp.algebra.mxalgebra]
P':1560 [in mathcomp.ssreflect.order]
P':1573 [in mathcomp.ssreflect.order]
P':1611 [in mathcomp.ssreflect.order]
P':1626 [in mathcomp.ssreflect.order]
P':1640 [in mathcomp.ssreflect.order]
P':1653 [in mathcomp.ssreflect.order]
P':1694 [in mathcomp.ssreflect.order]
P':1709 [in mathcomp.ssreflect.order]
P':1744 [in mathcomp.ssreflect.order]
P':1757 [in mathcomp.ssreflect.order]
P':1803 [in mathcomp.ssreflect.order]
P':1826 [in mathcomp.ssreflect.order]
P':2353 [in mathcomp.ssreflect.bigop]
P':2381 [in mathcomp.ssreflect.bigop]
P':2405 [in mathcomp.ssreflect.bigop]
P':2432 [in mathcomp.ssreflect.bigop]
P':2445 [in mathcomp.ssreflect.bigop]
P':2484 [in mathcomp.ssreflect.bigop]
P':2508 [in mathcomp.ssreflect.bigop]
p':42 [in mathcomp.ssreflect.ssrAC]
p':431 [in mathcomp.ssreflect.path]
P':761 [in mathcomp.ssreflect.finset]
p':774 [in mathcomp.ssreflect.path]
p':784 [in mathcomp.ssreflect.path]
p0:1190 [in mathcomp.ssreflect.ssrnat]
P0:2762 [in mathcomp.ssreflect.seq]
P0:2769 [in mathcomp.ssreflect.seq]
P0:2778 [in mathcomp.ssreflect.seq]
p1:10 [in mathcomp.ssreflect.path]
P1:123 [in mathcomp.algebra.qpoly]
p1:130 [in mathcomp.solvable.burnside_app]
p1:130 [in mathcomp.ssreflect.eqtype]
p1:152 [in mathcomp.solvable.burnside_app]
P1:1578 [in mathcomp.ssreflect.finset]
P1:1604 [in mathcomp.ssreflect.finset]
p1:1794 [in mathcomp.algebra.matrix]
p1:1817 [in mathcomp.algebra.matrix]
p1:1826 [in mathcomp.algebra.matrix]
p1:1849 [in mathcomp.algebra.matrix]
p1:229 [in mathcomp.field.closed_field]
p1:233 [in mathcomp.field.closed_field]
P1:2522 [in mathcomp.ssreflect.bigop]
P1:2592 [in mathcomp.algebra.matrix]
p1:26 [in mathcomp.solvable.alt]
p1:301 [in mathcomp.ssreflect.path]
p1:310 [in mathcomp.ssreflect.path]
p1:318 [in mathcomp.ssreflect.path]
p1:375 [in mathcomp.ssreflect.path]
p1:379 [in mathcomp.ssreflect.path]
p1:384 [in mathcomp.ssreflect.path]
p1:397 [in mathcomp.ssreflect.eqtype]
p1:399 [in mathcomp.ssreflect.path]
p1:402 [in mathcomp.ssreflect.path]
p1:406 [in mathcomp.ssreflect.path]
p1:418 [in mathcomp.ssreflect.path]
p1:427 [in mathcomp.algebra.intdiv]
p1:430 [in mathcomp.algebra.intdiv]
p1:44 [in mathcomp.solvable.burnside_app]
P1:459 [in mathcomp.ssreflect.fintype]
P1:468 [in mathcomp.ssreflect.fintype]
P1:477 [in mathcomp.ssreflect.fintype]
P1:486 [in mathcomp.ssreflect.fintype]
P1:527 [in mathcomp.ssreflect.bigop]
P1:537 [in mathcomp.ssreflect.bigop]
p1:567 [in mathcomp.algebra.polydiv]
P1:568 [in mathcomp.ssreflect.bigop]
P1:581 [in mathcomp.ssreflect.bigop]
P1:755 [in mathcomp.ssreflect.bigop]
p1:805 [in mathcomp.ssreflect.path]
p1:810 [in mathcomp.ssreflect.path]
p1:819 [in mathcomp.ssreflect.path]
p1:83 [in mathcomp.character.character]
p1:941 [in mathcomp.algebra.polydiv]
p1:948 [in mathcomp.algebra.polydiv]
p2:11 [in mathcomp.ssreflect.path]
p2:131 [in mathcomp.solvable.burnside_app]
p2:131 [in mathcomp.ssreflect.eqtype]
p2:153 [in mathcomp.solvable.burnside_app]
P2:1579 [in mathcomp.ssreflect.finset]
P2:1605 [in mathcomp.ssreflect.finset]
p2:1795 [in mathcomp.algebra.matrix]
p2:1818 [in mathcomp.algebra.matrix]
p2:1827 [in mathcomp.algebra.matrix]
p2:1850 [in mathcomp.algebra.matrix]
P2:2523 [in mathcomp.ssreflect.bigop]
p2:302 [in mathcomp.ssreflect.path]
p2:311 [in mathcomp.ssreflect.path]
p2:319 [in mathcomp.ssreflect.path]
p2:376 [in mathcomp.ssreflect.path]
p2:383 [in mathcomp.ssreflect.path]
p2:398 [in mathcomp.ssreflect.eqtype]
p2:400 [in mathcomp.ssreflect.path]
p2:403 [in mathcomp.ssreflect.path]
p2:407 [in mathcomp.ssreflect.path]
p2:419 [in mathcomp.ssreflect.path]
p2:45 [in mathcomp.solvable.burnside_app]
P2:460 [in mathcomp.ssreflect.fintype]
P2:469 [in mathcomp.ssreflect.fintype]
P2:478 [in mathcomp.ssreflect.fintype]
P2:487 [in mathcomp.ssreflect.fintype]
P2:528 [in mathcomp.ssreflect.bigop]
P2:538 [in mathcomp.ssreflect.bigop]
p2:568 [in mathcomp.algebra.polydiv]
P2:569 [in mathcomp.ssreflect.bigop]
P2:582 [in mathcomp.ssreflect.bigop]
P2:756 [in mathcomp.ssreflect.bigop]
p2:77 [in mathcomp.character.character]
p2:806 [in mathcomp.ssreflect.path]
p2:811 [in mathcomp.ssreflect.path]
p2:820 [in mathcomp.ssreflect.path]
p2:88 [in mathcomp.character.character]
p2:942 [in mathcomp.algebra.polydiv]
p2:949 [in mathcomp.algebra.polydiv]
p3:380 [in mathcomp.ssreflect.path]
p3:385 [in mathcomp.ssreflect.path]
p3:408 [in mathcomp.ssreflect.path]
p3:58 [in mathcomp.field.separable]
p:10 [in mathcomp.ssreflect.binomial]
p:10 [in mathcomp.field.finfield]
p:10 [in mathcomp.field.algnum]
p:10 [in mathcomp.solvable.abelian]
p:10 [in mathcomp.solvable.maximal]
p:100 [in mathcomp.field.algC]
p:100 [in mathcomp.algebra.mxpoly]
p:100 [in mathcomp.algebra.qpoly]
p:1001 [in mathcomp.algebra.polydiv]
P:1005 [in mathcomp.fingroup.fingroup]
P:1005 [in mathcomp.ssreflect.bigop]
p:1008 [in mathcomp.algebra.polydiv]
p:101 [in mathcomp.algebra.polydiv]
p:101 [in mathcomp.field.algC]
p:101 [in mathcomp.algebra.polyXY]
p:101 [in mathcomp.algebra.poly]
p:101 [in mathcomp.algebra.qpoly]
p:1010 [in mathcomp.algebra.polydiv]
p:1010 [in mathcomp.algebra.poly]
p:1011 [in mathcomp.algebra.poly]
p:1012 [in mathcomp.algebra.poly]
p:1013 [in mathcomp.algebra.polydiv]
p:1013 [in mathcomp.algebra.poly]
p:1014 [in mathcomp.algebra.poly]
P:1015 [in mathcomp.fingroup.fingroup]
p:1015 [in mathcomp.algebra.poly]
p:1016 [in mathcomp.algebra.polydiv]
p:1018 [in mathcomp.algebra.polydiv]
P:1018 [in mathcomp.ssreflect.bigop]
p:102 [in mathcomp.algebra.mxpoly]
p:1020 [in mathcomp.algebra.polydiv]
p:1022 [in mathcomp.algebra.polydiv]
p:1024 [in mathcomp.algebra.polydiv]
p:1024 [in mathcomp.algebra.mxalgebra]
p:1026 [in mathcomp.algebra.polydiv]
p:103 [in mathcomp.field.separable]
P:103 [in mathcomp.solvable.sylow]
p:103 [in mathcomp.solvable.burnside_app]
p:103 [in mathcomp.algebra.poly]
P:1036 [in mathcomp.ssreflect.bigop]
P:104 [in mathcomp.ssreflect.choice]
p:104 [in mathcomp.solvable.extremal]
P:104 [in mathcomp.solvable.nilpotent]
p:104 [in mathcomp.algebra.qpoly]
p:1040 [in mathcomp.algebra.polydiv]
p:1040 [in mathcomp.algebra.poly]
p:1041 [in mathcomp.algebra.poly]
p:1042 [in mathcomp.algebra.poly]
p:1043 [in mathcomp.algebra.polydiv]
p:1043 [in mathcomp.algebra.poly]
P:1043 [in mathcomp.ssreflect.bigop]
p:1044 [in mathcomp.algebra.poly]
p:1045 [in mathcomp.algebra.poly]
p:1046 [in mathcomp.algebra.polydiv]
p:1049 [in mathcomp.algebra.polydiv]
p:105 [in mathcomp.field.closed_field]
p:105 [in mathcomp.field.algnum]
p:105 [in mathcomp.solvable.burnside_app]
p:105 [in mathcomp.algebra.poly]
p:1052 [in mathcomp.algebra.polydiv]
p:1055 [in mathcomp.algebra.polydiv]
p:106 [in mathcomp.algebra.intdiv]
P:106 [in mathcomp.character.inertia]
p:106 [in mathcomp.solvable.sylow]
p:1065 [in mathcomp.algebra.polydiv]
p:1066 [in mathcomp.fingroup.fingroup]
p:1066 [in mathcomp.algebra.poly]
P:1066 [in mathcomp.algebra.mxalgebra]
p:1067 [in mathcomp.algebra.polydiv]
p:1069 [in mathcomp.algebra.polydiv]
p:1069 [in mathcomp.algebra.poly]
p:107 [in mathcomp.ssreflect.prime]
p:107 [in mathcomp.solvable.burnside_app]
p:1071 [in mathcomp.algebra.polydiv]
p:1073 [in mathcomp.algebra.polydiv]
P:1074 [in mathcomp.algebra.poly]
P:1074 [in mathcomp.algebra.mxalgebra]
p:1075 [in mathcomp.algebra.polydiv]
p:1077 [in mathcomp.algebra.polydiv]
p:1079 [in mathcomp.algebra.polydiv]
p:108 [in mathcomp.algebra.intdiv]
P:108 [in mathcomp.ssreflect.seq]
p:108 [in mathcomp.field.algC]
p:108 [in mathcomp.field.separable]
p:108 [in mathcomp.algebra.polyXY]
p:108 [in mathcomp.solvable.burnside_app]
p:1080 [in mathcomp.character.character]
p:1081 [in mathcomp.algebra.polydiv]
P:1083 [in mathcomp.algebra.mxalgebra]
p:1084 [in mathcomp.algebra.polydiv]
P:1084 [in mathcomp.ssreflect.finset]
p:1085 [in mathcomp.algebra.poly]
p:1087 [in mathcomp.algebra.polydiv]
P:1089 [in mathcomp.ssreflect.bigop]
p:109 [in mathcomp.ssreflect.div]
p:109 [in mathcomp.field.algC]
p:109 [in mathcomp.field.closed_field]
p:109 [in mathcomp.solvable.burnside_app]
p:1090 [in mathcomp.algebra.polydiv]
P:1091 [in mathcomp.ssreflect.finset]
p:1096 [in mathcomp.algebra.poly]
P:1097 [in mathcomp.ssreflect.finset]
p:1099 [in mathcomp.algebra.poly]
p:11 [in mathcomp.field.finfield]
p:11 [in mathcomp.algebra.polyXY]
p:11 [in mathcomp.solvable.maximal]
P:110 [in mathcomp.solvable.sylow]
p:110 [in mathcomp.ssreflect.prime]
p:110 [in mathcomp.algebra.polyXY]
p:110 [in mathcomp.solvable.extremal]
P:1100 [in mathcomp.ssreflect.bigop]
p:1102 [in mathcomp.algebra.poly]
P:1105 [in mathcomp.ssreflect.finset]
p:1105 [in mathcomp.algebra.poly]
P:1106 [in mathcomp.ssreflect.bigop]
p:1108 [in mathcomp.algebra.poly]
p:111 [in mathcomp.algebra.polydiv]
p:111 [in mathcomp.ssreflect.prime]
p:111 [in mathcomp.algebra.polyXY]
p:111 [in mathcomp.algebra.poly]
p:1110 [in mathcomp.algebra.poly]
P:1111 [in mathcomp.ssreflect.finset]
p:1111 [in mathcomp.algebra.mxalgebra]
p:1113 [in mathcomp.algebra.poly]
P:1114 [in mathcomp.ssreflect.bigop]
p:1115 [in mathcomp.algebra.poly]
p:1116 [in mathcomp.algebra.mxalgebra]
p:1117 [in mathcomp.algebra.poly]
P:1118 [in mathcomp.ssreflect.finset]
p:1118 [in mathcomp.algebra.poly]
p:1119 [in mathcomp.algebra.poly]
p:112 [in mathcomp.field.separable]
p:112 [in mathcomp.ssreflect.prime]
p:1121 [in mathcomp.ssreflect.seq]
p:1121 [in mathcomp.algebra.poly]
p:1122 [in mathcomp.algebra.poly]
p:1124 [in mathcomp.algebra.poly]
P:1125 [in mathcomp.ssreflect.finset]
P:1127 [in mathcomp.ssreflect.bigop]
p:1129 [in mathcomp.algebra.poly]
P:113 [in mathcomp.ssreflect.choice]
p:113 [in mathcomp.field.closed_field]
p:1130 [in mathcomp.algebra.poly]
p:1134 [in mathcomp.algebra.poly]
p:1136 [in mathcomp.algebra.poly]
p:1137 [in mathcomp.algebra.poly]
p:114 [in mathcomp.character.integral_char]
p:114 [in mathcomp.ssreflect.div]
p:114 [in mathcomp.algebra.polydiv]
p:1140 [in mathcomp.algebra.poly]
P:1140 [in mathcomp.ssreflect.bigop]
P:1141 [in mathcomp.fingroup.fingroup]
p:1142 [in mathcomp.algebra.poly]
P:1144 [in mathcomp.algebra.poly]
P:1146 [in mathcomp.ssreflect.seq]
P:1148 [in mathcomp.algebra.ssralg]
p:115 [in mathcomp.character.integral_char]
p:115 [in mathcomp.algebra.polydiv]
p:115 [in mathcomp.field.separable]
p:115 [in mathcomp.character.inertia]
p:115 [in mathcomp.field.closed_field]
P:1151 [in mathcomp.ssreflect.bigop]
P:1152 [in mathcomp.fingroup.fingroup]
p:116 [in mathcomp.ssreflect.binomial]
P:116 [in mathcomp.ssreflect.choice]
p:116 [in mathcomp.field.algC]
p:116 [in mathcomp.field.finfield]
p:116 [in mathcomp.solvable.abelian]
P:116 [in mathcomp.solvable.nilpotent]
P:1160 [in mathcomp.ssreflect.finset]
P:1161 [in mathcomp.ssreflect.bigop]
p:1165 [in mathcomp.character.mxrepresentation]
p:1166 [in mathcomp.algebra.mxalgebra]
P:1167 [in mathcomp.ssreflect.finset]
p:1169 [in mathcomp.algebra.poly]
p:117 [in mathcomp.ssreflect.div]
p:117 [in mathcomp.ssreflect.prime]
p:117 [in mathcomp.algebra.poly]
p:1170 [in mathcomp.algebra.mxalgebra]
p:1173 [in mathcomp.ssreflect.ssrnat]
P:1173 [in mathcomp.ssreflect.finset]
P:1173 [in mathcomp.algebra.ssrnum]
P:1173 [in mathcomp.algebra.poly]
p:1174 [in mathcomp.algebra.mxalgebra]
p:1178 [in mathcomp.algebra.mxalgebra]
P:118 [in mathcomp.ssreflect.choice]
p:118 [in mathcomp.ssreflect.ssrnat]
p:118 [in mathcomp.field.algC]
p:118 [in mathcomp.field.fieldext]
p:118 [in mathcomp.field.closed_field]
p:118 [in mathcomp.ssreflect.prime]
p:118 [in mathcomp.solvable.abelian]
P:1180 [in mathcomp.ssreflect.finset]
P:1180 [in mathcomp.algebra.poly]
p:1182 [in mathcomp.algebra.mxalgebra]
p:1186 [in mathcomp.algebra.poly]
P:1188 [in mathcomp.ssreflect.finset]
P:1188 [in mathcomp.algebra.ssrnum]
p:1188 [in mathcomp.algebra.poly]
p:1189 [in mathcomp.ssreflect.ssrnat]
p:119 [in mathcomp.algebra.intdiv]
p:119 [in mathcomp.ssreflect.prime]
P:1195 [in mathcomp.ssreflect.bigop]
P:1198 [in mathcomp.ssreflect.finset]
p:1198 [in mathcomp.algebra.poly]
p:12 [in mathcomp.algebra.mxpoly]
p:12 [in mathcomp.solvable.maximal]
p:120 [in mathcomp.ssreflect.div]
p:120 [in mathcomp.field.algC]
p:120 [in mathcomp.field.fieldext]
p:120 [in mathcomp.solvable.abelian]
p:1200 [in mathcomp.algebra.poly]
p:1203 [in mathcomp.ssreflect.ssrnat]
p:1203 [in mathcomp.algebra.poly]
p:1204 [in mathcomp.ssreflect.ssrnat]
p:1205 [in mathcomp.algebra.poly]
p:1206 [in mathcomp.ssreflect.ssrnat]
p:1207 [in mathcomp.algebra.poly]
p:1209 [in mathcomp.algebra.poly]
p:121 [in mathcomp.algebra.polydiv]
P:121 [in mathcomp.ssreflect.choice]
p:121 [in mathcomp.ssreflect.ssrnat]
p:121 [in mathcomp.field.fieldext]
p:121 [in mathcomp.ssreflect.prime]
p:121 [in mathcomp.solvable.abelian]
p:1211 [in mathcomp.algebra.poly]
P:1212 [in mathcomp.ssreflect.seq]
P:1214 [in mathcomp.algebra.mxalgebra]
P:1217 [in mathcomp.ssreflect.bigop]
P:1219 [in mathcomp.ssreflect.seq]
p:122 [in mathcomp.algebra.polydiv]
p:122 [in mathcomp.field.fieldext]
p:122 [in mathcomp.solvable.sylow]
p:1221 [in mathcomp.algebra.poly]
p:1222 [in mathcomp.algebra.poly]
p:1223 [in mathcomp.algebra.poly]
p:1224 [in mathcomp.algebra.poly]
p:1225 [in mathcomp.algebra.poly]
P:1226 [in mathcomp.algebra.mxalgebra]
p:1227 [in mathcomp.algebra.poly]
P:1227 [in mathcomp.algebra.mxalgebra]
p:123 [in mathcomp.algebra.intdiv]
p:123 [in mathcomp.algebra.polydiv]
P:123 [in mathcomp.solvable.sylow]
p:123 [in mathcomp.ssreflect.prime]
p:123 [in mathcomp.solvable.abelian]
P:1238 [in mathcomp.algebra.ssralg]
p:1239 [in mathcomp.algebra.poly]
p:124 [in mathcomp.solvable.sylow]
p:124 [in mathcomp.solvable.burnside_app]
p:124 [in mathcomp.solvable.maximal]
p:1245 [in mathcomp.algebra.poly]
p:1247 [in mathcomp.algebra.poly]
P:1248 [in mathcomp.algebra.ssralg]
p:125 [in mathcomp.fingroup.perm]
p:125 [in mathcomp.ssreflect.div]
p:125 [in mathcomp.algebra.polydiv]
P:125 [in mathcomp.solvable.sylow]
p:125 [in mathcomp.ssreflect.prime]
P:1252 [in mathcomp.ssreflect.bigop]
p:1253 [in mathcomp.algebra.poly]
p:1257 [in mathcomp.ssreflect.order]
P:1259 [in mathcomp.algebra.matrix]
p:126 [in mathcomp.solvable.abelian]
P:1260 [in mathcomp.ssreflect.finset]
P:1265 [in mathcomp.ssreflect.bigop]
P:1266 [in mathcomp.ssreflect.finset]
p:127 [in mathcomp.field.fieldext]
p:127 [in mathcomp.algebra.mxpoly]
p:127 [in mathcomp.ssreflect.prime]
P:127 [in mathcomp.character.character]
P:1271 [in mathcomp.ssreflect.finset]
P:1271 [in mathcomp.algebra.matrix]
P:1277 [in mathcomp.ssreflect.finset]
P:1277 [in mathcomp.ssreflect.bigop]
p:128 [in mathcomp.ssreflect.div]
p:128 [in mathcomp.ssreflect.ssrnat]
p:128 [in mathcomp.field.fieldext]
p:128 [in mathcomp.algebra.qpoly]
P:1280 [in mathcomp.ssreflect.finset]
P:1282 [in mathcomp.algebra.mxalgebra]
P:1284 [in mathcomp.ssreflect.order]
P:1287 [in mathcomp.ssreflect.finset]
P:1288 [in mathcomp.algebra.matrix]
P:1288 [in mathcomp.ssreflect.bigop]
p:129 [in mathcomp.field.fieldext]
p:129 [in mathcomp.solvable.abelian]
p:129 [in mathcomp.solvable.burnside_app]
p:129 [in mathcomp.solvable.maximal]
p:129 [in mathcomp.algebra.qpoly]
P:1291 [in mathcomp.ssreflect.order]
P:1298 [in mathcomp.ssreflect.bigop]
p:13 [in mathcomp.field.separable]
p:13 [in mathcomp.ssreflect.path]
p:13 [in mathcomp.algebra.polyXY]
p:13 [in mathcomp.solvable.abelian]
P:13 [in mathcomp.algebra.rat]
p:130 [in mathcomp.field.fieldext]
p:130 [in mathcomp.ssreflect.prime]
p:130 [in mathcomp.algebra.qpoly]
P:1300 [in mathcomp.algebra.matrix]
P:1301 [in mathcomp.ssreflect.finset]
P:1308 [in mathcomp.ssreflect.finset]
P:1308 [in mathcomp.ssreflect.bigop]
p:131 [in mathcomp.ssreflect.div]
p:131 [in mathcomp.solvable.abelian]
p:131 [in mathcomp.algebra.qpoly]
p:1315 [in mathcomp.algebra.poly]
P:1319 [in mathcomp.ssreflect.finset]
p:132 [in mathcomp.algebra.polydiv]
p:132 [in mathcomp.solvable.pgroup]
p:132 [in mathcomp.solvable.cyclic]
p:1322 [in mathcomp.algebra.poly]
P:1322 [in mathcomp.ssreflect.bigop]
p:1329 [in mathcomp.algebra.poly]
P:133 [in mathcomp.ssreflect.prime]
p:133 [in mathcomp.solvable.maximal]
p:133 [in mathcomp.algebra.qpoly]
p:1332 [in mathcomp.algebra.poly]
P:1334 [in mathcomp.ssreflect.finset]
p:1335 [in mathcomp.algebra.poly]
P:1335 [in mathcomp.ssreflect.bigop]
P:1336 [in mathcomp.ssreflect.finset]
p:1337 [in mathcomp.algebra.poly]
p:1338 [in mathcomp.ssreflect.seq]
P:1338 [in mathcomp.ssreflect.finset]
p:1339 [in mathcomp.algebra.poly]
p:134 [in mathcomp.field.separable]
p:134 [in mathcomp.solvable.abelian]
p:134 [in mathcomp.algebra.qpoly]
P:1340 [in mathcomp.ssreflect.finset]
P:1341 [in mathcomp.algebra.ssrnum]
P:1342 [in mathcomp.ssreflect.finset]
P:1344 [in mathcomp.ssreflect.finset]
P:1345 [in mathcomp.ssreflect.bigop]
P:1346 [in mathcomp.ssreflect.finset]
P:1348 [in mathcomp.ssreflect.finset]
P:135 [in mathcomp.solvable.pgroup]
p:135 [in mathcomp.ssreflect.prime]
p:135 [in mathcomp.solvable.burnside_app]
P:1350 [in mathcomp.ssreflect.finset]
P:1353 [in mathcomp.ssreflect.finset]
P:1354 [in mathcomp.algebra.ssralg]
P:1356 [in mathcomp.ssreflect.finset]
P:1356 [in mathcomp.algebra.ssrnum]
P:1356 [in mathcomp.ssreflect.bigop]
p:136 [in mathcomp.field.fieldext]
p:136 [in mathcomp.solvable.abelian]
p:136 [in mathcomp.solvable.burnside_app]
P:136 [in mathcomp.solvable.hall]
p:136 [in mathcomp.algebra.qpoly]
P:1360 [in mathcomp.ssreflect.finset]
P:1366 [in mathcomp.ssreflect.bigop]
p:137 [in mathcomp.field.galois]
p:137 [in mathcomp.solvable.burnside_app]
P:137 [in mathcomp.solvable.hall]
P:137 [in mathcomp.ssreflect.bigop]
P:1371 [in mathcomp.ssreflect.finset]
P:1374 [in mathcomp.ssreflect.finset]
P:1376 [in mathcomp.ssreflect.finset]
P:1377 [in mathcomp.ssreflect.bigop]
P:1378 [in mathcomp.ssreflect.finset]
p:138 [in mathcomp.field.algnum]
p:138 [in mathcomp.solvable.abelian]
p:138 [in mathcomp.solvable.burnside_app]
P:1380 [in mathcomp.algebra.ssrnum]
P:1381 [in mathcomp.ssreflect.finset]
P:1383 [in mathcomp.ssreflect.finset]
p:1384 [in mathcomp.ssreflect.seq]
P:1386 [in mathcomp.ssreflect.finset]
P:1388 [in mathcomp.ssreflect.bigop]
P:1389 [in mathcomp.ssreflect.finset]
P:139 [in mathcomp.character.vcharacter]
P:1392 [in mathcomp.ssreflect.finset]
P:1393 [in mathcomp.ssreflect.finset]
P:1399 [in mathcomp.ssreflect.bigop]
p:14 [in mathcomp.algebra.polydiv]
p:14 [in mathcomp.field.galois]
p:14 [in mathcomp.field.qfpoly]
p:140 [in mathcomp.solvable.burnside_app]
P:140 [in mathcomp.solvable.hall]
P:1401 [in mathcomp.ssreflect.finset]
P:1402 [in mathcomp.algebra.mxalgebra]
P:1404 [in mathcomp.ssreflect.finset]
p:141 [in mathcomp.field.finfield]
p:141 [in mathcomp.solvable.abelian]
P:141 [in mathcomp.solvable.hall]
P:1410 [in mathcomp.ssreflect.order]
P:1411 [in mathcomp.ssreflect.bigop]
P:1413 [in mathcomp.ssreflect.finset]
p:142 [in mathcomp.ssreflect.div]
P:142 [in mathcomp.solvable.hall]
P:1420 [in mathcomp.ssreflect.order]
P:1426 [in mathcomp.ssreflect.finset]
P:1428 [in mathcomp.ssreflect.order]
P:1436 [in mathcomp.ssreflect.order]
P:1438 [in mathcomp.ssreflect.finset]
p:144 [in mathcomp.ssreflect.div]
p:144 [in mathcomp.algebra.polydiv]
p:144 [in mathcomp.ssreflect.prime]
p:144 [in mathcomp.solvable.abelian]
p:144 [in mathcomp.algebra.poly]
P:144 [in mathcomp.solvable.nilpotent]
P:1445 [in mathcomp.ssreflect.order]
P:1446 [in mathcomp.ssreflect.finset]
p:145 [in mathcomp.algebra.polydiv]
p:145 [in mathcomp.ssreflect.prime]
P:1453 [in mathcomp.ssreflect.finset]
P:1454 [in mathcomp.ssreflect.order]
p:146 [in mathcomp.field.fieldext]
p:146 [in mathcomp.solvable.sylow]
P:146 [in mathcomp.solvable.hall]
P:1462 [in mathcomp.ssreflect.finset]
P:1463 [in mathcomp.ssreflect.order]
p:1464 [in mathcomp.ssreflect.bigop]
P:1465 [in mathcomp.ssreflect.bigop]
p:147 [in mathcomp.field.fieldext]
P:1472 [in mathcomp.ssreflect.order]
P:1478 [in mathcomp.ssreflect.bigop]
p:148 [in mathcomp.algebra.polydiv]
p:148 [in mathcomp.field.galois]
P:148 [in mathcomp.solvable.sylow]
p:148 [in mathcomp.solvable.abelian]
p:148 [in mathcomp.algebra.qpoly]
P:1484 [in mathcomp.ssreflect.order]
p:1489 [in mathcomp.character.mxrepresentation]
p:149 [in mathcomp.algebra.polydiv]
p:149 [in mathcomp.field.galois]
p:1490 [in mathcomp.character.mxrepresentation]
p:1491 [in mathcomp.character.mxrepresentation]
P:1492 [in mathcomp.ssreflect.bigop]
P:1496 [in mathcomp.ssreflect.order]
p:15 [in mathcomp.field.qfpoly]
p:15 [in mathcomp.algebra.poly]
P:150 [in mathcomp.ssreflect.ssrnat]
p:150 [in mathcomp.solvable.sylow]
p:150 [in mathcomp.field.finfield]
p:150 [in mathcomp.algebra.poly]
P:1503 [in mathcomp.ssreflect.bigop]
P:1504 [in mathcomp.ssreflect.order]
p:151 [in mathcomp.algebra.archimedean]
p:151 [in mathcomp.algebra.polydiv]
P:151 [in mathcomp.solvable.sylow]
p:151 [in mathcomp.field.finfield]
p:151 [in mathcomp.algebra.qpoly]
P:1510 [in mathcomp.ssreflect.finset]
P:1512 [in mathcomp.ssreflect.order]
P:1514 [in mathcomp.ssreflect.finset]
p:152 [in mathcomp.algebra.polydiv]
p:152 [in mathcomp.solvable.abelian]
p:152 [in mathcomp.field.falgebra]
P:1520 [in mathcomp.ssreflect.order]
p:1524 [in mathcomp.algebra.matrix]
P:1527 [in mathcomp.ssreflect.finset]
P:1529 [in mathcomp.ssreflect.finset]
P:1529 [in mathcomp.ssreflect.order]
p:153 [in mathcomp.algebra.qpoly]
p:1534 [in mathcomp.algebra.matrix]
P:1536 [in mathcomp.ssreflect.bigop]
p:1537 [in mathcomp.ssreflect.bigop]
p:1541 [in mathcomp.algebra.matrix]
P:1541 [in mathcomp.ssreflect.order]
p:1545 [in mathcomp.algebra.matrix]
p:1549 [in mathcomp.algebra.matrix]
p:155 [in mathcomp.ssreflect.div]
p:155 [in mathcomp.algebra.polydiv]
p:155 [in mathcomp.solvable.abelian]
p:155 [in mathcomp.ssreflect.eqtype]
p:155 [in mathcomp.algebra.qpoly]
P:1553 [in mathcomp.ssreflect.finset]
p:1555 [in mathcomp.algebra.matrix]
P:1559 [in mathcomp.ssreflect.order]
p:156 [in mathcomp.field.algebraics_fundamentals]
p:156 [in mathcomp.field.algC]
p:156 [in mathcomp.solvable.abelian]
p:156 [in mathcomp.algebra.poly]
p:1560 [in mathcomp.algebra.ssrnum]
P:1561 [in mathcomp.ssreflect.finset]
p:1561 [in mathcomp.algebra.matrix]
P:1561 [in mathcomp.ssreflect.bigop]
P:1565 [in mathcomp.algebra.matrix]
p:157 [in mathcomp.solvable.abelian]
p:157 [in mathcomp.algebra.qpoly]
p:1571 [in mathcomp.algebra.mxalgebra]
P:1572 [in mathcomp.ssreflect.order]
P:1573 [in mathcomp.ssreflect.finset]
p:1573 [in mathcomp.ssreflect.bigop]
p:1574 [in mathcomp.ssreflect.bigop]
p:1575 [in mathcomp.algebra.matrix]
p:1575 [in mathcomp.ssreflect.bigop]
P:1579 [in mathcomp.algebra.matrix]
P:158 [in mathcomp.algebra.polydiv]
p:158 [in mathcomp.algebra.poly]
P:1581 [in mathcomp.ssreflect.finset]
P:1582 [in mathcomp.ssreflect.bigop]
P:1584 [in mathcomp.ssreflect.finset]
P:1586 [in mathcomp.ssreflect.finset]
P:1586 [in mathcomp.ssreflect.order]
P:1589 [in mathcomp.ssreflect.finset]
P:159 [in mathcomp.ssreflect.binomial]
p:159 [in mathcomp.ssreflect.div]
p:159 [in mathcomp.field.algC]
p:159 [in mathcomp.ssreflect.eqtype]
p:1591 [in mathcomp.ssreflect.bigop]
p:1592 [in mathcomp.ssreflect.bigop]
p:1593 [in mathcomp.ssreflect.bigop]
p:1595 [in mathcomp.ssreflect.seq]
P:1596 [in mathcomp.ssreflect.finset]
P:1598 [in mathcomp.ssreflect.order]
p:16 [in mathcomp.algebra.polydiv]
p:16 [in mathcomp.field.separable]
p:16 [in mathcomp.ssreflect.path]
p:16 [in mathcomp.field.algnum]
p:16 [in mathcomp.solvable.abelian]
p:160 [in mathcomp.field.algebraics_fundamentals]
p:160 [in mathcomp.solvable.abelian]
p:160 [in mathcomp.algebra.poly]
P:1600 [in mathcomp.ssreflect.bigop]
P:1601 [in mathcomp.ssreflect.finset]
p:1601 [in mathcomp.algebra.matrix]
P:1604 [in mathcomp.algebra.mxalgebra]
P:1607 [in mathcomp.ssreflect.finset]
p:1609 [in mathcomp.algebra.matrix]
p:1609 [in mathcomp.ssreflect.bigop]
P:1610 [in mathcomp.ssreflect.finset]
P:1610 [in mathcomp.ssreflect.order]
p:1610 [in mathcomp.ssreflect.bigop]
p:1611 [in mathcomp.ssreflect.bigop]
P:1613 [in mathcomp.ssreflect.finset]
P:1616 [in mathcomp.ssreflect.finset]
p:1617 [in mathcomp.algebra.matrix]
P:1618 [in mathcomp.ssreflect.finset]
P:162 [in mathcomp.algebra.mxpoly]
p:162 [in mathcomp.algebra.poly]
P:1621 [in mathcomp.ssreflect.finset]
p:1621 [in mathcomp.ssreflect.bigop]
p:1622 [in mathcomp.ssreflect.bigop]
p:1623 [in mathcomp.ssreflect.bigop]
p:1624 [in mathcomp.algebra.matrix]
P:1625 [in mathcomp.ssreflect.finset]
P:1625 [in mathcomp.ssreflect.order]
P:1628 [in mathcomp.ssreflect.bigop]
p:163 [in mathcomp.solvable.abelian]
p:163 [in mathcomp.algebra.qpoly]
p:1630 [in mathcomp.algebra.matrix]
p:1637 [in mathcomp.algebra.matrix]
P:1639 [in mathcomp.ssreflect.order]
P:164 [in mathcomp.algebra.ssralg]
p:1643 [in mathcomp.algebra.matrix]
p:165 [in mathcomp.ssreflect.prime]
P:165 [in mathcomp.ssreflect.bigop]
P:1651 [in mathcomp.ssreflect.bigop]
P:1652 [in mathcomp.ssreflect.order]
p:166 [in mathcomp.algebra.polydiv]
p:166 [in mathcomp.ssreflect.ssrnat]
P:166 [in mathcomp.algebra.mxpoly]
P:166 [in mathcomp.algebra.poly]
p:166 [in mathcomp.algebra.qpoly]
P:1667 [in mathcomp.ssreflect.order]
P:167 [in mathcomp.ssreflect.choice]
P:167 [in mathcomp.fingroup.fingroup]
p:167 [in mathcomp.solvable.abelian]
P:1670 [in mathcomp.ssreflect.bigop]
P:168 [in mathcomp.fingroup.quotient]
p:168 [in mathcomp.ssreflect.binomial]
P:168 [in mathcomp.solvable.sylow]
p:168 [in mathcomp.ssreflect.prime]
p:168 [in mathcomp.algebra.qpoly]
p:1680 [in mathcomp.algebra.matrix]
P:1680 [in mathcomp.ssreflect.order]
p:1686 [in mathcomp.algebra.matrix]
p:169 [in mathcomp.algebra.polydiv]
p:169 [in mathcomp.ssreflect.ssrnat]
p:169 [in mathcomp.field.closed_field]
p:1692 [in mathcomp.algebra.matrix]
p:1692 [in mathcomp.algebra.ssralg]
P:1693 [in mathcomp.ssreflect.order]
p:1693 [in mathcomp.algebra.ssralg]
P:1693 [in mathcomp.ssreflect.bigop]
p:1694 [in mathcomp.algebra.ssralg]
P:1695 [in mathcomp.ssreflect.seq]
P:1699 [in mathcomp.ssreflect.seq]
p:17 [in mathcomp.solvable.pgroup]
p:17 [in mathcomp.field.algnum]
p:17 [in mathcomp.algebra.poly]
p:170 [in mathcomp.algebra.polydiv]
p:170 [in mathcomp.ssreflect.prime]
p:170 [in mathcomp.solvable.abelian]
P:1703 [in mathcomp.algebra.ssralg]
P:1708 [in mathcomp.ssreflect.order]
p:171 [in mathcomp.ssreflect.binomial]
p:171 [in mathcomp.algebra.polydiv]
p:171 [in mathcomp.ssreflect.prime]
P:171 [in mathcomp.ssreflect.fintype]
p:172 [in mathcomp.ssreflect.ssrnat]
p:172 [in mathcomp.algebra.qpoly]
P:1721 [in mathcomp.ssreflect.order]
P:1723 [in mathcomp.ssreflect.bigop]
P:1727 [in mathcomp.algebra.ssralg]
p:173 [in mathcomp.algebra.polydiv]
p:173 [in mathcomp.ssreflect.fingraph]
P:1732 [in mathcomp.ssreflect.order]
P:1734 [in mathcomp.ssreflect.bigop]
P:1736 [in mathcomp.algebra.ssralg]
p:174 [in mathcomp.ssreflect.prime]
p:174 [in mathcomp.solvable.abelian]
P:174 [in mathcomp.algebra.ssralg]
p:174 [in mathcomp.ssreflect.eqtype]
p:174 [in mathcomp.algebra.qpoly]
P:1743 [in mathcomp.ssreflect.order]
P:1744 [in mathcomp.ssreflect.bigop]
P:1745 [in mathcomp.algebra.ssralg]
p:175 [in mathcomp.algebra.polydiv]
p:175 [in mathcomp.ssreflect.ssrnat]
p:175 [in mathcomp.ssreflect.fingraph]
p:175 [in mathcomp.algebra.poly]
p:175 [in mathcomp.algebra.qpoly]
P:1750 [in mathcomp.ssreflect.bigop]
P:1753 [in mathcomp.algebra.ssralg]
P:1756 [in mathcomp.ssreflect.order]
P:1758 [in mathcomp.ssreflect.bigop]
P:176 [in mathcomp.ssreflect.choice]
P:176 [in mathcomp.solvable.sylow]
p:176 [in mathcomp.field.finfield]
p:176 [in mathcomp.ssreflect.eqtype]
p:176 [in mathcomp.algebra.qpoly]
p:176 [in mathcomp.algebra.mxalgebra]
p:1766 [in mathcomp.algebra.ssralg]
p:177 [in mathcomp.algebra.polydiv]
p:177 [in mathcomp.algebra.mxpoly]
P:177 [in mathcomp.solvable.sylow]
p:177 [in mathcomp.ssreflect.prime]
p:177 [in mathcomp.ssreflect.fingraph]
P:1770 [in mathcomp.ssreflect.order]
P:1772 [in mathcomp.ssreflect.bigop]
p:1779 [in mathcomp.algebra.matrix]
p:178 [in mathcomp.solvable.abelian]
p:178 [in mathcomp.algebra.poly]
p:178 [in mathcomp.algebra.qpoly]
P:1782 [in mathcomp.ssreflect.bigop]
p:1784 [in mathcomp.algebra.matrix]
P:1786 [in mathcomp.ssreflect.order]
p:179 [in mathcomp.algebra.mxpoly]
P:1793 [in mathcomp.ssreflect.bigop]
p:18 [in mathcomp.algebra.polydiv]
p:18 [in mathcomp.algebra.qpoly]
P:180 [in mathcomp.ssreflect.choice]
p:180 [in mathcomp.ssreflect.prime]
P:180 [in mathcomp.algebra.ssrnum]
p:180 [in mathcomp.algebra.qpoly]
p:1802 [in mathcomp.algebra.matrix]
P:1802 [in mathcomp.ssreflect.order]
P:1804 [in mathcomp.ssreflect.bigop]
p:1809 [in mathcomp.algebra.matrix]
p:181 [in mathcomp.algebra.polydiv]
p:181 [in mathcomp.algebra.mxpoly]
p:181 [in mathcomp.ssreflect.prime]
p:181 [in mathcomp.algebra.mxalgebra]
P:1815 [in mathcomp.ssreflect.bigop]
p:182 [in mathcomp.solvable.abelian]
p:1822 [in mathcomp.algebra.ssrnum]
P:1825 [in mathcomp.ssreflect.order]
P:1827 [in mathcomp.ssreflect.bigop]
p:183 [in mathcomp.algebra.polydiv]
P:1837 [in mathcomp.algebra.ssralg]
p:1838 [in mathcomp.algebra.matrix]
p:184 [in mathcomp.ssreflect.prime]
p:184 [in mathcomp.solvable.abelian]
p:184 [in mathcomp.algebra.poly]
P:1847 [in mathcomp.ssreflect.order]
P:1847 [in mathcomp.algebra.ssralg]
p:185 [in mathcomp.algebra.polydiv]
p:185 [in mathcomp.field.closed_field]
p:185 [in mathcomp.ssreflect.prime]
P:1852 [in mathcomp.ssreflect.order]
P:1857 [in mathcomp.ssreflect.order]
p:1861 [in mathcomp.algebra.matrix]
P:1863 [in mathcomp.ssreflect.order]
p:1867 [in mathcomp.algebra.matrix]
P:1872 [in mathcomp.ssreflect.order]
p:1874 [in mathcomp.algebra.matrix]
p:188 [in mathcomp.algebra.polydiv]
p:188 [in mathcomp.ssreflect.ssrnat]
P:188 [in mathcomp.solvable.pgroup]
p:188 [in mathcomp.solvable.abelian]
p:188 [in mathcomp.ssreflect.fingraph]
p:188 [in mathcomp.solvable.burnside_app]
p:188 [in mathcomp.algebra.poly]
p:1880 [in mathcomp.algebra.matrix]
P:1881 [in mathcomp.ssreflect.order]
P:1886 [in mathcomp.ssreflect.bigop]
P:1889 [in mathcomp.algebra.ssralg]
p:189 [in mathcomp.algebra.polydiv]
p:189 [in mathcomp.field.closed_field]
p:189 [in mathcomp.solvable.burnside_app]
P:189 [in mathcomp.character.character]
P:1890 [in mathcomp.ssreflect.order]
P:1896 [in mathcomp.ssreflect.order]
P:1898 [in mathcomp.ssreflect.bigop]
p:19 [in mathcomp.ssreflect.choice]
p:19 [in mathcomp.field.separable]
P:19 [in mathcomp.solvable.pgroup]
p:19 [in mathcomp.ssreflect.path]
p:19 [in mathcomp.algebra.poly]
p:190 [in mathcomp.algebra.mxpoly]
p:190 [in mathcomp.algebra.poly]
p:1904 [in mathcomp.algebra.matrix]
p:1909 [in mathcomp.ssreflect.bigop]
p:191 [in mathcomp.character.integral_char]
p:191 [in mathcomp.algebra.polydiv]
p:191 [in mathcomp.ssreflect.ssrnat]
P:191 [in mathcomp.solvable.pgroup]
p:191 [in mathcomp.ssreflect.prime]
P:1910 [in mathcomp.ssreflect.bigop]
P:1912 [in mathcomp.ssreflect.order]
P:1919 [in mathcomp.ssreflect.order]
p:192 [in mathcomp.field.closed_field]
p:192 [in mathcomp.algebra.poly]
P:1924 [in mathcomp.ssreflect.bigop]
P:1926 [in mathcomp.ssreflect.order]
P:193 [in mathcomp.character.integral_char]
p:193 [in mathcomp.algebra.polydiv]
p:193 [in mathcomp.solvable.pgroup]
p:193 [in mathcomp.ssreflect.prime]
P:1933 [in mathcomp.ssreflect.order]
P:1936 [in mathcomp.ssreflect.bigop]
p:194 [in mathcomp.solvable.abelian]
p:194 [in mathcomp.algebra.poly]
P:1940 [in mathcomp.ssreflect.order]
P:1947 [in mathcomp.ssreflect.order]
p:195 [in mathcomp.algebra.intdiv]
p:195 [in mathcomp.algebra.mxpoly]
p:195 [in mathcomp.field.closed_field]
P:195 [in mathcomp.solvable.pgroup]
P:1952 [in mathcomp.ssreflect.bigop]
P:1954 [in mathcomp.ssreflect.order]
P:196 [in mathcomp.algebra.ssrint]
p:196 [in mathcomp.ssreflect.prime]
P:1961 [in mathcomp.algebra.matrix]
P:1963 [in mathcomp.ssreflect.order]
P:197 [in mathcomp.algebra.ssrnum]
P:1972 [in mathcomp.ssreflect.order]
p:198 [in mathcomp.algebra.intdiv]
p:198 [in mathcomp.field.closed_field]
p:198 [in mathcomp.ssreflect.prime]
p:198 [in mathcomp.solvable.abelian]
p:198 [in mathcomp.solvable.burnside_app]
p:198 [in mathcomp.algebra.poly]
P:1981 [in mathcomp.ssreflect.order]
P:1989 [in mathcomp.ssreflect.order]
p:199 [in mathcomp.ssreflect.binomial]
p:199 [in mathcomp.solvable.burnside_app]
p:199 [in mathcomp.algebra.poly]
P:1999 [in mathcomp.ssreflect.order]
P:1999 [in mathcomp.algebra.ssralg]
p:2 [in mathcomp.solvable.alt]
p:2 [in mathcomp.field.separable]
P:20 [in mathcomp.ssreflect.generic_quotient]
p:20 [in mathcomp.algebra.polydiv]
p:20 [in mathcomp.field.algnum]
p:20 [in mathcomp.ssreflect.fingraph]
p:20 [in mathcomp.algebra.qpoly]
p:200 [in mathcomp.ssreflect.ssrnat]
P:200 [in mathcomp.character.classfun]
p:200 [in mathcomp.ssreflect.prime]
P:200 [in mathcomp.ssreflect.fintype]
P:2002 [in mathcomp.ssreflect.bigop]
p:201 [in mathcomp.ssreflect.binomial]
p:201 [in mathcomp.algebra.intdiv]
p:201 [in mathcomp.field.closed_field]
p:201 [in mathcomp.ssreflect.prime]
P:201 [in mathcomp.ssreflect.fintype]
P:2015 [in mathcomp.ssreflect.bigop]
p:202 [in mathcomp.algebra.intdiv]
p:202 [in mathcomp.ssreflect.prime]
p:202 [in mathcomp.algebra.poly]
P:2028 [in mathcomp.ssreflect.bigop]
p:203 [in mathcomp.ssreflect.binomial]
p:203 [in mathcomp.field.galois]
P:203 [in mathcomp.solvable.pgroup]
p:203 [in mathcomp.solvable.abelian]
P:203 [in mathcomp.solvable.nilpotent]
p:2030 [in mathcomp.algebra.matrix]
p:2037 [in mathcomp.algebra.matrix]
p:204 [in mathcomp.field.galois]
p:204 [in mathcomp.solvable.pgroup]
p:204 [in mathcomp.ssreflect.prime]
p:205 [in mathcomp.algebra.intdiv]
p:205 [in mathcomp.field.galois]
p:205 [in mathcomp.algebra.mxpoly]
p:205 [in mathcomp.solvable.pgroup]
p:206 [in mathcomp.algebra.polydiv]
p:206 [in mathcomp.field.algnum]
P:2061 [in mathcomp.ssreflect.bigop]
P:207 [in mathcomp.algebra.ssrint]
p:207 [in mathcomp.ssreflect.prime]
p:207 [in mathcomp.solvable.abelian]
P:207 [in mathcomp.algebra.ssrnum]
P:207 [in mathcomp.algebra.poly]
P:2072 [in mathcomp.ssreflect.bigop]
p:208 [in mathcomp.algebra.intdiv]
p:208 [in mathcomp.algebra.polydiv]
P:2082 [in mathcomp.ssreflect.bigop]
P:209 [in mathcomp.field.separable]
p:209 [in mathcomp.ssreflect.prime]
P:2092 [in mathcomp.ssreflect.bigop]
p:21 [in mathcomp.field.separable]
p:21 [in mathcomp.field.algnum]
p:210 [in mathcomp.algebra.polydiv]
p:210 [in mathcomp.solvable.burnside_app]
P:2107 [in mathcomp.ssreflect.bigop]
p:211 [in mathcomp.algebra.intdiv]
p:211 [in mathcomp.ssreflect.prime]
p:211 [in mathcomp.solvable.abelian]
p:211 [in mathcomp.solvable.burnside_app]
p:212 [in mathcomp.algebra.polydiv]
P:212 [in mathcomp.algebra.vector]
P:2120 [in mathcomp.ssreflect.bigop]
p:214 [in mathcomp.algebra.intdiv]
p:214 [in mathcomp.solvable.abelian]
p:214 [in mathcomp.solvable.cyclic]
p:2146 [in mathcomp.algebra.matrix]
p:215 [in mathcomp.ssreflect.prime]
P:215 [in mathcomp.algebra.ssrnum]
P:215 [in mathcomp.solvable.nilpotent]
p:2151 [in mathcomp.algebra.matrix]
P:2155 [in mathcomp.ssreflect.bigop]
p:2156 [in mathcomp.algebra.matrix]
p:2156 [in mathcomp.ssreflect.bigop]
p:2162 [in mathcomp.algebra.matrix]
p:2168 [in mathcomp.algebra.matrix]
p:217 [in mathcomp.algebra.intdiv]
p:217 [in mathcomp.ssreflect.ssrnat]
p:217 [in mathcomp.ssreflect.prime]
P:217 [in mathcomp.character.mxrepresentation]
p:218 [in mathcomp.algebra.polydiv]
p:218 [in mathcomp.field.closed_field]
p:218 [in mathcomp.algebra.mxalgebra]
P:219 [in mathcomp.ssreflect.choice]
p:219 [in mathcomp.ssreflect.prime]
p:219 [in mathcomp.solvable.abelian]
p:22 [in mathcomp.algebra.polydiv]
p:22 [in mathcomp.ssreflect.ssrnat]
p:22 [in mathcomp.algebra.mxpoly]
p:22 [in mathcomp.field.qfpoly]
p:22 [in mathcomp.ssreflect.path]
p:22 [in mathcomp.algebra.polyXY]
p:22 [in mathcomp.field.algnum]
p:22 [in mathcomp.algebra.poly]
p:22 [in mathcomp.algebra.qpoly]
p:220 [in mathcomp.algebra.polydiv]
p:220 [in mathcomp.ssreflect.ssrnat]
P:2205 [in mathcomp.ssreflect.bigop]
P:221 [in mathcomp.field.separable]
p:221 [in mathcomp.algebra.mxpoly]
p:221 [in mathcomp.field.closed_field]
p:221 [in mathcomp.solvable.burnside_app]
p:2212 [in mathcomp.algebra.matrix]
p:2217 [in mathcomp.ssreflect.bigop]
p:2218 [in mathcomp.ssreflect.bigop]
p:2219 [in mathcomp.ssreflect.bigop]
p:222 [in mathcomp.algebra.polydiv]
p:222 [in mathcomp.ssreflect.prime]
p:222 [in mathcomp.solvable.burnside_app]
P:2222 [in mathcomp.ssreflect.bigop]
p:223 [in mathcomp.ssreflect.ssrnat]
p:223 [in mathcomp.solvable.abelian]
p:2231 [in mathcomp.ssreflect.bigop]
p:2232 [in mathcomp.ssreflect.bigop]
P:2233 [in mathcomp.ssreflect.order]
p:2233 [in mathcomp.ssreflect.bigop]
P:2236 [in mathcomp.ssreflect.order]
P:2236 [in mathcomp.ssreflect.bigop]
P:2239 [in mathcomp.algebra.ssralg]
p:224 [in mathcomp.algebra.polydiv]
P:224 [in mathcomp.ssreflect.choice]
p:224 [in mathcomp.ssreflect.prime]
p:2244 [in mathcomp.ssreflect.seq]
P:2245 [in mathcomp.ssreflect.order]
p:2245 [in mathcomp.ssreflect.bigop]
p:2246 [in mathcomp.ssreflect.seq]
p:2246 [in mathcomp.ssreflect.bigop]
p:2247 [in mathcomp.ssreflect.bigop]
P:2248 [in mathcomp.ssreflect.order]
p:225 [in mathcomp.field.closed_field]
p:225 [in mathcomp.algebra.poly]
p:2257 [in mathcomp.ssreflect.bigop]
p:2258 [in mathcomp.ssreflect.bigop]
p:2259 [in mathcomp.ssreflect.bigop]
p:226 [in mathcomp.algebra.polydiv]
p:226 [in mathcomp.ssreflect.ssrnat]
p:226 [in mathcomp.algebra.mxpoly]
p:226 [in mathcomp.algebra.poly]
P:2264 [in mathcomp.ssreflect.bigop]
p:227 [in mathcomp.field.closed_field]
p:227 [in mathcomp.ssreflect.prime]
p:227 [in mathcomp.solvable.burnside_app]
P:2270 [in mathcomp.algebra.ssralg]
p:228 [in mathcomp.algebra.polydiv]
p:228 [in mathcomp.algebra.mxpoly]
p:228 [in mathcomp.solvable.burnside_app]
P:2286 [in mathcomp.ssreflect.bigop]
p:229 [in mathcomp.ssreflect.ssrnat]
p:229 [in mathcomp.field.algC]
p:229 [in mathcomp.algebra.mxpoly]
p:229 [in mathcomp.ssreflect.prime]
P:229 [in mathcomp.character.mxrepresentation]
P:229 [in mathcomp.fingroup.gproduct]
p:229 [in mathcomp.solvable.burnside_app]
P:23 [in mathcomp.ssreflect.generic_quotient]
p:23 [in mathcomp.field.separable]
p:23 [in mathcomp.field.closed_field]
p:23 [in mathcomp.field.algnum]
p:230 [in mathcomp.field.algC]
p:230 [in mathcomp.algebra.mxpoly]
p:230 [in mathcomp.solvable.burnside_app]
P:2305 [in mathcomp.ssreflect.bigop]
p:231 [in mathcomp.algebra.polydiv]
p:231 [in mathcomp.algebra.mxpoly]
p:231 [in mathcomp.solvable.abelian]
p:231 [in mathcomp.algebra.poly]
p:232 [in mathcomp.ssreflect.ssrnat]
p:232 [in mathcomp.ssreflect.prime]
P:2322 [in mathcomp.algebra.ssrnum]
P:2327 [in mathcomp.ssreflect.bigop]
p:233 [in mathcomp.algebra.polydiv]
p:233 [in mathcomp.algebra.mxalgebra]
p:234 [in mathcomp.ssreflect.div]
p:234 [in mathcomp.solvable.abelian]
p:234 [in mathcomp.algebra.poly]
P:2341 [in mathcomp.ssreflect.order]
P:2345 [in mathcomp.algebra.ssrnum]
p:2348 [in mathcomp.ssreflect.seq]
P:2349 [in mathcomp.ssreflect.order]
p:235 [in mathcomp.algebra.polydiv]
p:235 [in mathcomp.ssreflect.prime]
P:2352 [in mathcomp.ssreflect.bigop]
P:2358 [in mathcomp.ssreflect.order]
P:2358 [in mathcomp.algebra.ssrnum]
P:236 [in mathcomp.ssreflect.choice]
P:236 [in mathcomp.fingroup.action]
P:2366 [in mathcomp.ssreflect.order]
p:2367 [in mathcomp.ssreflect.seq]
P:2368 [in mathcomp.ssreflect.bigop]
p:237 [in mathcomp.algebra.polydiv]
p:237 [in mathcomp.algebra.poly]
P:2373 [in mathcomp.ssreflect.order]
p:238 [in mathcomp.field.closed_field]
p:238 [in mathcomp.ssreflect.prime]
P:2380 [in mathcomp.ssreflect.bigop]
P:2382 [in mathcomp.ssreflect.order]
p:239 [in mathcomp.algebra.polydiv]
p:239 [in mathcomp.algebra.mxalgebra]
P:2391 [in mathcomp.ssreflect.order]
P:2393 [in mathcomp.ssreflect.bigop]
p:24 [in mathcomp.solvable.alt]
p:24 [in mathcomp.algebra.polydiv]
p:24 [in mathcomp.ssreflect.choice]
p:24 [in mathcomp.field.closed_field]
P:24 [in mathcomp.solvable.sylow]
p:24 [in mathcomp.solvable.pgroup]
p:24 [in mathcomp.ssreflect.path]
p:24 [in mathcomp.algebra.polyXY]
p:24 [in mathcomp.solvable.abelian]
p:24 [in mathcomp.solvable.burnside_app]
p:24 [in mathcomp.algebra.poly]
p:24 [in mathcomp.algebra.qpoly]
p:240 [in mathcomp.field.closed_field]
P:240 [in mathcomp.ssreflect.path]
P:240 [in mathcomp.fingroup.gproduct]
p:240 [in mathcomp.algebra.poly]
P:2404 [in mathcomp.ssreflect.bigop]
p:241 [in mathcomp.algebra.polydiv]
p:241 [in mathcomp.ssreflect.ssrnat]
P:2419 [in mathcomp.ssreflect.bigop]
p:242 [in mathcomp.ssreflect.seq]
p:242 [in mathcomp.solvable.abelian]
p:242 [in mathcomp.algebra.poly]
p:243 [in mathcomp.fingroup.quotient]
p:243 [in mathcomp.algebra.polydiv]
p:243 [in mathcomp.ssreflect.ssrnat]
p:243 [in mathcomp.field.closed_field]
P:2431 [in mathcomp.ssreflect.bigop]
p:244 [in mathcomp.ssreflect.div]
p:244 [in mathcomp.ssreflect.prime]
p:244 [in mathcomp.algebra.poly]
P:244 [in mathcomp.ssreflect.eqtype]
P:2444 [in mathcomp.ssreflect.bigop]
p:245 [in mathcomp.ssreflect.prime]
P:2453 [in mathcomp.ssreflect.order]
P:2456 [in mathcomp.ssreflect.bigop]
p:246 [in mathcomp.fingroup.quotient]
p:246 [in mathcomp.solvable.abelian]
p:246 [in mathcomp.algebra.poly]
p:246 [in mathcomp.algebra.mxalgebra]
P:2461 [in mathcomp.ssreflect.order]
P:2467 [in mathcomp.ssreflect.bigop]
p:247 [in mathcomp.ssreflect.div]
p:247 [in mathcomp.ssreflect.ssrnat]
p:247 [in mathcomp.solvable.abelian]
P:2470 [in mathcomp.ssreflect.order]
P:2478 [in mathcomp.ssreflect.order]
P:2479 [in mathcomp.ssreflect.seq]
p:248 [in mathcomp.fingroup.quotient]
P:2483 [in mathcomp.ssreflect.bigop]
P:2485 [in mathcomp.ssreflect.order]
P:2494 [in mathcomp.ssreflect.order]
P:2497 [in mathcomp.ssreflect.seq]
P:2497 [in mathcomp.ssreflect.bigop]
p:25 [in mathcomp.ssreflect.ssrnat]
p:25 [in mathcomp.field.separable]
P:25 [in mathcomp.algebra.ssrint]
P:25 [in mathcomp.solvable.sylow]
p:25 [in mathcomp.solvable.pgroup]
p:25 [in mathcomp.ssreflect.path]
p:25 [in mathcomp.solvable.abelian]
p:25 [in mathcomp.solvable.burnside_app]
p:250 [in mathcomp.ssreflect.div]
p:250 [in mathcomp.ssreflect.ssrnat]
p:250 [in mathcomp.field.closed_field]
P:2503 [in mathcomp.ssreflect.order]
P:2507 [in mathcomp.ssreflect.bigop]
p:252 [in mathcomp.algebra.poly]
p:253 [in mathcomp.ssreflect.div]
p:253 [in mathcomp.ssreflect.ssrnat]
p:253 [in mathcomp.algebra.mxpoly]
P:2536 [in mathcomp.ssreflect.bigop]
p:254 [in mathcomp.ssreflect.prime]
p:254 [in mathcomp.solvable.abelian]
p:255 [in mathcomp.ssreflect.ssrnat]
p:255 [in mathcomp.field.algC]
p:255 [in mathcomp.algebra.poly]
P:2553 [in mathcomp.ssreflect.bigop]
p:256 [in mathcomp.field.algC]
p:257 [in mathcomp.algebra.mxpoly]
p:257 [in mathcomp.solvable.abelian]
P:2571 [in mathcomp.ssreflect.bigop]
P:2577 [in mathcomp.ssreflect.order]
p:258 [in mathcomp.ssreflect.div]
P:2582 [in mathcomp.ssreflect.bigop]
p:259 [in mathcomp.algebra.polydiv]
p:259 [in mathcomp.ssreflect.ssrnat]
p:259 [in mathcomp.ssreflect.prime]
p:259 [in mathcomp.field.algnum]
P:2594 [in mathcomp.algebra.matrix]
p:26 [in mathcomp.algebra.polydiv]
P:26 [in mathcomp.solvable.sylow]
p:26 [in mathcomp.solvable.abelian]
p:26 [in mathcomp.algebra.poly]
p:260 [in mathcomp.field.closed_field]
p:260 [in mathcomp.algebra.poly]
p:261 [in mathcomp.ssreflect.div]
p:261 [in mathcomp.solvable.abelian]
P:261 [in mathcomp.ssreflect.eqtype]
P:2612 [in mathcomp.ssreflect.order]
P:2613 [in mathcomp.ssreflect.bigop]
P:2616 [in mathcomp.ssreflect.seq]
p:262 [in mathcomp.algebra.polydiv]
p:262 [in mathcomp.ssreflect.ssrnat]
P:2625 [in mathcomp.ssreflect.seq]
P:263 [in mathcomp.fingroup.gproduct]
p:263 [in mathcomp.ssreflect.fintype]
p:263 [in mathcomp.algebra.poly]
p:264 [in mathcomp.algebra.polydiv]
p:265 [in mathcomp.ssreflect.ssrnat]
p:265 [in mathcomp.algebra.mxpoly]
P:265 [in mathcomp.ssreflect.eqtype]
P:2655 [in mathcomp.ssreflect.bigop]
p:266 [in mathcomp.algebra.polydiv]
p:266 [in mathcomp.ssreflect.prime]
p:266 [in mathcomp.solvable.abelian]
P:266 [in mathcomp.algebra.vector]
p:266 [in mathcomp.ssreflect.fintype]
p:2666 [in mathcomp.algebra.matrix]
p:267 [in mathcomp.ssreflect.tuple]
p:267 [in mathcomp.ssreflect.prime]
p:267 [in mathcomp.algebra.poly]
p:2676 [in mathcomp.algebra.matrix]
p:268 [in mathcomp.algebra.polydiv]
p:268 [in mathcomp.ssreflect.ssrnat]
p:268 [in mathcomp.field.closed_field]
p:268 [in mathcomp.ssreflect.prime]
p:268 [in mathcomp.algebra.ssralg]
p:268 [in mathcomp.algebra.poly]
p:269 [in mathcomp.solvable.abelian]
p:27 [in mathcomp.algebra.polydiv]
p:27 [in mathcomp.field.separable]
P:27 [in mathcomp.solvable.sylow]
p:27 [in mathcomp.ssreflect.path]
p:27 [in mathcomp.solvable.abelian]
p:27 [in mathcomp.solvable.burnside_app]
P:27 [in mathcomp.algebra.qpoly]
p:270 [in mathcomp.field.closed_field]
p:270 [in mathcomp.algebra.poly]
p:271 [in mathcomp.algebra.polydiv]
p:271 [in mathcomp.ssreflect.ssrnat]
p:271 [in mathcomp.solvable.pgroup]
P:272 [in mathcomp.fingroup.fingroup]
p:272 [in mathcomp.solvable.pgroup]
p:272 [in mathcomp.solvable.abelian]
P:272 [in mathcomp.algebra.vector]
p:272 [in mathcomp.algebra.poly]
p:273 [in mathcomp.algebra.polydiv]
p:273 [in mathcomp.solvable.pgroup]
p:273 [in mathcomp.ssreflect.prime]
P:273 [in mathcomp.algebra.ssralg]
P:273 [in mathcomp.character.character]
P:2747 [in mathcomp.ssreflect.order]
p:275 [in mathcomp.algebra.polydiv]
p:275 [in mathcomp.field.closed_field]
p:275 [in mathcomp.solvable.pgroup]
p:275 [in mathcomp.ssreflect.prime]
P:275 [in mathcomp.fingroup.gproduct]
p:275 [in mathcomp.algebra.poly]
P:2757 [in mathcomp.ssreflect.order]
P:2758 [in mathcomp.ssreflect.seq]
p:276 [in mathcomp.algebra.intdiv]
P:2764 [in mathcomp.ssreflect.seq]
p:277 [in mathcomp.algebra.polydiv]
p:277 [in mathcomp.ssreflect.prime]
p:277 [in mathcomp.algebra.poly]
p:278 [in mathcomp.algebra.polydiv]
p:278 [in mathcomp.ssreflect.ssrnat]
p:278 [in mathcomp.algebra.mxpoly]
p:278 [in mathcomp.field.closed_field]
P:279 [in mathcomp.algebra.vector]
p:28 [in mathcomp.solvable.alt]
p:28 [in mathcomp.algebra.polydiv]
P:28 [in mathcomp.solvable.sylow]
p:28 [in mathcomp.ssreflect.path]
p:280 [in mathcomp.algebra.polydiv]
p:280 [in mathcomp.ssreflect.prime]
p:280 [in mathcomp.solvable.abelian]
p:281 [in mathcomp.algebra.intdiv]
p:281 [in mathcomp.ssreflect.ssrnat]
p:281 [in mathcomp.field.closed_field]
p:282 [in mathcomp.algebra.polydiv]
p:282 [in mathcomp.ssreflect.prime]
p:283 [in mathcomp.algebra.polydiv]
p:283 [in mathcomp.field.closed_field]
p:283 [in mathcomp.algebra.poly]
p:284 [in mathcomp.algebra.intdiv]
p:284 [in mathcomp.ssreflect.ssrnat]
P:284 [in mathcomp.algebra.ssralg]
P:2842 [in mathcomp.ssreflect.bigop]
p:285 [in mathcomp.algebra.polydiv]
p:285 [in mathcomp.solvable.abelian]
p:285 [in mathcomp.algebra.poly]
P:2858 [in mathcomp.ssreflect.bigop]
p:286 [in mathcomp.algebra.polydiv]
p:286 [in mathcomp.field.algebraics_fundamentals]
p:286 [in mathcomp.field.closed_field]
p:286 [in mathcomp.ssreflect.prime]
p:286 [in mathcomp.algebra.poly]
p:2861 [in mathcomp.algebra.matrix]
p:287 [in mathcomp.algebra.polydiv]
p:287 [in mathcomp.ssreflect.ssrnat]
p:287 [in mathcomp.algebra.poly]
P:2870 [in mathcomp.ssreflect.bigop]
p:2873 [in mathcomp.algebra.matrix]
p:288 [in mathcomp.ssreflect.tuple]
p:288 [in mathcomp.algebra.polydiv]
P:2884 [in mathcomp.ssreflect.bigop]
p:289 [in mathcomp.algebra.mxpoly]
P:289 [in mathcomp.character.classfun]
p:289 [in mathcomp.ssreflect.prime]
p:289 [in mathcomp.solvable.abelian]
P:289 [in mathcomp.algebra.vector]
P:2894 [in mathcomp.ssreflect.bigop]
p:29 [in mathcomp.ssreflect.ssrAC]
p:29 [in mathcomp.solvable.burnside_app]
p:290 [in mathcomp.algebra.polydiv]
p:290 [in mathcomp.ssreflect.ssrnat]
P:2902 [in mathcomp.ssreflect.bigop]
P:2909 [in mathcomp.ssreflect.bigop]
p:291 [in mathcomp.solvable.abelian]
p:2915 [in mathcomp.algebra.matrix]
p:292 [in mathcomp.algebra.polydiv]
P:292 [in mathcomp.algebra.ssrint]
P:292 [in mathcomp.fingroup.fingroup]
p:292 [in mathcomp.ssreflect.prime]
p:292 [in mathcomp.solvable.abelian]
p:2923 [in mathcomp.algebra.matrix]
P:2923 [in mathcomp.ssreflect.bigop]
p:293 [in mathcomp.ssreflect.ssrnat]
p:293 [in mathcomp.algebra.mxpoly]
p:293 [in mathcomp.ssreflect.prime]
p:293 [in mathcomp.algebra.poly]
P:2932 [in mathcomp.ssreflect.bigop]
p:2935 [in mathcomp.algebra.matrix]
P:2940 [in mathcomp.ssreflect.bigop]
p:2947 [in mathcomp.algebra.matrix]
P:2948 [in mathcomp.ssreflect.bigop]
p:295 [in mathcomp.fingroup.perm]
p:295 [in mathcomp.algebra.polydiv]
p:295 [in mathcomp.ssreflect.prime]
p:295 [in mathcomp.solvable.abelian]
P:2956 [in mathcomp.ssreflect.bigop]
p:296 [in mathcomp.algebra.mxpoly]
p:296 [in mathcomp.field.closed_field]
P:296 [in mathcomp.ssreflect.bigop]
P:2964 [in mathcomp.ssreflect.bigop]
p:2968 [in mathcomp.algebra.matrix]
p:297 [in mathcomp.field.closed_field]
p:297 [in mathcomp.solvable.abelian]
p:297 [in mathcomp.algebra.poly]
P:2976 [in mathcomp.ssreflect.bigop]
p:298 [in mathcomp.algebra.polydiv]
p:298 [in mathcomp.field.closed_field]
P:2984 [in mathcomp.ssreflect.bigop]
p:299 [in mathcomp.ssreflect.prime]
p:299 [in mathcomp.solvable.abelian]
p:299 [in mathcomp.algebra.poly]
P:2992 [in mathcomp.ssreflect.bigop]
P:2999 [in mathcomp.ssreflect.bigop]
p:3 [in mathcomp.field.qfpoly]
p:3 [in mathcomp.algebra.qpoly]
p:30 [in mathcomp.solvable.alt]
p:30 [in mathcomp.algebra.polydiv]
p:30 [in mathcomp.ssreflect.ssrnat]
P:30 [in mathcomp.solvable.sylow]
p:30 [in mathcomp.solvable.burnside_app]
P:30 [in mathcomp.ssreflect.fintype]
p:30 [in mathcomp.algebra.poly]
p:300 [in mathcomp.ssreflect.ssrnat]
p:300 [in mathcomp.algebra.mxpoly]
P:3012 [in mathcomp.ssreflect.bigop]
p:302 [in mathcomp.algebra.polydiv]
P:302 [in mathcomp.field.algebraics_fundamentals]
P:302 [in mathcomp.algebra.ssrint]
p:302 [in mathcomp.ssreflect.prime]
p:302 [in mathcomp.solvable.abelian]
p:302 [in mathcomp.algebra.poly]
P:3021 [in mathcomp.ssreflect.bigop]
P:3022 [in mathcomp.algebra.matrix]
p:303 [in mathcomp.ssreflect.ssrnat]
P:303 [in mathcomp.field.algebraics_fundamentals]
p:303 [in mathcomp.ssreflect.path]
p:303 [in mathcomp.ssreflect.prime]
P:3030 [in mathcomp.ssreflect.bigop]
P:3039 [in mathcomp.ssreflect.bigop]
p:304 [in mathcomp.algebra.polydiv]
p:304 [in mathcomp.ssreflect.prime]
p:304 [in mathcomp.solvable.abelian]
p:304 [in mathcomp.algebra.poly]
P:3047 [in mathcomp.ssreflect.bigop]
P:3048 [in mathcomp.algebra.matrix]
P:306 [in mathcomp.field.algC]
P:306 [in mathcomp.character.classfun]
p:306 [in mathcomp.ssreflect.prime]
p:307 [in mathcomp.algebra.polydiv]
P:307 [in mathcomp.algebra.mxpoly]
p:307 [in mathcomp.solvable.abelian]
p:308 [in mathcomp.algebra.polydiv]
p:308 [in mathcomp.ssreflect.ssrnat]
p:308 [in mathcomp.ssreflect.prime]
P:308 [in mathcomp.algebra.poly]
P:3081 [in mathcomp.ssreflect.bigop]
p:309 [in mathcomp.algebra.poly]
P:3090 [in mathcomp.ssreflect.bigop]
P:3099 [in mathcomp.ssreflect.bigop]
p:31 [in mathcomp.solvable.alt]
P:31 [in mathcomp.solvable.sylow]
P:31 [in mathcomp.ssreflect.ssrbool]
p:31 [in mathcomp.solvable.burnside_app]
p:310 [in mathcomp.algebra.polydiv]
P:310 [in mathcomp.fingroup.gproduct]
P:3106 [in mathcomp.ssreflect.bigop]
P:3109 [in mathcomp.algebra.matrix]
p:311 [in mathcomp.ssreflect.ssrnat]
p:311 [in mathcomp.ssreflect.prime]
p:311 [in mathcomp.solvable.abelian]
P:3115 [in mathcomp.ssreflect.bigop]
p:312 [in mathcomp.algebra.polydiv]
p:313 [in mathcomp.ssreflect.path]
p:313 [in mathcomp.ssreflect.prime]
P:3135 [in mathcomp.algebra.matrix]
p:314 [in mathcomp.ssreflect.ssrnat]
p:314 [in mathcomp.solvable.abelian]
p:315 [in mathcomp.ssreflect.prime]
p:317 [in mathcomp.algebra.polydiv]
p:317 [in mathcomp.ssreflect.ssrnat]
P:317 [in mathcomp.field.algC]
P:317 [in mathcomp.algebra.mxalgebra]
p:318 [in mathcomp.algebra.polydiv]
p:318 [in mathcomp.ssreflect.prime]
p:319 [in mathcomp.algebra.polydiv]
p:319 [in mathcomp.solvable.abelian]
P:319 [in mathcomp.ssreflect.eqtype]
p:32 [in mathcomp.algebra.polydiv]
P:32 [in mathcomp.solvable.sylow]
p:32 [in mathcomp.solvable.burnside_app]
p:32 [in mathcomp.fingroup.presentation]
p:320 [in mathcomp.ssreflect.ssrnat]
p:320 [in mathcomp.solvable.pgroup]
p:320 [in mathcomp.ssreflect.path]
P:320 [in mathcomp.ssreflect.bigop]
P:3209 [in mathcomp.algebra.matrix]
p:321 [in mathcomp.algebra.intdiv]
p:321 [in mathcomp.ssreflect.prime]
p:323 [in mathcomp.algebra.polydiv]
p:323 [in mathcomp.ssreflect.ssrnat]
P:323 [in mathcomp.algebra.mxpoly]
p:323 [in mathcomp.solvable.abelian]
P:3236 [in mathcomp.algebra.matrix]
p:324 [in mathcomp.algebra.intdiv]
p:324 [in mathcomp.ssreflect.prime]
p:324 [in mathcomp.solvable.abelian]
P:324 [in mathcomp.algebra.ssralg]
p:324 [in mathcomp.algebra.poly]
p:3246 [in mathcomp.algebra.matrix]
p:325 [in mathcomp.algebra.polydiv]
p:325 [in mathcomp.ssreflect.path]
p:325 [in mathcomp.ssreflect.prime]
p:325 [in mathcomp.solvable.abelian]
p:325 [in mathcomp.algebra.poly]
p:326 [in mathcomp.ssreflect.ssrnat]
p:326 [in mathcomp.solvable.abelian]
p:326 [in mathcomp.algebra.poly]
p:327 [in mathcomp.algebra.intdiv]
p:327 [in mathcomp.algebra.polydiv]
p:327 [in mathcomp.ssreflect.prime]
p:327 [in mathcomp.solvable.abelian]
p:327 [in mathcomp.algebra.poly]
p:328 [in mathcomp.algebra.intdiv]
p:328 [in mathcomp.field.fieldext]
p:328 [in mathcomp.ssreflect.path]
p:329 [in mathcomp.ssreflect.ssrnat]
p:329 [in mathcomp.solvable.abelian]
p:329 [in mathcomp.algebra.poly]
p:33 [in mathcomp.ssreflect.binomial]
p:33 [in mathcomp.algebra.polydiv]
p:33 [in mathcomp.ssreflect.ssrnat]
p:33 [in mathcomp.field.fieldext]
p:33 [in mathcomp.field.separable]
P:33 [in mathcomp.solvable.sylow]
p:33 [in mathcomp.solvable.extremal]
p:33 [in mathcomp.solvable.abelian]
p:33 [in mathcomp.ssreflect.fingraph]
p:330 [in mathcomp.algebra.polydiv]
p:330 [in mathcomp.algebra.poly]
P:330 [in mathcomp.ssreflect.eqtype]
p:3303 [in mathcomp.algebra.matrix]
p:331 [in mathcomp.algebra.intdiv]
p:331 [in mathcomp.ssreflect.prime]
P:331 [in mathcomp.solvable.abelian]
P:331 [in mathcomp.algebra.vector]
p:332 [in mathcomp.algebra.polydiv]
p:332 [in mathcomp.ssreflect.ssrnat]
p:332 [in mathcomp.solvable.abelian]
p:332 [in mathcomp.algebra.poly]
p:3325 [in mathcomp.algebra.matrix]
p:333 [in mathcomp.ssreflect.prime]
p:334 [in mathcomp.algebra.intdiv]
p:334 [in mathcomp.ssreflect.path]
p:334 [in mathcomp.solvable.abelian]
p:334 [in mathcomp.algebra.poly]
p:335 [in mathcomp.ssreflect.seq]
p:335 [in mathcomp.ssreflect.ssrnat]
p:335 [in mathcomp.ssreflect.prime]
p:336 [in mathcomp.algebra.poly]
p:337 [in mathcomp.algebra.intdiv]
p:337 [in mathcomp.algebra.polydiv]
p:337 [in mathcomp.ssreflect.path]
P:337 [in mathcomp.algebra.vector]
p:338 [in mathcomp.ssreflect.seq]
p:338 [in mathcomp.ssreflect.ssrnat]
P:338 [in mathcomp.ssreflect.finset]
p:338 [in mathcomp.algebra.poly]
P:3385 [in mathcomp.ssreflect.order]
p:339 [in mathcomp.algebra.polydiv]
p:339 [in mathcomp.ssreflect.ssrnat]
p:339 [in mathcomp.ssreflect.prime]
P:3397 [in mathcomp.ssreflect.order]
p:34 [in mathcomp.algebra.polydiv]
P:34 [in mathcomp.solvable.sylow]
p:34 [in mathcomp.field.algnum]
p:34 [in mathcomp.ssreflect.fingraph]
p:34 [in mathcomp.solvable.burnside_app]
p:340 [in mathcomp.ssreflect.path]
p:340 [in mathcomp.ssreflect.prime]
p:340 [in mathcomp.algebra.poly]
p:341 [in mathcomp.ssreflect.seq]
p:341 [in mathcomp.ssreflect.prime]
P:342 [in mathcomp.algebra.ssralg]
p:342 [in mathcomp.algebra.poly]
P:3422 [in mathcomp.algebra.matrix]
p:343 [in mathcomp.ssreflect.path]
p:344 [in mathcomp.ssreflect.ssrnat]
p:344 [in mathcomp.field.closed_field]
p:345 [in mathcomp.ssreflect.ssrnat]
p:3459 [in mathcomp.algebra.matrix]
p:346 [in mathcomp.ssreflect.path]
P:346 [in mathcomp.algebra.poly]
P:347 [in mathcomp.ssreflect.bigop]
P:348 [in mathcomp.character.vcharacter]
P:348 [in mathcomp.algebra.mxpoly]
p:348 [in mathcomp.ssreflect.path]
p:3493 [in mathcomp.algebra.matrix]
p:35 [in mathcomp.field.algebraics_fundamentals]
p:35 [in mathcomp.ssreflect.ssrAC]
p:35 [in mathcomp.algebra.polyXY]
p:350 [in mathcomp.ssreflect.ssrnat]
p:350 [in mathcomp.field.galois]
p:350 [in mathcomp.ssreflect.path]
p:3504 [in mathcomp.algebra.matrix]
p:351 [in mathcomp.ssreflect.ssrnat]
p:351 [in mathcomp.ssreflect.path]
p:3519 [in mathcomp.algebra.matrix]
p:352 [in mathcomp.ssreflect.path]
P:353 [in mathcomp.field.closed_field]
p:353 [in mathcomp.ssreflect.path]
p:353 [in mathcomp.solvable.abelian]
p:354 [in mathcomp.algebra.intdiv]
p:354 [in mathcomp.ssreflect.path]
p:355 [in mathcomp.algebra.mxpoly]
p:355 [in mathcomp.solvable.abelian]
P:355 [in mathcomp.algebra.poly]
p:356 [in mathcomp.ssreflect.ssrnat]
p:356 [in mathcomp.ssreflect.path]
p:357 [in mathcomp.algebra.intdiv]
P:357 [in mathcomp.algebra.ssralg]
p:358 [in mathcomp.field.fieldext]
p:358 [in mathcomp.algebra.mxpoly]
p:358 [in mathcomp.ssreflect.path]
p:358 [in mathcomp.solvable.abelian]
p:359 [in mathcomp.ssreflect.path]
p:359 [in mathcomp.solvable.extremal]
p:36 [in mathcomp.algebra.polydiv]
P:36 [in mathcomp.algebra.zmodp]
p:36 [in mathcomp.field.qfpoly]
p:36 [in mathcomp.algebra.polyXY]
p:360 [in mathcomp.ssreflect.path]
P:362 [in mathcomp.algebra.ssrnum]
P:362 [in mathcomp.ssreflect.eqtype]
p:363 [in mathcomp.ssreflect.path]
P:365 [in mathcomp.ssreflect.eqtype]
p:366 [in mathcomp.ssreflect.path]
P:366 [in mathcomp.fingroup.gproduct]
p:367 [in mathcomp.ssreflect.prime]
p:368 [in mathcomp.ssreflect.prime]
p:368 [in mathcomp.solvable.extremal]
p:368 [in mathcomp.algebra.poly]
p:369 [in mathcomp.ssreflect.path]
p:369 [in mathcomp.ssreflect.prime]
p:369 [in mathcomp.solvable.extremal]
p:369 [in mathcomp.algebra.poly]
p:37 [in mathcomp.solvable.alt]
p:370 [in mathcomp.algebra.poly]
P:371 [in mathcomp.algebra.ssrnum]
p:371 [in mathcomp.algebra.poly]
p:372 [in mathcomp.ssreflect.path]
p:373 [in mathcomp.algebra.intdiv]
p:373 [in mathcomp.algebra.mxpoly]
p:373 [in mathcomp.algebra.poly]
P:373 [in mathcomp.ssreflect.bigop]
p:374 [in mathcomp.solvable.abelian]
p:375 [in mathcomp.algebra.polydiv]
p:375 [in mathcomp.field.closed_field]
p:375 [in mathcomp.solvable.abelian]
p:375 [in mathcomp.algebra.poly]
P:375 [in mathcomp.ssreflect.eqtype]
p:377 [in mathcomp.algebra.intdiv]
p:377 [in mathcomp.algebra.polydiv]
p:377 [in mathcomp.solvable.pgroup]
P:377 [in mathcomp.fingroup.gproduct]
p:377 [in mathcomp.solvable.abelian]
P:377 [in mathcomp.algebra.vector]
p:377 [in mathcomp.algebra.poly]
p:378 [in mathcomp.algebra.intdiv]
p:378 [in mathcomp.field.algnum]
p:379 [in mathcomp.algebra.mxpoly]
P:379 [in mathcomp.solvable.pgroup]
p:379 [in mathcomp.algebra.poly]
p:38 [in mathcomp.algebra.polydiv]
P:38 [in mathcomp.solvable.extremal]
p:380 [in mathcomp.algebra.intdiv]
p:380 [in mathcomp.algebra.polydiv]
P:380 [in mathcomp.solvable.pgroup]
P:380 [in mathcomp.ssreflect.eqtype]
p:381 [in mathcomp.algebra.intdiv]
P:381 [in mathcomp.ssreflect.fintype]
p:381 [in mathcomp.algebra.poly]
P:382 [in mathcomp.solvable.pgroup]
p:382 [in mathcomp.solvable.abelian]
p:383 [in mathcomp.algebra.intdiv]
p:383 [in mathcomp.algebra.polydiv]
p:384 [in mathcomp.algebra.mxpoly]
P:384 [in mathcomp.character.classfun]
p:384 [in mathcomp.solvable.abelian]
p:385 [in mathcomp.algebra.intdiv]
p:385 [in mathcomp.algebra.mxpoly]
p:385 [in mathcomp.algebra.poly]
p:385 [in mathcomp.algebra.mxalgebra]
p:386 [in mathcomp.algebra.polydiv]
p:386 [in mathcomp.ssreflect.prime]
p:386 [in mathcomp.algebra.poly]
p:387 [in mathcomp.algebra.intdiv]
p:387 [in mathcomp.algebra.poly]
p:388 [in mathcomp.ssreflect.prime]
P:388 [in mathcomp.fingroup.gproduct]
p:389 [in mathcomp.algebra.intdiv]
p:39 [in mathcomp.solvable.alt]
p:39 [in mathcomp.field.separable]
p:390 [in mathcomp.algebra.intdiv]
p:390 [in mathcomp.algebra.polydiv]
p:390 [in mathcomp.ssreflect.path]
p:390 [in mathcomp.ssreflect.prime]
p:390 [in mathcomp.solvable.abelian]
p:391 [in mathcomp.algebra.intdiv]
p:391 [in mathcomp.solvable.abelian]
p:392 [in mathcomp.algebra.intdiv]
p:392 [in mathcomp.algebra.poly]
p:393 [in mathcomp.algebra.intdiv]
P:393 [in mathcomp.ssreflect.fintype]
P:393 [in mathcomp.ssreflect.bigop]
p:393 [in mathcomp.algebra.mxalgebra]
p:394 [in mathcomp.algebra.intdiv]
p:394 [in mathcomp.solvable.extremal]
P:3949 [in mathcomp.ssreflect.order]
p:395 [in mathcomp.algebra.intdiv]
p:396 [in mathcomp.algebra.intdiv]
p:397 [in mathcomp.algebra.polydiv]
p:397 [in mathcomp.ssreflect.path]
P:397 [in mathcomp.algebra.ssrnum]
p:397 [in mathcomp.algebra.poly]
p:397 [in mathcomp.algebra.mxalgebra]
p:398 [in mathcomp.algebra.intdiv]
p:398 [in mathcomp.algebra.mxpoly]
P:398 [in mathcomp.fingroup.gproduct]
P:398 [in mathcomp.character.character]
p:399 [in mathcomp.algebra.intdiv]
P:399 [in mathcomp.ssreflect.fintype]
p:4 [in mathcomp.field.galois]
p:4 [in mathcomp.field.separable]
p:4 [in mathcomp.algebra.qpoly]
p:40 [in mathcomp.solvable.alt]
P:40 [in mathcomp.algebra.archimedean]
p:40 [in mathcomp.algebra.polydiv]
P:40 [in mathcomp.ssreflect.eqtype]
p:400 [in mathcomp.ssreflect.div]
p:400 [in mathcomp.algebra.polydiv]
p:400 [in mathcomp.algebra.poly]
p:401 [in mathcomp.algebra.poly]
p:404 [in mathcomp.algebra.intdiv]
p:404 [in mathcomp.algebra.polydiv]
p:404 [in mathcomp.algebra.mxpoly]
p:404 [in mathcomp.ssreflect.prime]
P:404 [in mathcomp.algebra.ssrnum]
p:404 [in mathcomp.algebra.poly]
p:406 [in mathcomp.algebra.polydiv]
p:407 [in mathcomp.algebra.intdiv]
p:408 [in mathcomp.algebra.polydiv]
p:408 [in mathcomp.algebra.poly]
p:409 [in mathcomp.field.closed_field]
p:41 [in mathcomp.solvable.alt]
p:41 [in mathcomp.algebra.polydiv]
p:41 [in mathcomp.field.galois]
p:41 [in mathcomp.ssreflect.ssrAC]
p:41 [in mathcomp.field.qfpoly]
P:41 [in mathcomp.solvable.sylow]
p:41 [in mathcomp.solvable.pgroup]
p:41 [in mathcomp.solvable.abelian]
p:410 [in mathcomp.algebra.intdiv]
p:410 [in mathcomp.algebra.polydiv]
p:410 [in mathcomp.solvable.extremal]
p:412 [in mathcomp.algebra.intdiv]
p:412 [in mathcomp.algebra.polydiv]
P:412 [in mathcomp.ssreflect.bigop]
p:413 [in mathcomp.field.closed_field]
P:413 [in mathcomp.ssreflect.fintype]
p:414 [in mathcomp.algebra.poly]
p:415 [in mathcomp.algebra.intdiv]
p:416 [in mathcomp.algebra.intdiv]
p:416 [in mathcomp.field.closed_field]
P:417 [in mathcomp.character.classfun]
P:417 [in mathcomp.ssreflect.prime]
p:418 [in mathcomp.field.closed_field]
P:418 [in mathcomp.ssreflect.fintype]
p:419 [in mathcomp.algebra.polydiv]
p:42 [in mathcomp.ssreflect.path]
p:42 [in mathcomp.solvable.abelian]
P:42 [in mathcomp.fingroup.morphism]
p:42 [in mathcomp.ssreflect.fingraph]
p:42 [in mathcomp.solvable.cyclic]
p:420 [in mathcomp.algebra.polydiv]
p:420 [in mathcomp.field.closed_field]
p:420 [in mathcomp.ssreflect.path]
p:421 [in mathcomp.algebra.polydiv]
p:421 [in mathcomp.solvable.extremal]
p:422 [in mathcomp.algebra.polydiv]
p:422 [in mathcomp.field.closed_field]
p:423 [in mathcomp.algebra.intdiv]
p:424 [in mathcomp.field.closed_field]
p:424 [in mathcomp.ssreflect.path]
P:424 [in mathcomp.algebra.ssralg]
p:425 [in mathcomp.algebra.intdiv]
P:425 [in mathcomp.field.galois]
P:426 [in mathcomp.algebra.vector]
p:427 [in mathcomp.algebra.polydiv]
P:427 [in mathcomp.fingroup.gproduct]
P:428 [in mathcomp.ssreflect.seq]
p:428 [in mathcomp.ssreflect.path]
p:429 [in mathcomp.algebra.polydiv]
p:429 [in mathcomp.solvable.extremal]
p:429 [in mathcomp.algebra.poly]
P:429 [in mathcomp.ssreflect.bigop]
p:43 [in mathcomp.field.algebraics_fundamentals]
P:43 [in mathcomp.solvable.sylow]
p:43 [in mathcomp.ssreflect.prime]
p:43 [in mathcomp.solvable.abelian]
p:43 [in mathcomp.ssreflect.fingraph]
p:43 [in mathcomp.fingroup.presentation]
P:43 [in mathcomp.ssreflect.eqtype]
p:430 [in mathcomp.algebra.polydiv]
P:430 [in mathcomp.ssreflect.fintype]
p:431 [in mathcomp.algebra.poly]
p:432 [in mathcomp.algebra.polydiv]
p:432 [in mathcomp.solvable.extremal]
p:432 [in mathcomp.solvable.abelian]
p:433 [in mathcomp.ssreflect.path]
p:434 [in mathcomp.algebra.polydiv]
p:434 [in mathcomp.solvable.abelian]
P:434 [in mathcomp.algebra.ssralg]
p:435 [in mathcomp.solvable.extremal]
p:436 [in mathcomp.algebra.polydiv]
p:436 [in mathcomp.solvable.abelian]
P:437 [in mathcomp.ssreflect.prime]
P:437 [in mathcomp.ssreflect.fintype]
P:438 [in mathcomp.fingroup.gproduct]
P:438 [in mathcomp.algebra.poly]
p:439 [in mathcomp.algebra.polydiv]
p:44 [in mathcomp.solvable.pgroup]
p:44 [in mathcomp.ssreflect.path]
p:44 [in mathcomp.algebra.qpoly]
P:442 [in mathcomp.ssreflect.bigop]
p:443 [in mathcomp.character.inertia]
P:443 [in mathcomp.ssreflect.fintype]
p:445 [in mathcomp.algebra.polydiv]
p:445 [in mathcomp.character.inertia]
p:446 [in mathcomp.character.inertia]
p:448 [in mathcomp.algebra.poly]
p:45 [in mathcomp.ssreflect.div]
p:45 [in mathcomp.algebra.polydiv]
p:45 [in mathcomp.field.qfpoly]
p:45 [in mathcomp.algebra.qpoly]
P:451 [in mathcomp.fingroup.gproduct]
p:451 [in mathcomp.solvable.abelian]
p:451 [in mathcomp.algebra.poly]
p:454 [in mathcomp.solvable.abelian]
p:454 [in mathcomp.algebra.poly]
P:454 [in mathcomp.ssreflect.bigop]
p:455 [in mathcomp.algebra.polydiv]
p:456 [in mathcomp.ssreflect.prime]
p:456 [in mathcomp.algebra.poly]
p:457 [in mathcomp.algebra.polydiv]
p:458 [in mathcomp.solvable.abelian]
p:459 [in mathcomp.algebra.polydiv]
p:459 [in mathcomp.ssreflect.prime]
p:459 [in mathcomp.algebra.poly]
p:46 [in mathcomp.ssreflect.ssrnat]
P:46 [in mathcomp.solvable.sylow]
p:46 [in mathcomp.ssreflect.path]
P:46 [in mathcomp.ssreflect.eqtype]
p:460 [in mathcomp.ssreflect.div]
P:461 [in mathcomp.fingroup.fingroup]
p:461 [in mathcomp.algebra.poly]
p:462 [in mathcomp.algebra.polydiv]
P:462 [in mathcomp.algebra.ssralg]
p:463 [in mathcomp.ssreflect.div]
p:465 [in mathcomp.algebra.polydiv]
p:466 [in mathcomp.ssreflect.div]
p:466 [in mathcomp.algebra.poly]
p:468 [in mathcomp.algebra.polydiv]
p:468 [in mathcomp.character.inertia]
p:47 [in mathcomp.algebra.zmodp]
P:47 [in mathcomp.solvable.sylow]
p:47 [in mathcomp.solvable.pgroup]
p:47 [in mathcomp.ssreflect.prime]
p:470 [in mathcomp.algebra.polydiv]
p:470 [in mathcomp.field.galois]
p:471 [in mathcomp.ssreflect.div]
p:471 [in mathcomp.field.galois]
p:471 [in mathcomp.algebra.poly]
p:472 [in mathcomp.algebra.poly]
P:472 [in mathcomp.ssreflect.bigop]
P:473 [in mathcomp.ssreflect.ssrnat]
p:474 [in mathcomp.ssreflect.div]
P:474 [in mathcomp.fingroup.gproduct]
p:475 [in mathcomp.algebra.polydiv]
p:475 [in mathcomp.algebra.mxpoly]
P:475 [in mathcomp.fingroup.fingroup]
p:475 [in mathcomp.algebra.poly]
p:476 [in mathcomp.algebra.polydiv]
p:477 [in mathcomp.ssreflect.div]
P:477 [in mathcomp.ssreflect.ssrnat]
p:478 [in mathcomp.algebra.polydiv]
p:478 [in mathcomp.algebra.poly]
p:479 [in mathcomp.algebra.mxpoly]
p:479 [in mathcomp.character.inertia]
p:479 [in mathcomp.algebra.mxalgebra]
p:48 [in mathcomp.algebra.zmodp]
p:48 [in mathcomp.field.fieldext]
p:48 [in mathcomp.algebra.mxpoly]
P:48 [in mathcomp.solvable.sylow]
p:480 [in mathcomp.ssreflect.div]
p:480 [in mathcomp.algebra.polydiv]
p:481 [in mathcomp.algebra.poly]
p:482 [in mathcomp.algebra.polydiv]
p:483 [in mathcomp.algebra.ssralg]
p:485 [in mathcomp.algebra.polydiv]
p:485 [in mathcomp.ssreflect.prime]
p:485 [in mathcomp.algebra.mxalgebra]
p:486 [in mathcomp.ssreflect.prime]
p:486 [in mathcomp.algebra.poly]
P:487 [in mathcomp.ssreflect.seq]
p:488 [in mathcomp.algebra.poly]
p:489 [in mathcomp.algebra.polydiv]
p:49 [in mathcomp.algebra.intdiv]
p:49 [in mathcomp.ssreflect.ssrnat]
P:49 [in mathcomp.solvable.sylow]
p:49 [in mathcomp.algebra.polyXY]
p:490 [in mathcomp.algebra.poly]
P:491 [in mathcomp.ssreflect.bigop]
P:492 [in mathcomp.ssreflect.seq]
p:492 [in mathcomp.algebra.mxpoly]
p:492 [in mathcomp.algebra.poly]
p:493 [in mathcomp.algebra.mxpoly]
p:4930 [in mathcomp.ssreflect.order]
p:494 [in mathcomp.algebra.poly]
p:4944 [in mathcomp.ssreflect.order]
p:4946 [in mathcomp.ssreflect.order]
P:495 [in mathcomp.ssreflect.fintype]
p:4957 [in mathcomp.ssreflect.order]
p:4959 [in mathcomp.ssreflect.order]
p:496 [in mathcomp.ssreflect.prime]
p:496 [in mathcomp.algebra.poly]
p:497 [in mathcomp.ssreflect.div]
p:497 [in mathcomp.solvable.abelian]
p:4970 [in mathcomp.ssreflect.order]
p:4974 [in mathcomp.ssreflect.order]
p:4978 [in mathcomp.ssreflect.order]
p:498 [in mathcomp.algebra.polydiv]
p:498 [in mathcomp.ssreflect.prime]
p:498 [in mathcomp.algebra.poly]
p:4985 [in mathcomp.ssreflect.order]
p:499 [in mathcomp.ssreflect.prime]
p:5 [in mathcomp.fingroup.perm]
p:5 [in mathcomp.field.separable]
p:5 [in mathcomp.algebra.mxpoly]
p:5 [in mathcomp.solvable.sylow]
p:5 [in mathcomp.algebra.poly]
p:50 [in mathcomp.ssreflect.tuple]
p:50 [in mathcomp.algebra.polydiv]
p:50 [in mathcomp.algebra.zmodp]
p:50 [in mathcomp.ssreflect.ssrAC]
p:50 [in mathcomp.solvable.pgroup]
p:50 [in mathcomp.ssreflect.fingraph]
p:50 [in mathcomp.solvable.cyclic]
p:500 [in mathcomp.ssreflect.div]
p:500 [in mathcomp.algebra.mxalgebra]
p:501 [in mathcomp.ssreflect.prime]
P:501 [in mathcomp.ssreflect.bigop]
P:502 [in mathcomp.character.mxrepresentation]
P:502 [in mathcomp.fingroup.gproduct]
P:503 [in mathcomp.ssreflect.fintype]
p:504 [in mathcomp.solvable.abelian]
p:505 [in mathcomp.ssreflect.prime]
p:505 [in mathcomp.algebra.poly]
p:506 [in mathcomp.solvable.abelian]
p:507 [in mathcomp.algebra.mxalgebra]
p:508 [in mathcomp.algebra.polydiv]
p:508 [in mathcomp.solvable.abelian]
p:508 [in mathcomp.algebra.poly]
P:51 [in mathcomp.algebra.archimedean]
P:51 [in mathcomp.solvable.sylow]
p:51 [in mathcomp.algebra.polyXY]
p:51 [in mathcomp.ssreflect.fingraph]
p:51 [in mathcomp.field.falgebra]
p:510 [in mathcomp.algebra.polydiv]
p:510 [in mathcomp.algebra.mxpoly]
p:510 [in mathcomp.solvable.abelian]
P:510 [in mathcomp.ssreflect.fintype]
p:511 [in mathcomp.algebra.polydiv]
p:512 [in mathcomp.algebra.polydiv]
p:512 [in mathcomp.character.inertia]
P:513 [in mathcomp.fingroup.gproduct]
p:513 [in mathcomp.algebra.poly]
p:513 [in mathcomp.algebra.mxalgebra]
p:514 [in mathcomp.algebra.polydiv]
p:516 [in mathcomp.algebra.polydiv]
p:517 [in mathcomp.character.inertia]
P:517 [in mathcomp.ssreflect.path]
p:518 [in mathcomp.algebra.polydiv]
p:518 [in mathcomp.character.inertia]
P:518 [in mathcomp.ssreflect.fintype]
p:518 [in mathcomp.algebra.poly]
P:518 [in mathcomp.ssreflect.bigop]
p:519 [in mathcomp.character.inertia]
p:519 [in mathcomp.solvable.abelian]
p:52 [in mathcomp.ssreflect.div]
p:52 [in mathcomp.algebra.zmodp]
P:52 [in mathcomp.solvable.sylow]
p:520 [in mathcomp.algebra.polydiv]
p:520 [in mathcomp.algebra.mxpoly]
p:520 [in mathcomp.character.inertia]
p:520 [in mathcomp.solvable.abelian]
p:521 [in mathcomp.character.inertia]
p:522 [in mathcomp.algebra.polydiv]
p:522 [in mathcomp.character.inertia]
p:522 [in mathcomp.solvable.abelian]
P:523 [in mathcomp.fingroup.gproduct]
p:524 [in mathcomp.character.inertia]
p:525 [in mathcomp.algebra.polydiv]
p:525 [in mathcomp.character.classfun]
P:525 [in mathcomp.ssreflect.fintype]
p:526 [in mathcomp.character.inertia]
p:527 [in mathcomp.algebra.polydiv]
p:527 [in mathcomp.character.inertia]
p:527 [in mathcomp.solvable.abelian]
p:528 [in mathcomp.algebra.polydiv]
p:528 [in mathcomp.character.inertia]
p:529 [in mathcomp.algebra.polydiv]
P:529 [in mathcomp.character.mxrepresentation]
p:529 [in mathcomp.solvable.abelian]
p:53 [in mathcomp.field.fieldext]
P:53 [in mathcomp.algebra.ssrint]
p:53 [in mathcomp.field.qfpoly]
P:53 [in mathcomp.solvable.sylow]
p:53 [in mathcomp.fingroup.presentation]
p:53 [in mathcomp.algebra.poly]
P:530 [in mathcomp.ssreflect.fintype]
p:531 [in mathcomp.algebra.mxpoly]
p:531 [in mathcomp.ssreflect.path]
p:532 [in mathcomp.solvable.abelian]
p:534 [in mathcomp.ssreflect.path]
p:534 [in mathcomp.solvable.abelian]
p:535 [in mathcomp.ssreflect.prime]
P:536 [in mathcomp.ssreflect.fintype]
p:537 [in mathcomp.ssreflect.prime]
p:539 [in mathcomp.ssreflect.prime]
p:539 [in mathcomp.solvable.abelian]
p:54 [in mathcomp.algebra.zmodp]
P:54 [in mathcomp.ssreflect.finset]
P:54 [in mathcomp.solvable.sylow]
p:54 [in mathcomp.algebra.polyXY]
p:54 [in mathcomp.solvable.cyclic]
p:540 [in mathcomp.field.galois]
p:543 [in mathcomp.ssreflect.prime]
P:544 [in mathcomp.ssreflect.fintype]
p:545 [in mathcomp.ssreflect.prime]
P:546 [in mathcomp.ssreflect.path]
p:547 [in mathcomp.algebra.vector]
P:547 [in mathcomp.ssreflect.bigop]
p:55 [in mathcomp.ssreflect.div]
p:55 [in mathcomp.algebra.polyXY]
P:55 [in mathcomp.ssreflect.fintype]
p:55 [in mathcomp.algebra.poly]
P:551 [in mathcomp.ssreflect.path]
p:553 [in mathcomp.algebra.poly]
p:554 [in mathcomp.algebra.polydiv]
P:554 [in mathcomp.field.galois]
p:555 [in mathcomp.algebra.poly]
p:557 [in mathcomp.algebra.polydiv]
P:557 [in mathcomp.ssreflect.bigop]
p:558 [in mathcomp.ssreflect.ssrnat]
p:56 [in mathcomp.algebra.polydiv]
p:56 [in mathcomp.field.fieldext]
p:56 [in mathcomp.ssreflect.prime]
p:56 [in mathcomp.algebra.polyXY]
P:56 [in mathcomp.ssreflect.ssrbool]
p:56 [in mathcomp.solvable.burnside_app]
p:56 [in mathcomp.fingroup.presentation]
p:561 [in mathcomp.algebra.polydiv]
p:563 [in mathcomp.solvable.abelian]
P:564 [in mathcomp.algebra.ssrnum]
p:565 [in mathcomp.algebra.polydiv]
p:565 [in mathcomp.algebra.poly]
p:57 [in mathcomp.ssreflect.ssrnat]
p:57 [in mathcomp.ssreflect.ssrAC]
p:57 [in mathcomp.field.closed_field]
p:57 [in mathcomp.field.qfpoly]
p:57 [in mathcomp.solvable.pgroup]
p:57 [in mathcomp.algebra.polyXY]
p:57 [in mathcomp.solvable.abelian]
p:57 [in mathcomp.solvable.burnside_app]
p:571 [in mathcomp.algebra.polydiv]
P:572 [in mathcomp.field.galois]
P:572 [in mathcomp.algebra.ssrnum]
P:573 [in mathcomp.character.mxrepresentation]
p:573 [in mathcomp.algebra.poly]
p:574 [in mathcomp.algebra.poly]
p:576 [in mathcomp.ssreflect.prime]
p:578 [in mathcomp.algebra.poly]
p:58 [in mathcomp.algebra.polydiv]
p:58 [in mathcomp.field.closed_field]
p:58 [in mathcomp.field.qfpoly]
P:58 [in mathcomp.solvable.sylow]
p:58 [in mathcomp.algebra.polyXY]
p:58 [in mathcomp.solvable.cyclic]
p:58 [in mathcomp.algebra.poly]
P:58 [in mathcomp.ssreflect.eqtype]
p:58 [in mathcomp.algebra.qpoly]
p:580 [in mathcomp.ssreflect.prime]
p:580 [in mathcomp.solvable.abelian]
p:580 [in mathcomp.algebra.poly]
p:581 [in mathcomp.algebra.polydiv]
p:582 [in mathcomp.fingroup.action]
p:582 [in mathcomp.ssreflect.prime]
p:583 [in mathcomp.algebra.polydiv]
p:583 [in mathcomp.ssreflect.prime]
p:583 [in mathcomp.algebra.poly]
p:584 [in mathcomp.ssreflect.prime]
p:585 [in mathcomp.algebra.polydiv]
p:586 [in mathcomp.ssreflect.prime]
p:586 [in mathcomp.algebra.poly]
P:587 [in mathcomp.ssreflect.path]
p:588 [in mathcomp.ssreflect.prime]
p:588 [in mathcomp.algebra.poly]
p:59 [in mathcomp.algebra.intdiv]
p:59 [in mathcomp.field.fieldext]
p:59 [in mathcomp.algebra.polyXY]
p:590 [in mathcomp.algebra.poly]
p:591 [in mathcomp.fingroup.action]
p:591 [in mathcomp.algebra.poly]
p:592 [in mathcomp.fingroup.action]
p:592 [in mathcomp.algebra.poly]
P:592 [in mathcomp.ssreflect.bigop]
p:593 [in mathcomp.algebra.polydiv]
p:593 [in mathcomp.fingroup.action]
p:594 [in mathcomp.algebra.polydiv]
p:594 [in mathcomp.fingroup.action]
p:594 [in mathcomp.algebra.poly]
p:595 [in mathcomp.ssreflect.path]
P:595 [in mathcomp.algebra.ssrnum]
p:596 [in mathcomp.algebra.polydiv]
p:596 [in mathcomp.solvable.pgroup]
p:597 [in mathcomp.solvable.pgroup]
p:598 [in mathcomp.algebra.polydiv]
p:598 [in mathcomp.solvable.pgroup]
p:598 [in mathcomp.algebra.poly]
p:599 [in mathcomp.algebra.polydiv]
P:599 [in mathcomp.ssreflect.bigop]
p:6 [in mathcomp.ssreflect.path]
p:6 [in mathcomp.solvable.burnside_app]
p:60 [in mathcomp.algebra.polydiv]
p:60 [in mathcomp.algebra.mxpoly]
p:60 [in mathcomp.field.closed_field]
p:60 [in mathcomp.solvable.abelian]
P:60 [in mathcomp.algebra.ssralg]
p:60 [in mathcomp.algebra.qpoly]
p:600 [in mathcomp.algebra.polydiv]
P:600 [in mathcomp.ssreflect.path]
p:600 [in mathcomp.algebra.poly]
p:600 [in mathcomp.algebra.mxalgebra]
p:601 [in mathcomp.algebra.polydiv]
p:602 [in mathcomp.algebra.polydiv]
p:602 [in mathcomp.ssreflect.path]
p:602 [in mathcomp.algebra.poly]
P:603 [in mathcomp.algebra.ssrnum]
p:604 [in mathcomp.algebra.poly]
p:605 [in mathcomp.algebra.polydiv]
p:605 [in mathcomp.algebra.poly]
p:607 [in mathcomp.algebra.poly]
p:607 [in mathcomp.algebra.mxalgebra]
p:609 [in mathcomp.algebra.polydiv]
p:609 [in mathcomp.solvable.abelian]
P:61 [in mathcomp.algebra.archimedean]
P:61 [in mathcomp.ssreflect.choice]
p:61 [in mathcomp.solvable.abelian]
p:610 [in mathcomp.algebra.poly]
p:611 [in mathcomp.algebra.polydiv]
p:611 [in mathcomp.algebra.poly]
P:611 [in mathcomp.ssreflect.bigop]
p:612 [in mathcomp.solvable.abelian]
P:612 [in mathcomp.algebra.ssrnum]
p:612 [in mathcomp.algebra.poly]
p:613 [in mathcomp.algebra.poly]
p:614 [in mathcomp.algebra.polydiv]
p:614 [in mathcomp.algebra.mxpoly]
p:614 [in mathcomp.solvable.abelian]
p:615 [in mathcomp.algebra.poly]
p:616 [in mathcomp.solvable.abelian]
p:617 [in mathcomp.algebra.polydiv]
p:618 [in mathcomp.algebra.poly]
p:619 [in mathcomp.algebra.polydiv]
p:619 [in mathcomp.solvable.abelian]
p:62 [in mathcomp.algebra.intdiv]
p:62 [in mathcomp.algebra.polydiv]
p:62 [in mathcomp.field.closed_field]
P:62 [in mathcomp.solvable.sylow]
p:62 [in mathcomp.ssreflect.prime]
p:62 [in mathcomp.solvable.abelian]
p:62 [in mathcomp.solvable.burnside_app]
p:62 [in mathcomp.algebra.poly]
p:620 [in mathcomp.algebra.polydiv]
P:620 [in mathcomp.algebra.ssrnum]
P:621 [in mathcomp.fingroup.fingroup]
p:621 [in mathcomp.algebra.poly]
P:621 [in mathcomp.ssreflect.bigop]
p:621 [in mathcomp.algebra.mxalgebra]
p:623 [in mathcomp.algebra.polydiv]
p:623 [in mathcomp.solvable.abelian]
p:626 [in mathcomp.algebra.polydiv]
p:628 [in mathcomp.solvable.abelian]
p:628 [in mathcomp.algebra.poly]
p:628 [in mathcomp.algebra.mxalgebra]
p:63 [in mathcomp.algebra.mxpoly]
p:63 [in mathcomp.field.closed_field]
p:63 [in mathcomp.solvable.burnside_app]
p:63 [in mathcomp.algebra.poly]
p:630 [in mathcomp.algebra.poly]
P:630 [in mathcomp.ssreflect.bigop]
p:631 [in mathcomp.algebra.polydiv]
p:632 [in mathcomp.solvable.abelian]
p:633 [in mathcomp.ssreflect.ssrnat]
p:633 [in mathcomp.algebra.mxpoly]
p:633 [in mathcomp.algebra.poly]
p:634 [in mathcomp.ssreflect.seq]
p:634 [in mathcomp.algebra.polydiv]
p:635 [in mathcomp.algebra.poly]
p:636 [in mathcomp.algebra.polydiv]
p:639 [in mathcomp.algebra.polydiv]
p:639 [in mathcomp.algebra.poly]
p:64 [in mathcomp.solvable.pgroup]
p:64 [in mathcomp.solvable.burnside_app]
p:64 [in mathcomp.fingroup.presentation]
p:64 [in mathcomp.algebra.poly]
p:640 [in mathcomp.solvable.abelian]
P:641 [in mathcomp.ssreflect.bigop]
p:642 [in mathcomp.algebra.polydiv]
p:642 [in mathcomp.algebra.poly]
p:644 [in mathcomp.ssreflect.seq]
p:644 [in mathcomp.algebra.poly]
p:645 [in mathcomp.algebra.polydiv]
p:645 [in mathcomp.solvable.abelian]
p:645 [in mathcomp.algebra.poly]
p:648 [in mathcomp.algebra.polydiv]
P:648 [in mathcomp.ssreflect.bigop]
P:65 [in mathcomp.ssreflect.choice]
p:65 [in mathcomp.character.character]
p:65 [in mathcomp.algebra.poly]
p:650 [in mathcomp.algebra.poly]
p:651 [in mathcomp.algebra.polydiv]
p:652 [in mathcomp.algebra.poly]
P:653 [in mathcomp.ssreflect.fintype]
p:654 [in mathcomp.algebra.polydiv]
p:654 [in mathcomp.solvable.abelian]
p:654 [in mathcomp.algebra.poly]
P:655 [in mathcomp.ssreflect.path]
p:655 [in mathcomp.solvable.abelian]
p:656 [in mathcomp.solvable.abelian]
p:656 [in mathcomp.algebra.poly]
p:657 [in mathcomp.algebra.polydiv]
p:657 [in mathcomp.solvable.abelian]
p:659 [in mathcomp.algebra.poly]
p:66 [in mathcomp.algebra.mxpoly]
P:66 [in mathcomp.solvable.sylow]
p:66 [in mathcomp.solvable.pgroup]
p:66 [in mathcomp.algebra.polyXY]
p:66 [in mathcomp.algebra.poly]
p:661 [in mathcomp.solvable.abelian]
p:662 [in mathcomp.algebra.polydiv]
p:662 [in mathcomp.ssreflect.order]
p:662 [in mathcomp.algebra.poly]
P:662 [in mathcomp.ssreflect.bigop]
p:663 [in mathcomp.algebra.polydiv]
p:664 [in mathcomp.ssreflect.order]
P:664 [in mathcomp.character.mxrepresentation]
p:664 [in mathcomp.algebra.poly]
p:666 [in mathcomp.algebra.polydiv]
p:666 [in mathcomp.algebra.poly]
p:667 [in mathcomp.solvable.abelian]
p:667 [in mathcomp.algebra.poly]
p:668 [in mathcomp.ssreflect.order]
p:669 [in mathcomp.algebra.polydiv]
p:67 [in mathcomp.field.closed_field]
p:67 [in mathcomp.fingroup.presentation]
p:670 [in mathcomp.ssreflect.order]
p:672 [in mathcomp.algebra.polydiv]
P:672 [in mathcomp.ssreflect.bigop]
p:675 [in mathcomp.algebra.poly]
p:676 [in mathcomp.solvable.abelian]
p:677 [in mathcomp.algebra.mxpoly]
p:677 [in mathcomp.algebra.poly]
P:678 [in mathcomp.ssreflect.path]
p:679 [in mathcomp.solvable.abelian]
p:68 [in mathcomp.algebra.mxpoly]
P:68 [in mathcomp.solvable.sylow]
p:68 [in mathcomp.solvable.pgroup]
p:68 [in mathcomp.ssreflect.prime]
P:68 [in mathcomp.solvable.maximal]
p:68 [in mathcomp.algebra.poly]
p:680 [in mathcomp.algebra.poly]
p:680 [in mathcomp.algebra.mxalgebra]
p:681 [in mathcomp.algebra.mxpoly]
p:681 [in mathcomp.solvable.abelian]
p:682 [in mathcomp.algebra.poly]
P:683 [in mathcomp.ssreflect.bigop]
p:685 [in mathcomp.algebra.mxpoly]
p:686 [in mathcomp.algebra.poly]
p:689 [in mathcomp.algebra.poly]
P:69 [in mathcomp.ssreflect.choice]
p:69 [in mathcomp.field.closed_field]
p:69 [in mathcomp.ssreflect.prime]
p:69 [in mathcomp.algebra.poly]
p:690 [in mathcomp.algebra.polydiv]
p:691 [in mathcomp.algebra.poly]
p:692 [in mathcomp.algebra.poly]
p:695 [in mathcomp.algebra.polydiv]
P:695 [in mathcomp.algebra.vector]
p:695 [in mathcomp.algebra.poly]
p:696 [in mathcomp.algebra.polydiv]
p:697 [in mathcomp.algebra.poly]
p:699 [in mathcomp.algebra.polydiv]
p:699 [in mathcomp.algebra.poly]
p:7 [in mathcomp.solvable.alt]
P:7 [in mathcomp.ssreflect.finset]
p:7 [in mathcomp.algebra.polyXY]
p:7 [in mathcomp.solvable.burnside_app]
p:7 [in mathcomp.algebra.poly]
p:70 [in mathcomp.field.closed_field]
p:70 [in mathcomp.field.qfpoly]
p:70 [in mathcomp.ssreflect.prime]
p:70 [in mathcomp.algebra.polyXY]
P:70 [in mathcomp.solvable.center]
p:70 [in mathcomp.algebra.poly]
p:70 [in mathcomp.algebra.qpoly]
p:702 [in mathcomp.algebra.polydiv]
p:702 [in mathcomp.algebra.mxpoly]
p:705 [in mathcomp.algebra.polydiv]
P:705 [in mathcomp.ssreflect.bigop]
p:706 [in mathcomp.algebra.poly]
p:708 [in mathcomp.algebra.polydiv]
p:71 [in mathcomp.algebra.polydiv]
p:71 [in mathcomp.character.character]
P:71 [in mathcomp.solvable.maximal]
p:71 [in mathcomp.algebra.poly]
p:710 [in mathcomp.algebra.polydiv]
p:717 [in mathcomp.algebra.polydiv]
P:718 [in mathcomp.algebra.mxpoly]
P:718 [in mathcomp.ssreflect.fintype]
P:719 [in mathcomp.algebra.ssralg]
P:72 [in mathcomp.character.mxabelem]
p:72 [in mathcomp.field.qfpoly]
p:72 [in mathcomp.algebra.polyXY]
P:72 [in mathcomp.algebra.ssralg]
P:721 [in mathcomp.algebra.mxpoly]
p:722 [in mathcomp.algebra.polydiv]
P:722 [in mathcomp.algebra.mxpoly]
p:722 [in mathcomp.ssreflect.path]
p:723 [in mathcomp.algebra.polydiv]
P:723 [in mathcomp.algebra.mxpoly]
p:723 [in mathcomp.algebra.poly]
p:724 [in mathcomp.algebra.polydiv]
P:724 [in mathcomp.algebra.matrix]
P:724 [in mathcomp.algebra.mxpoly]
p:724 [in mathcomp.ssreflect.path]
p:725 [in mathcomp.algebra.polydiv]
P:725 [in mathcomp.algebra.mxpoly]
p:725 [in mathcomp.algebra.poly]
P:726 [in mathcomp.algebra.mxpoly]
P:726 [in mathcomp.ssreflect.fintype]
p:727 [in mathcomp.algebra.polydiv]
p:729 [in mathcomp.algebra.poly]
p:73 [in mathcomp.field.separable]
p:73 [in mathcomp.algebra.mxpoly]
P:73 [in mathcomp.solvable.sylow]
p:73 [in mathcomp.algebra.poly]
P:730 [in mathcomp.algebra.ssralg]
P:731 [in mathcomp.algebra.mxpoly]
p:732 [in mathcomp.algebra.polydiv]
P:732 [in mathcomp.ssreflect.fintype]
P:733 [in mathcomp.algebra.matrix]
p:734 [in mathcomp.algebra.polydiv]
P:734 [in mathcomp.ssreflect.bigop]
P:736 [in mathcomp.algebra.mxpoly]
p:736 [in mathcomp.algebra.poly]
P:736 [in mathcomp.algebra.mxalgebra]
p:737 [in mathcomp.algebra.poly]
p:74 [in mathcomp.field.galois]
p:74 [in mathcomp.field.qfpoly]
p:74 [in mathcomp.fingroup.presentation]
P:740 [in mathcomp.algebra.mxpoly]
P:740 [in mathcomp.ssreflect.fintype]
p:741 [in mathcomp.algebra.polydiv]
p:741 [in mathcomp.algebra.poly]
P:742 [in mathcomp.algebra.matrix]
p:742 [in mathcomp.algebra.poly]
P:743 [in mathcomp.algebra.mxpoly]
p:743 [in mathcomp.algebra.poly]
p:744 [in mathcomp.algebra.polydiv]
p:744 [in mathcomp.algebra.poly]
p:745 [in mathcomp.algebra.polydiv]
P:746 [in mathcomp.algebra.mxpoly]
P:746 [in mathcomp.algebra.mxalgebra]
p:747 [in mathcomp.algebra.polydiv]
p:747 [in mathcomp.algebra.poly]
p:748 [in mathcomp.algebra.poly]
P:75 [in mathcomp.solvable.sylow]
p:75 [in mathcomp.algebra.ssrnum]
p:750 [in mathcomp.algebra.polydiv]
P:750 [in mathcomp.algebra.mxpoly]
p:752 [in mathcomp.algebra.polydiv]
p:753 [in mathcomp.algebra.poly]
P:754 [in mathcomp.algebra.mxalgebra]
P:755 [in mathcomp.algebra.mxpoly]
p:756 [in mathcomp.algebra.polydiv]
P:757 [in mathcomp.algebra.matrix]
p:757 [in mathcomp.algebra.poly]
p:759 [in mathcomp.algebra.polydiv]
P:759 [in mathcomp.algebra.mxpoly]
p:759 [in mathcomp.algebra.poly]
P:76 [in mathcomp.algebra.archimedean]
P:76 [in mathcomp.ssreflect.choice]
P:76 [in mathcomp.solvable.sylow]
P:760 [in mathcomp.ssreflect.finset]
p:762 [in mathcomp.algebra.polydiv]
p:762 [in mathcomp.ssreflect.path]
p:762 [in mathcomp.algebra.poly]
p:763 [in mathcomp.ssreflect.path]
P:763 [in mathcomp.algebra.mxalgebra]
p:764 [in mathcomp.algebra.polydiv]
P:764 [in mathcomp.algebra.mxpoly]
p:764 [in mathcomp.algebra.poly]
p:765 [in mathcomp.algebra.poly]
p:767 [in mathcomp.algebra.polydiv]
P:767 [in mathcomp.algebra.matrix]
p:767 [in mathcomp.algebra.poly]
p:769 [in mathcomp.algebra.polydiv]
p:769 [in mathcomp.algebra.poly]
P:77 [in mathcomp.character.classfun]
p:77 [in mathcomp.field.closed_field]
p:77 [in mathcomp.field.qfpoly]
P:77 [in mathcomp.solvable.sylow]
p:77 [in mathcomp.solvable.pgroup]
p:77 [in mathcomp.ssreflect.path]
p:77 [in mathcomp.solvable.burnside_app]
p:77 [in mathcomp.algebra.poly]
p:770 [in mathcomp.algebra.polydiv]
P:770 [in mathcomp.algebra.mxpoly]
P:771 [in mathcomp.ssreflect.fintype]
p:771 [in mathcomp.algebra.poly]
p:772 [in mathcomp.algebra.polydiv]
p:774 [in mathcomp.algebra.polydiv]
P:774 [in mathcomp.algebra.mxpoly]
P:775 [in mathcomp.algebra.mxalgebra]
p:778 [in mathcomp.algebra.polydiv]
P:778 [in mathcomp.algebra.mxpoly]
p:778 [in mathcomp.algebra.poly]
p:779 [in mathcomp.algebra.polydiv]
p:779 [in mathcomp.algebra.poly]
p:78 [in mathcomp.field.qfpoly]
P:78 [in mathcomp.solvable.sylow]
P:78 [in mathcomp.solvable.pgroup]
p:78 [in mathcomp.solvable.burnside_app]
p:78 [in mathcomp.algebra.fraction]
P:780 [in mathcomp.ssreflect.order]
P:780 [in mathcomp.ssreflect.fintype]
P:780 [in mathcomp.ssreflect.bigop]
p:781 [in mathcomp.algebra.polydiv]
p:781 [in mathcomp.algebra.poly]
p:785 [in mathcomp.ssreflect.path]
P:786 [in mathcomp.algebra.matrix]
P:786 [in mathcomp.algebra.mxalgebra]
p:787 [in mathcomp.ssreflect.seq]
p:787 [in mathcomp.algebra.polydiv]
p:787 [in mathcomp.ssreflect.path]
P:787 [in mathcomp.ssreflect.bigop]
P:788 [in mathcomp.algebra.vector]
p:788 [in mathcomp.algebra.poly]
p:789 [in mathcomp.algebra.poly]
p:79 [in mathcomp.field.galois]
p:79 [in mathcomp.field.closed_field]
p:79 [in mathcomp.field.qfpoly]
P:79 [in mathcomp.solvable.sylow]
P:79 [in mathcomp.solvable.pgroup]
p:79 [in mathcomp.algebra.polyXY]
P:79 [in mathcomp.ssreflect.eqtype]
P:790 [in mathcomp.ssreflect.fintype]
p:790 [in mathcomp.algebra.poly]
p:791 [in mathcomp.algebra.poly]
p:793 [in mathcomp.algebra.poly]
p:794 [in mathcomp.ssreflect.seq]
p:795 [in mathcomp.ssreflect.path]
p:797 [in mathcomp.algebra.polydiv]
P:797 [in mathcomp.algebra.mxalgebra]
p:798 [in mathcomp.ssreflect.seq]
p:798 [in mathcomp.algebra.poly]
p:8 [in mathcomp.algebra.polyXY]
p:8 [in mathcomp.solvable.extremal]
p:8 [in mathcomp.solvable.burnside_app]
p:8 [in mathcomp.algebra.poly]
p:8 [in mathcomp.algebra.qpoly]
P:80 [in mathcomp.ssreflect.choice]
p:80 [in mathcomp.solvable.pgroup]
p:80 [in mathcomp.algebra.fraction]
p:80 [in mathcomp.algebra.poly]
P:80 [in mathcomp.solvable.nilpotent]
p:800 [in mathcomp.ssreflect.path]
p:800 [in mathcomp.algebra.mxalgebra]
p:801 [in mathcomp.algebra.polydiv]
p:802 [in mathcomp.algebra.polydiv]
P:802 [in mathcomp.algebra.vector]
P:802 [in mathcomp.ssreflect.fintype]
p:803 [in mathcomp.algebra.polydiv]
p:804 [in mathcomp.ssreflect.seq]
p:804 [in mathcomp.algebra.polydiv]
p:805 [in mathcomp.algebra.polydiv]
p:805 [in mathcomp.algebra.poly]
p:806 [in mathcomp.algebra.polydiv]
p:807 [in mathcomp.algebra.polydiv]
p:807 [in mathcomp.ssreflect.path]
p:807 [in mathcomp.algebra.poly]
p:808 [in mathcomp.ssreflect.seq]
P:808 [in mathcomp.ssreflect.bigop]
p:809 [in mathcomp.algebra.polydiv]
p:809 [in mathcomp.algebra.poly]
p:81 [in mathcomp.algebra.polydiv]
p:81 [in mathcomp.field.qfpoly]
p:81 [in mathcomp.solvable.pgroup]
p:810 [in mathcomp.algebra.polydiv]
P:810 [in mathcomp.algebra.mxalgebra]
p:811 [in mathcomp.algebra.poly]
p:812 [in mathcomp.algebra.polydiv]
p:812 [in mathcomp.ssreflect.path]
p:812 [in mathcomp.algebra.poly]
P:813 [in mathcomp.algebra.mxpoly]
p:813 [in mathcomp.ssreflect.path]
p:813 [in mathcomp.algebra.poly]
p:814 [in mathcomp.algebra.polydiv]
P:814 [in mathcomp.algebra.mxpoly]
p:814 [in mathcomp.algebra.poly]
p:815 [in mathcomp.algebra.poly]
p:818 [in mathcomp.algebra.polydiv]
p:818 [in mathcomp.algebra.poly]
P:818 [in mathcomp.ssreflect.bigop]
p:819 [in mathcomp.algebra.polydiv]
P:82 [in mathcomp.ssreflect.choice]
P:82 [in mathcomp.solvable.sylow]
p:82 [in mathcomp.solvable.pgroup]
P:82 [in mathcomp.ssreflect.eqtype]
p:821 [in mathcomp.ssreflect.path]
p:822 [in mathcomp.algebra.polydiv]
p:822 [in mathcomp.algebra.poly]
P:822 [in mathcomp.algebra.mxalgebra]
P:824 [in mathcomp.ssreflect.order]
p:824 [in mathcomp.algebra.poly]
p:825 [in mathcomp.algebra.polydiv]
p:825 [in mathcomp.algebra.ssrint]
p:825 [in mathcomp.algebra.poly]
p:827 [in mathcomp.algebra.poly]
p:828 [in mathcomp.algebra.polydiv]
P:829 [in mathcomp.ssreflect.finset]
p:829 [in mathcomp.algebra.poly]
P:83 [in mathcomp.character.mxabelem]
p:83 [in mathcomp.solvable.sylow]
p:831 [in mathcomp.algebra.poly]
p:832 [in mathcomp.algebra.polydiv]
p:832 [in mathcomp.algebra.ssrint]
p:833 [in mathcomp.algebra.polydiv]
p:833 [in mathcomp.algebra.poly]
p:835 [in mathcomp.algebra.poly]
p:836 [in mathcomp.algebra.polydiv]
P:836 [in mathcomp.ssreflect.bigop]
P:836 [in mathcomp.algebra.mxalgebra]
p:837 [in mathcomp.algebra.ssrint]
p:837 [in mathcomp.fingroup.fingroup]
P:837 [in mathcomp.ssreflect.order]
p:838 [in mathcomp.algebra.polydiv]
p:838 [in mathcomp.algebra.ssrint]
p:838 [in mathcomp.algebra.poly]
p:839 [in mathcomp.algebra.polydiv]
P:84 [in mathcomp.ssreflect.choice]
p:84 [in mathcomp.field.galois]
p:84 [in mathcomp.field.separable]
P:84 [in mathcomp.solvable.sylow]
p:841 [in mathcomp.algebra.polydiv]
p:843 [in mathcomp.algebra.polydiv]
p:844 [in mathcomp.algebra.polydiv]
p:844 [in mathcomp.algebra.poly]
p:845 [in mathcomp.algebra.polydiv]
p:847 [in mathcomp.algebra.polydiv]
p:847 [in mathcomp.algebra.poly]
P:847 [in mathcomp.ssreflect.bigop]
p:848 [in mathcomp.fingroup.fingroup]
p:849 [in mathcomp.algebra.poly]
P:85 [in mathcomp.solvable.sylow]
p:85 [in mathcomp.solvable.pgroup]
P:85 [in mathcomp.solvable.center]
p:850 [in mathcomp.algebra.poly]
p:851 [in mathcomp.fingroup.fingroup]
P:852 [in mathcomp.algebra.ssrnum]
p:853 [in mathcomp.algebra.poly]
p:855 [in mathcomp.algebra.poly]
p:856 [in mathcomp.algebra.poly]
P:857 [in mathcomp.ssreflect.bigop]
p:859 [in mathcomp.algebra.polydiv]
p:859 [in mathcomp.algebra.poly]
p:86 [in mathcomp.algebra.intdiv]
p:86 [in mathcomp.ssreflect.ssrAC]
P:86 [in mathcomp.solvable.sylow]
p:86 [in mathcomp.algebra.qpoly]
P:860 [in mathcomp.algebra.ssrnum]
p:861 [in mathcomp.algebra.polydiv]
p:861 [in mathcomp.algebra.poly]
p:862 [in mathcomp.algebra.polydiv]
P:862 [in mathcomp.algebra.ssralg]
p:863 [in mathcomp.algebra.polydiv]
p:863 [in mathcomp.algebra.poly]
p:864 [in mathcomp.algebra.poly]
p:865 [in mathcomp.algebra.polydiv]
p:867 [in mathcomp.algebra.polydiv]
p:867 [in mathcomp.algebra.poly]
P:868 [in mathcomp.algebra.ssrnum]
p:87 [in mathcomp.character.vcharacter]
P:87 [in mathcomp.solvable.sylow]
p:87 [in mathcomp.algebra.poly]
p:87 [in mathcomp.algebra.qpoly]
p:870 [in mathcomp.algebra.poly]
p:871 [in mathcomp.algebra.polydiv]
p:871 [in mathcomp.algebra.mxalgebra]
p:873 [in mathcomp.algebra.polydiv]
p:873 [in mathcomp.algebra.poly]
p:874 [in mathcomp.algebra.poly]
p:874 [in mathcomp.algebra.mxalgebra]
p:875 [in mathcomp.algebra.poly]
p:876 [in mathcomp.algebra.poly]
P:876 [in mathcomp.ssreflect.bigop]
p:877 [in mathcomp.algebra.poly]
P:878 [in mathcomp.ssreflect.order]
p:879 [in mathcomp.algebra.mxalgebra]
P:88 [in mathcomp.ssreflect.choice]
P:88 [in mathcomp.solvable.sylow]
p:88 [in mathcomp.algebra.polyXY]
p:880 [in mathcomp.algebra.polydiv]
P:881 [in mathcomp.ssreflect.ssrnat]
P:881 [in mathcomp.ssreflect.order]
P:881 [in mathcomp.algebra.ssrnum]
p:881 [in mathcomp.algebra.poly]
p:882 [in mathcomp.algebra.polydiv]
P:884 [in mathcomp.ssreflect.ssrnat]
p:885 [in mathcomp.algebra.polydiv]
p:885 [in mathcomp.algebra.poly]
P:886 [in mathcomp.ssreflect.bigop]
p:887 [in mathcomp.algebra.polydiv]
p:887 [in mathcomp.algebra.poly]
p:888 [in mathcomp.algebra.mxalgebra]
P:889 [in mathcomp.ssreflect.finset]
P:89 [in mathcomp.character.inertia]
p:89 [in mathcomp.field.closed_field]
P:89 [in mathcomp.solvable.sylow]
p:89 [in mathcomp.fingroup.presentation]
p:89 [in mathcomp.algebra.poly]
p:89 [in mathcomp.algebra.qpoly]
p:890 [in mathcomp.algebra.polydiv]
P:890 [in mathcomp.ssreflect.order]
p:890 [in mathcomp.algebra.poly]
p:892 [in mathcomp.algebra.polydiv]
p:892 [in mathcomp.algebra.poly]
P:893 [in mathcomp.ssreflect.ssrnat]
P:893 [in mathcomp.ssreflect.order]
p:894 [in mathcomp.algebra.polydiv]
p:895 [in mathcomp.algebra.poly]
P:895 [in mathcomp.ssreflect.bigop]
p:896 [in mathcomp.algebra.polydiv]
P:896 [in mathcomp.ssreflect.ssrnat]
p:897 [in mathcomp.algebra.poly]
p:9 [in mathcomp.field.separable]
p:9 [in mathcomp.field.finfield]
p:9 [in mathcomp.algebra.polyXY]
p:9 [in mathcomp.field.algnum]
p:9 [in mathcomp.algebra.qpoly]
P:90 [in mathcomp.solvable.sylow]
p:90 [in mathcomp.solvable.maximal]
p:900 [in mathcomp.algebra.polydiv]
p:901 [in mathcomp.algebra.poly]
p:904 [in mathcomp.algebra.polydiv]
P:906 [in mathcomp.ssreflect.bigop]
P:907 [in mathcomp.algebra.poly]
p:908 [in mathcomp.algebra.polydiv]
p:908 [in mathcomp.algebra.poly]
p:909 [in mathcomp.algebra.mxalgebra]
P:91 [in mathcomp.ssreflect.choice]
p:91 [in mathcomp.field.separable]
p:911 [in mathcomp.algebra.polydiv]
p:912 [in mathcomp.algebra.polydiv]
P:914 [in mathcomp.ssreflect.order]
p:914 [in mathcomp.algebra.mxalgebra]
p:915 [in mathcomp.algebra.poly]
p:917 [in mathcomp.algebra.polydiv]
P:917 [in mathcomp.ssreflect.ssrnat]
P:917 [in mathcomp.ssreflect.order]
P:917 [in mathcomp.ssreflect.bigop]
p:919 [in mathcomp.algebra.polydiv]
p:919 [in mathcomp.algebra.poly]
p:92 [in mathcomp.algebra.intdiv]
p:92 [in mathcomp.algebra.polydiv]
p:92 [in mathcomp.field.separable]
P:92 [in mathcomp.solvable.sylow]
p:92 [in mathcomp.algebra.polyXY]
P:92 [in mathcomp.solvable.nilpotent]
P:920 [in mathcomp.ssreflect.ssrnat]
p:921 [in mathcomp.algebra.polydiv]
p:921 [in mathcomp.algebra.poly]
p:921 [in mathcomp.algebra.mxalgebra]
p:923 [in mathcomp.algebra.poly]
p:924 [in mathcomp.algebra.polydiv]
P:925 [in mathcomp.ssreflect.seq]
p:926 [in mathcomp.algebra.poly]
p:927 [in mathcomp.algebra.polydiv]
P:928 [in mathcomp.character.mxrepresentation]
p:929 [in mathcomp.algebra.poly]
p:93 [in mathcomp.algebra.polydiv]
P:93 [in mathcomp.solvable.sylow]
p:93 [in mathcomp.solvable.maximal]
P:93 [in mathcomp.algebra.poly]
p:930 [in mathcomp.algebra.polydiv]
p:931 [in mathcomp.ssreflect.ssrnat]
p:932 [in mathcomp.algebra.poly]
p:933 [in mathcomp.algebra.polydiv]
p:934 [in mathcomp.algebra.poly]
p:935 [in mathcomp.ssreflect.ssrnat]
p:936 [in mathcomp.algebra.polydiv]
p:936 [in mathcomp.algebra.poly]
P:938 [in mathcomp.ssreflect.bigop]
p:939 [in mathcomp.algebra.polydiv]
p:939 [in mathcomp.ssreflect.ssrnat]
p:94 [in mathcomp.ssreflect.ssrAC]
p:94 [in mathcomp.field.closed_field]
P:94 [in mathcomp.solvable.sylow]
p:94 [in mathcomp.fingroup.presentation]
p:941 [in mathcomp.algebra.poly]
p:943 [in mathcomp.ssreflect.ssrnat]
p:945 [in mathcomp.algebra.poly]
P:948 [in mathcomp.ssreflect.bigop]
p:95 [in mathcomp.algebra.intdiv]
P:95 [in mathcomp.solvable.sylow]
P:951 [in mathcomp.algebra.poly]
p:952 [in mathcomp.algebra.polydiv]
p:952 [in mathcomp.algebra.poly]
p:955 [in mathcomp.algebra.polydiv]
P:955 [in mathcomp.algebra.ssralg]
p:959 [in mathcomp.algebra.polydiv]
p:959 [in mathcomp.algebra.poly]
p:96 [in mathcomp.algebra.polydiv]
P:96 [in mathcomp.solvable.sylow]
p:96 [in mathcomp.algebra.polyXY]
p:96 [in mathcomp.solvable.maximal]
P:960 [in mathcomp.ssreflect.bigop]
p:961 [in mathcomp.algebra.polydiv]
p:963 [in mathcomp.algebra.polydiv]
P:963 [in mathcomp.ssreflect.fintype]
p:963 [in mathcomp.algebra.poly]
p:965 [in mathcomp.algebra.polydiv]
p:965 [in mathcomp.algebra.poly]
p:967 [in mathcomp.algebra.poly]
p:968 [in mathcomp.algebra.polydiv]
P:969 [in mathcomp.algebra.ssralg]
p:97 [in mathcomp.field.closed_field]
P:97 [in mathcomp.solvable.sylow]
p:97 [in mathcomp.fingroup.presentation]
p:97 [in mathcomp.solvable.maximal]
p:97 [in mathcomp.algebra.qpoly]
p:970 [in mathcomp.algebra.polydiv]
p:970 [in mathcomp.algebra.poly]
p:972 [in mathcomp.algebra.poly]
p:973 [in mathcomp.ssreflect.seq]
p:975 [in mathcomp.algebra.poly]
P:977 [in mathcomp.algebra.vector]
P:979 [in mathcomp.ssreflect.fintype]
p:979 [in mathcomp.algebra.poly]
p:98 [in mathcomp.algebra.intdiv]
p:98 [in mathcomp.field.galois]
p:98 [in mathcomp.solvable.maximal]
p:98 [in mathcomp.algebra.qpoly]
p:980 [in mathcomp.algebra.poly]
p:981 [in mathcomp.algebra.ssralg]
p:981 [in mathcomp.algebra.poly]
p:985 [in mathcomp.algebra.polydiv]
p:987 [in mathcomp.algebra.polydiv]
p:989 [in mathcomp.algebra.polydiv]
p:99 [in mathcomp.field.closed_field]
p:99 [in mathcomp.solvable.sylow]
p:99 [in mathcomp.algebra.qpoly]
P:990 [in mathcomp.algebra.vector]
p:992 [in mathcomp.algebra.polydiv]
p:995 [in mathcomp.algebra.polydiv]
P:999 [in mathcomp.algebra.matrix]

Global Index

_

(76754 entries)

Notation Index

H

J

T

W

X

Y

_

(1892 entries)

Binder Index

_

other

(49588 entries)

Module Index

H

J

K

L

W

X

Y

_

other

(305 entries)

Variable Index

J

W

X

Y

_

other

(4034 entries)

Library Index

K

L

U

W

X

Y

_

other

(94 entries)

Lemma Index

Y

_

other

(14802 entries)

Constructor Index

J

K

W

Y

_

other

(222 entries)

Axiom Index

B

C

D

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(131 entries)

Projection Index

D

H

I

J

K

L

N

O

Q

U

W

X

Y

Z

_

other

(43 entries)

Section Index

J

W

X

Y

_

other

(1392 entries)

Abbreviation Index

Y

_

other

(1140 entries)

Definition Index

Y

_

other

(3066 entries)

Record Index

D

F

H

I

J

K

L

O

Q

U

W

X

Y

Z

_

other

(36 entries)