| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (71649 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1792 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (46193 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (266 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3623 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (91 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14204 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (259 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (134 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (44 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1276 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (682 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3041 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
T (binder)
tauS:262 [in mathcomp.character.vcharacter]tauS:574 [in mathcomp.character.classfun]
tau:166 [in mathcomp.character.classfun]
tau:170 [in mathcomp.character.classfun]
tau:263 [in mathcomp.character.vcharacter]
tau:264 [in mathcomp.character.vcharacter]
tau:266 [in mathcomp.character.vcharacter]
tau:267 [in mathcomp.character.vcharacter]
tau:568 [in mathcomp.character.classfun]
tau:571 [in mathcomp.character.classfun]
tau:572 [in mathcomp.character.classfun]
tau:575 [in mathcomp.character.classfun]
tau:576 [in mathcomp.character.classfun]
tau:578 [in mathcomp.character.classfun]
theta:437 [in mathcomp.character.inertia]
theta:485 [in mathcomp.character.inertia]
theta:496 [in mathcomp.character.inertia]
theta:538 [in mathcomp.character.inertia]
toL:365 [in mathcomp.field.fieldext]
toL:366 [in mathcomp.field.fieldext]
toPF:364 [in mathcomp.field.fieldext]
top:218 [in mathcomp.ssreflect.order]
to':31 [in mathcomp.fingroup.action]
to:12 [in mathcomp.fingroup.action]
to:158 [in mathcomp.solvable.frobenius]
to:30 [in mathcomp.fingroup.action]
to:37 [in mathcomp.fingroup.action]
to:39 [in mathcomp.fingroup.action]
to:39 [in mathcomp.solvable.frobenius]
to:4 [in mathcomp.fingroup.action]
to:43 [in mathcomp.fingroup.action]
to:46 [in mathcomp.fingroup.action]
to:463 [in mathcomp.fingroup.action]
to:466 [in mathcomp.fingroup.action]
to:5 [in mathcomp.solvable.burnside_app]
to:53 [in mathcomp.fingroup.action]
to:58 [in mathcomp.fingroup.action]
to:588 [in mathcomp.fingroup.gproduct]
to:592 [in mathcomp.fingroup.gproduct]
to:62 [in mathcomp.fingroup.action]
to:622 [in mathcomp.fingroup.action]
to:626 [in mathcomp.fingroup.action]
to:633 [in mathcomp.fingroup.action]
to:637 [in mathcomp.fingroup.action]
to:640 [in mathcomp.fingroup.action]
to:643 [in mathcomp.fingroup.action]
to:66 [in mathcomp.fingroup.action]
to:71 [in mathcomp.fingroup.action]
to:74 [in mathcomp.fingroup.action]
to:8 [in mathcomp.fingroup.action]
tP:158 [in mathcomp.ssreflect.choice]
tP:161 [in mathcomp.ssreflect.choice]
tP:164 [in mathcomp.ssreflect.choice]
ts:211 [in mathcomp.fingroup.perm]
ts:215 [in mathcomp.fingroup.perm]
ts:220 [in mathcomp.fingroup.perm]
ts:324 [in mathcomp.field.closed_field]
Tx:142 [in mathcomp.character.inertia]
ty':2 [in mathcomp.ssreflect.ssrAC]
ty:1 [in mathcomp.ssreflect.ssrAC]
ty:5 [in mathcomp.ssreflect.ssrAC]
ty:6 [in mathcomp.ssreflect.ssrAC]
T':104 [in mathcomp.fingroup.perm]
T':1210 [in mathcomp.ssreflect.finset]
T':1467 [in mathcomp.ssreflect.order]
T':150 [in mathcomp.ssreflect.fingraph]
t':1512 [in mathcomp.algebra.ssralg]
T':155 [in mathcomp.ssreflect.generic_quotient]
T':2095 [in mathcomp.ssreflect.order]
T':2126 [in mathcomp.ssreflect.order]
T':2133 [in mathcomp.ssreflect.order]
T':214 [in mathcomp.ssreflect.tuple]
T':2149 [in mathcomp.ssreflect.order]
T':2178 [in mathcomp.ssreflect.order]
T':2282 [in mathcomp.ssreflect.seq]
T':2367 [in mathcomp.ssreflect.seq]
T':2481 [in mathcomp.ssreflect.order]
T':2486 [in mathcomp.ssreflect.order]
T':2488 [in mathcomp.ssreflect.order]
T':2490 [in mathcomp.ssreflect.order]
T':2492 [in mathcomp.ssreflect.order]
T':2534 [in mathcomp.ssreflect.order]
T':2536 [in mathcomp.ssreflect.order]
T':2553 [in mathcomp.ssreflect.order]
T':2555 [in mathcomp.ssreflect.order]
T':2557 [in mathcomp.ssreflect.order]
T':2559 [in mathcomp.ssreflect.order]
T':2563 [in mathcomp.ssreflect.order]
T':2565 [in mathcomp.ssreflect.order]
T':2567 [in mathcomp.ssreflect.order]
T':2569 [in mathcomp.ssreflect.order]
T':2571 [in mathcomp.ssreflect.order]
T':2573 [in mathcomp.ssreflect.order]
T':2575 [in mathcomp.ssreflect.order]
T':2577 [in mathcomp.ssreflect.order]
T':2579 [in mathcomp.ssreflect.order]
T':2581 [in mathcomp.ssreflect.order]
T':2583 [in mathcomp.ssreflect.order]
T':2585 [in mathcomp.ssreflect.order]
T':2587 [in mathcomp.ssreflect.order]
T':2613 [in mathcomp.ssreflect.order]
T':2630 [in mathcomp.ssreflect.order]
T':2635 [in mathcomp.ssreflect.order]
T':2637 [in mathcomp.ssreflect.order]
T':2639 [in mathcomp.ssreflect.order]
T':2641 [in mathcomp.ssreflect.order]
T':2663 [in mathcomp.ssreflect.order]
T':2672 [in mathcomp.ssreflect.order]
T':2676 [in mathcomp.ssreflect.order]
T':2678 [in mathcomp.ssreflect.order]
T':2680 [in mathcomp.ssreflect.order]
T':3076 [in mathcomp.ssreflect.order]
T':3085 [in mathcomp.ssreflect.order]
T':533 [in mathcomp.ssreflect.fintype]
T':541 [in mathcomp.ssreflect.fintype]
T':627 [in mathcomp.ssreflect.fintype]
T':665 [in mathcomp.ssreflect.path]
T':675 [in mathcomp.ssreflect.path]
t':78 [in mathcomp.solvable.primitive_action]
T':786 [in mathcomp.ssreflect.path]
t':79 [in mathcomp.solvable.primitive_action]
T':863 [in mathcomp.ssreflect.fintype]
T':868 [in mathcomp.ssreflect.fintype]
T':958 [in mathcomp.ssreflect.order]
T':96 [in mathcomp.ssreflect.generic_quotient]
t1:110 [in mathcomp.solvable.burnside_app]
T1:1254 [in mathcomp.algebra.mxalgebra]
T1:1283 [in mathcomp.ssreflect.seq]
t1:13 [in mathcomp.ssreflect.tuple]
T1:1302 [in mathcomp.ssreflect.seq]
T1:1400 [in mathcomp.ssreflect.order]
t1:1492 [in mathcomp.algebra.ssralg]
t1:1551 [in mathcomp.ssreflect.seq]
t1:167 [in mathcomp.ssreflect.tuple]
T1:171 [in mathcomp.ssreflect.choice]
T1:173 [in mathcomp.ssreflect.choice]
t1:1964 [in mathcomp.ssreflect.seq]
t1:2064 [in mathcomp.ssreflect.seq]
t1:2092 [in mathcomp.ssreflect.seq]
t1:2186 [in mathcomp.ssreflect.seq]
T1:241 [in mathcomp.ssreflect.choice]
T1:243 [in mathcomp.ssreflect.choice]
t1:2825 [in mathcomp.ssreflect.order]
t1:2832 [in mathcomp.ssreflect.order]
t1:2842 [in mathcomp.ssreflect.order]
t1:2845 [in mathcomp.ssreflect.order]
t1:2848 [in mathcomp.ssreflect.order]
t1:2851 [in mathcomp.ssreflect.order]
t1:2855 [in mathcomp.ssreflect.order]
t1:2858 [in mathcomp.ssreflect.order]
t1:2860 [in mathcomp.ssreflect.order]
t1:2863 [in mathcomp.ssreflect.order]
t1:2880 [in mathcomp.ssreflect.order]
t1:2883 [in mathcomp.ssreflect.order]
t1:2886 [in mathcomp.ssreflect.order]
t1:2888 [in mathcomp.ssreflect.order]
t1:2890 [in mathcomp.ssreflect.order]
t1:2950 [in mathcomp.ssreflect.order]
t1:2956 [in mathcomp.ssreflect.order]
t1:2962 [in mathcomp.ssreflect.order]
T1:4 [in mathcomp.field.closed_field]
T1:406 [in mathcomp.ssreflect.eqtype]
T1:43 [in mathcomp.field.closed_field]
T1:7 [in mathcomp.field.closed_field]
t1:840 [in mathcomp.ssreflect.seq]
T1:851 [in mathcomp.ssreflect.order]
t1:853 [in mathcomp.ssreflect.seq]
t2:111 [in mathcomp.solvable.burnside_app]
T2:1255 [in mathcomp.algebra.mxalgebra]
T2:1284 [in mathcomp.ssreflect.seq]
T2:1303 [in mathcomp.ssreflect.seq]
t2:14 [in mathcomp.ssreflect.tuple]
T2:1401 [in mathcomp.ssreflect.order]
t2:1552 [in mathcomp.ssreflect.seq]
t2:168 [in mathcomp.ssreflect.tuple]
T2:172 [in mathcomp.ssreflect.choice]
T2:174 [in mathcomp.ssreflect.choice]
t2:1965 [in mathcomp.ssreflect.seq]
t2:2066 [in mathcomp.ssreflect.seq]
t2:2093 [in mathcomp.ssreflect.seq]
t2:2188 [in mathcomp.ssreflect.seq]
T2:242 [in mathcomp.ssreflect.choice]
T2:244 [in mathcomp.ssreflect.choice]
t2:2826 [in mathcomp.ssreflect.order]
t2:2833 [in mathcomp.ssreflect.order]
t2:2843 [in mathcomp.ssreflect.order]
t2:2846 [in mathcomp.ssreflect.order]
t2:2849 [in mathcomp.ssreflect.order]
t2:2852 [in mathcomp.ssreflect.order]
t2:2854 [in mathcomp.ssreflect.order]
t2:2859 [in mathcomp.ssreflect.order]
t2:2861 [in mathcomp.ssreflect.order]
t2:2864 [in mathcomp.ssreflect.order]
t2:2881 [in mathcomp.ssreflect.order]
t2:2884 [in mathcomp.ssreflect.order]
t2:2887 [in mathcomp.ssreflect.order]
t2:2889 [in mathcomp.ssreflect.order]
t2:2891 [in mathcomp.ssreflect.order]
t2:2951 [in mathcomp.ssreflect.order]
t2:2957 [in mathcomp.ssreflect.order]
t2:2963 [in mathcomp.ssreflect.order]
T2:407 [in mathcomp.ssreflect.eqtype]
T2:45 [in mathcomp.field.closed_field]
T2:8 [in mathcomp.field.closed_field]
t2:841 [in mathcomp.ssreflect.seq]
T2:852 [in mathcomp.ssreflect.order]
t2:854 [in mathcomp.ssreflect.seq]
T:1 [in mathcomp.ssreflect.generic_quotient]
T:1 [in mathcomp.algebra.interval]
T:1 [in mathcomp.algebra.ring_quotient]
T:1 [in mathcomp.ssreflect.ssreflect]
T:1 [in mathcomp.ssreflect.fingraph]
T:1 [in mathcomp.ssreflect.fintype]
T:1 [in mathcomp.ssreflect.bigop]
T:1 [in mathcomp.ssreflect.eqtype]
t:10 [in mathcomp.ssreflect.tuple]
T:10 [in mathcomp.ssreflect.bigop]
T:100 [in mathcomp.ssreflect.generic_quotient]
t:101 [in mathcomp.ssreflect.tuple]
T:101 [in mathcomp.ssreflect.bigop]
t:1024 [in mathcomp.character.mxrepresentation]
T:103 [in mathcomp.fingroup.perm]
t:104 [in mathcomp.ssreflect.tuple]
t:107 [in mathcomp.ssreflect.tuple]
t:107 [in mathcomp.field.closed_field]
T:1074 [in mathcomp.ssreflect.order]
T:1075 [in mathcomp.ssreflect.order]
T:1076 [in mathcomp.ssreflect.order]
T:1077 [in mathcomp.ssreflect.order]
t:108 [in mathcomp.ssreflect.tuple]
T:109 [in mathcomp.fingroup.perm]
T:1092 [in mathcomp.ssreflect.order]
T:11 [in mathcomp.fingroup.perm]
T:11 [in mathcomp.field.algebraics_fundamentals]
T:11 [in mathcomp.ssreflect.fintype]
t:110 [in mathcomp.ssreflect.tuple]
T:111 [in mathcomp.ssreflect.generic_quotient]
T:113 [in mathcomp.fingroup.perm]
t:113 [in mathcomp.ssreflect.tuple]
T:113 [in mathcomp.ssreflect.finfun]
T:113 [in mathcomp.algebra.ring_quotient]
t:116 [in mathcomp.fingroup.perm]
T:116 [in mathcomp.ssreflect.generic_quotient]
t:116 [in mathcomp.ssreflect.tuple]
t:1172 [in mathcomp.ssreflect.order]
T:118 [in mathcomp.ssreflect.eqtype]
T:119 [in mathcomp.ssreflect.generic_quotient]
t:119 [in mathcomp.ssreflect.tuple]
T:1194 [in mathcomp.ssreflect.seq]
T:1197 [in mathcomp.ssreflect.seq]
t:12 [in mathcomp.ssreflect.tuple]
T:12 [in mathcomp.ssreflect.fintype]
T:1201 [in mathcomp.ssreflect.seq]
T:121 [in mathcomp.fingroup.perm]
T:121 [in mathcomp.ssreflect.generic_quotient]
t:121 [in mathcomp.ssreflect.tuple]
T:121 [in mathcomp.ssreflect.bigop]
t:1219 [in mathcomp.ssreflect.order]
T:1231 [in mathcomp.ssreflect.order]
T:124 [in mathcomp.fingroup.perm]
t:124 [in mathcomp.ssreflect.tuple]
T:124 [in mathcomp.fingroup.action]
T:125 [in mathcomp.ssreflect.order]
t:1259 [in mathcomp.ssreflect.seq]
t:126 [in mathcomp.ssreflect.tuple]
T:126 [in mathcomp.ssreflect.eqtype]
t:1260 [in mathcomp.ssreflect.seq]
t:1269 [in mathcomp.ssreflect.seq]
T:127 [in mathcomp.fingroup.perm]
t:127 [in mathcomp.solvable.extremal]
t:1282 [in mathcomp.ssreflect.seq]
t:1287 [in mathcomp.ssreflect.order]
t:129 [in mathcomp.ssreflect.tuple]
t:1291 [in mathcomp.ssreflect.order]
T:1293 [in mathcomp.algebra.mxalgebra]
t:1295 [in mathcomp.ssreflect.order]
t:1299 [in mathcomp.ssreflect.order]
t:13 [in mathcomp.fingroup.presentation]
T:13 [in mathcomp.ssreflect.eqtype]
T:130 [in mathcomp.ssreflect.ssrbool]
T:1307 [in mathcomp.ssreflect.seq]
t:1323 [in mathcomp.ssreflect.seq]
t:133 [in mathcomp.ssreflect.tuple]
t:1347 [in mathcomp.ssreflect.seq]
T:136 [in mathcomp.ssreflect.generic_quotient]
t:136 [in mathcomp.ssreflect.tuple]
T:138 [in mathcomp.ssreflect.generic_quotient]
T:14 [in mathcomp.field.closed_field]
T:14 [in mathcomp.ssreflect.order]
T:140 [in mathcomp.ssreflect.generic_quotient]
t:1404 [in mathcomp.ssreflect.order]
t:1407 [in mathcomp.ssreflect.order]
T:141 [in mathcomp.ssreflect.tuple]
T:141 [in mathcomp.ssreflect.bigop]
t:1410 [in mathcomp.ssreflect.order]
t:1413 [in mathcomp.ssreflect.order]
t:1416 [in mathcomp.ssreflect.order]
t:1419 [in mathcomp.ssreflect.order]
t:142 [in mathcomp.ssreflect.tuple]
T:142 [in mathcomp.ssreflect.bigop]
t:1422 [in mathcomp.ssreflect.order]
t:1425 [in mathcomp.ssreflect.order]
t:1426 [in mathcomp.ssreflect.seq]
t:1428 [in mathcomp.ssreflect.order]
t:1431 [in mathcomp.ssreflect.order]
t:1435 [in mathcomp.ssreflect.order]
t:1435 [in mathcomp.algebra.ssralg]
t:1439 [in mathcomp.ssreflect.order]
T:144 [in mathcomp.ssreflect.order]
T:144 [in mathcomp.ssreflect.bigop]
t:1443 [in mathcomp.ssreflect.order]
t:1445 [in mathcomp.algebra.ssralg]
t:1447 [in mathcomp.ssreflect.order]
T:145 [in mathcomp.ssreflect.tuple]
t:1451 [in mathcomp.ssreflect.order]
t:1452 [in mathcomp.algebra.ssralg]
t:1454 [in mathcomp.algebra.ssralg]
T:1455 [in mathcomp.ssreflect.seq]
t:1455 [in mathcomp.ssreflect.order]
T:1457 [in mathcomp.ssreflect.finset]
t:1459 [in mathcomp.ssreflect.order]
t:146 [in mathcomp.ssreflect.tuple]
T:146 [in mathcomp.ssreflect.bigop]
T:1463 [in mathcomp.ssreflect.finset]
t:1463 [in mathcomp.ssreflect.order]
T:1466 [in mathcomp.ssreflect.order]
t:147 [in mathcomp.algebra.matrix]
t:1475 [in mathcomp.algebra.ssralg]
T:148 [in mathcomp.ssreflect.order]
t:1481 [in mathcomp.algebra.ssralg]
t:1484 [in mathcomp.algebra.ssralg]
t:1489 [in mathcomp.algebra.ssralg]
t:15 [in mathcomp.fingroup.perm]
t:15 [in mathcomp.ssreflect.tuple]
T:15 [in mathcomp.ssreflect.ssreflect]
T:15 [in mathcomp.ssreflect.bigop]
t:150 [in mathcomp.ssreflect.tuple]
t:150 [in mathcomp.algebra.matrix]
T:1514 [in mathcomp.ssreflect.order]
T:1522 [in mathcomp.ssreflect.order]
t:1529 [in mathcomp.ssreflect.seq]
t:153 [in mathcomp.algebra.matrix]
T:153 [in mathcomp.ssreflect.fintype]
t:1534 [in mathcomp.ssreflect.seq]
t:1540 [in mathcomp.ssreflect.seq]
t:1542 [in mathcomp.ssreflect.seq]
t:1544 [in mathcomp.ssreflect.seq]
t:1546 [in mathcomp.ssreflect.seq]
t:1548 [in mathcomp.ssreflect.seq]
t:155 [in mathcomp.ssreflect.tuple]
t:1550 [in mathcomp.algebra.ssralg]
t:1552 [in mathcomp.algebra.ssralg]
T:1555 [in mathcomp.ssreflect.order]
t:1556 [in mathcomp.ssreflect.seq]
T:156 [in mathcomp.ssreflect.fintype]
t:1560 [in mathcomp.ssreflect.seq]
t:1563 [in mathcomp.ssreflect.seq]
t:1567 [in mathcomp.ssreflect.seq]
t:1569 [in mathcomp.ssreflect.seq]
T:1576 [in mathcomp.ssreflect.seq]
t:1578 [in mathcomp.ssreflect.seq]
T:1580 [in mathcomp.ssreflect.seq]
T:159 [in mathcomp.ssreflect.fintype]
T:16 [in mathcomp.solvable.alt]
t:16 [in mathcomp.field.closed_field]
t:160 [in mathcomp.ssreflect.tuple]
t:1604 [in mathcomp.character.mxrepresentation]
t:1616 [in mathcomp.character.mxrepresentation]
T:162 [in mathcomp.ssreflect.ssrbool]
T:1620 [in mathcomp.ssreflect.order]
T:1626 [in mathcomp.ssreflect.order]
t:163 [in mathcomp.ssreflect.tuple]
T:163 [in mathcomp.field.galois]
T:1634 [in mathcomp.ssreflect.order]
T:166 [in mathcomp.ssreflect.order]
T:1661 [in mathcomp.ssreflect.seq]
T:1665 [in mathcomp.ssreflect.seq]
t:167 [in mathcomp.fingroup.perm]
T:167 [in mathcomp.ssreflect.ssrbool]
T:1670 [in mathcomp.ssreflect.seq]
T:1673 [in mathcomp.ssreflect.seq]
T:1675 [in mathcomp.ssreflect.order]
t:1698 [in mathcomp.algebra.matrix]
T:17 [in mathcomp.ssreflect.eqtype]
T:170 [in mathcomp.ssreflect.choice]
T:172 [in mathcomp.ssreflect.binomial]
t:172 [in mathcomp.fingroup.perm]
t:172 [in mathcomp.ssreflect.tuple]
T:172 [in mathcomp.ssreflect.ssrbool]
t:173 [in mathcomp.field.algebraics_fundamentals]
T:173 [in mathcomp.ssreflect.order]
t:1731 [in mathcomp.ssreflect.order]
t:1735 [in mathcomp.ssreflect.order]
t:174 [in mathcomp.ssreflect.tuple]
t:1747 [in mathcomp.ssreflect.order]
t:175 [in mathcomp.ssreflect.binomial]
T:175 [in mathcomp.ssreflect.choice]
t:176 [in mathcomp.ssreflect.binomial]
t:176 [in mathcomp.ssreflect.tuple]
T:176 [in mathcomp.ssreflect.choice]
T:1762 [in mathcomp.ssreflect.order]
t:1766 [in mathcomp.ssreflect.order]
t:177 [in mathcomp.ssreflect.binomial]
t:177 [in mathcomp.solvable.extremal]
T:177 [in mathcomp.ssreflect.ssrbool]
t:1770 [in mathcomp.ssreflect.order]
t:1777 [in mathcomp.algebra.ssralg]
t:178 [in mathcomp.ssreflect.binomial]
t:178 [in mathcomp.ssreflect.tuple]
t:1782 [in mathcomp.ssreflect.order]
t:179 [in mathcomp.ssreflect.binomial]
t:179 [in mathcomp.solvable.extremal]
t:18 [in mathcomp.ssreflect.tuple]
T:18 [in mathcomp.ssreflect.order]
T:181 [in mathcomp.ssreflect.binomial]
T:181 [in mathcomp.ssreflect.choice]
t:181 [in mathcomp.solvable.burnside_app]
T:182 [in mathcomp.ssreflect.ssrbool]
t:184 [in mathcomp.ssreflect.tuple]
t:184 [in mathcomp.solvable.extremal]
t:1845 [in mathcomp.ssreflect.order]
T:185 [in mathcomp.ssreflect.choice]
t:185 [in mathcomp.solvable.extremal]
T:186 [in mathcomp.ssreflect.tuple]
T:187 [in mathcomp.ssreflect.binomial]
t:187 [in mathcomp.solvable.extremal]
t:187 [in mathcomp.solvable.burnside_app]
T:188 [in mathcomp.ssreflect.tuple]
T:189 [in mathcomp.ssreflect.binomial]
t:189 [in mathcomp.solvable.extremal]
T:19 [in mathcomp.ssreflect.bigop]
T:19 [in mathcomp.ssreflect.eqtype]
T:190 [in mathcomp.ssreflect.choice]
t:1913 [in mathcomp.ssreflect.seq]
t:1918 [in mathcomp.ssreflect.seq]
T:1918 [in mathcomp.algebra.ssralg]
t:192 [in mathcomp.solvable.extremal]
t:1923 [in mathcomp.ssreflect.seq]
T:193 [in mathcomp.ssreflect.choice]
t:1932 [in mathcomp.ssreflect.seq]
T:1939 [in mathcomp.ssreflect.order]
T:194 [in mathcomp.ssreflect.choice]
t:194 [in mathcomp.solvable.extremal]
t:1945 [in mathcomp.ssreflect.seq]
t:195 [in mathcomp.solvable.extremal]
t:1955 [in mathcomp.ssreflect.seq]
T:1959 [in mathcomp.ssreflect.order]
T:196 [in mathcomp.ssreflect.choice]
t:196 [in mathcomp.solvable.extremal]
T:1963 [in mathcomp.ssreflect.order]
T:1968 [in mathcomp.ssreflect.order]
t:197 [in mathcomp.solvable.extremal]
t:197 [in mathcomp.solvable.burnside_app]
t:1974 [in mathcomp.ssreflect.seq]
T:1976 [in mathcomp.ssreflect.order]
t:198 [in mathcomp.solvable.extremal]
T:1981 [in mathcomp.ssreflect.order]
t:1984 [in mathcomp.ssreflect.seq]
t:199 [in mathcomp.solvable.extremal]
t:1993 [in mathcomp.ssreflect.seq]
T:1997 [in mathcomp.ssreflect.order]
T:2 [in mathcomp.field.fieldext]
T:2 [in mathcomp.ssreflect.ssreflect]
T:2 [in mathcomp.ssreflect.order]
T:20 [in mathcomp.ssreflect.prime]
t:200 [in mathcomp.solvable.extremal]
t:2002 [in mathcomp.ssreflect.seq]
T:2008 [in mathcomp.ssreflect.seq]
t:201 [in mathcomp.fingroup.gproduct]
t:2014 [in mathcomp.ssreflect.seq]
t:202 [in mathcomp.solvable.extremal]
T:2023 [in mathcomp.ssreflect.order]
t:2024 [in mathcomp.ssreflect.seq]
T:2027 [in mathcomp.ssreflect.order]
t:2028 [in mathcomp.ssreflect.seq]
t:2038 [in mathcomp.ssreflect.seq]
t:204 [in mathcomp.ssreflect.tuple]
T:2047 [in mathcomp.ssreflect.order]
t:2048 [in mathcomp.ssreflect.seq]
t:2056 [in mathcomp.ssreflect.seq]
T:2061 [in mathcomp.ssreflect.order]
t:207 [in mathcomp.solvable.burnside_app]
t:2074 [in mathcomp.ssreflect.seq]
t:208 [in mathcomp.solvable.extremal]
T:2083 [in mathcomp.ssreflect.order]
t:209 [in mathcomp.fingroup.perm]
t:209 [in mathcomp.solvable.extremal]
T:2093 [in mathcomp.ssreflect.order]
T:21 [in mathcomp.ssreflect.tuple]
t:210 [in mathcomp.solvable.extremal]
t:2103 [in mathcomp.ssreflect.seq]
T:2105 [in mathcomp.ssreflect.order]
t:2113 [in mathcomp.ssreflect.seq]
T:212 [in mathcomp.ssreflect.binomial]
t:212 [in mathcomp.fingroup.perm]
t:212 [in mathcomp.solvable.extremal]
t:2121 [in mathcomp.ssreflect.seq]
T:2124 [in mathcomp.ssreflect.order]
t:213 [in mathcomp.fingroup.perm]
t:2131 [in mathcomp.ssreflect.seq]
T:2131 [in mathcomp.ssreflect.order]
t:2139 [in mathcomp.ssreflect.seq]
t:214 [in mathcomp.fingroup.perm]
T:2147 [in mathcomp.ssreflect.seq]
T:2147 [in mathcomp.ssreflect.order]
t:215 [in mathcomp.solvable.extremal]
t:2154 [in mathcomp.ssreflect.seq]
T:2162 [in mathcomp.ssreflect.order]
t:2164 [in mathcomp.ssreflect.seq]
t:217 [in mathcomp.ssreflect.binomial]
T:217 [in mathcomp.ssreflect.order]
t:2171 [in mathcomp.ssreflect.seq]
T:2176 [in mathcomp.ssreflect.order]
t:2179 [in mathcomp.ssreflect.seq]
t:218 [in mathcomp.ssreflect.binomial]
t:218 [in mathcomp.solvable.extremal]
t:218 [in mathcomp.solvable.burnside_app]
T:2191 [in mathcomp.ssreflect.order]
t:2195 [in mathcomp.ssreflect.seq]
T:2195 [in mathcomp.ssreflect.order]
T:22 [in mathcomp.algebra.ring_quotient]
T:22 [in mathcomp.ssreflect.eqtype]
t:220 [in mathcomp.solvable.extremal]
T:2203 [in mathcomp.ssreflect.order]
t:221 [in mathcomp.fingroup.perm]
t:221 [in mathcomp.solvable.extremal]
T:2210 [in mathcomp.ssreflect.order]
t:222 [in mathcomp.fingroup.perm]
t:222 [in mathcomp.solvable.extremal]
t:223 [in mathcomp.fingroup.perm]
t:223 [in mathcomp.solvable.extremal]
T:224 [in mathcomp.ssreflect.choice]
T:224 [in mathcomp.ssreflect.order]
t:224 [in mathcomp.solvable.extremal]
T:2245 [in mathcomp.ssreflect.seq]
T:2255 [in mathcomp.ssreflect.seq]
T:2263 [in mathcomp.ssreflect.seq]
t:227 [in mathcomp.ssreflect.binomial]
t:227 [in mathcomp.solvable.extremal]
T:2271 [in mathcomp.ssreflect.seq]
T:2275 [in mathcomp.ssreflect.seq]
T:2281 [in mathcomp.ssreflect.seq]
t:2283 [in mathcomp.algebra.ssrnum]
t:2284 [in mathcomp.algebra.ssrnum]
T:2289 [in mathcomp.ssreflect.seq]
T:229 [in mathcomp.ssreflect.tuple]
t:2296 [in mathcomp.algebra.ssrnum]
t:2297 [in mathcomp.algebra.ssrnum]
T:2298 [in mathcomp.ssreflect.seq]
T:23 [in mathcomp.ssreflect.tuple]
t:23 [in mathcomp.solvable.primitive_action]
t:230 [in mathcomp.ssreflect.binomial]
T:2305 [in mathcomp.ssreflect.seq]
T:2309 [in mathcomp.ssreflect.seq]
T:231 [in mathcomp.ssreflect.tuple]
t:232 [in mathcomp.ssreflect.binomial]
t:232 [in mathcomp.solvable.extremal]
t:2320 [in mathcomp.algebra.ssrnum]
t:2321 [in mathcomp.algebra.ssrnum]
t:233 [in mathcomp.ssreflect.tuple]
T:2349 [in mathcomp.ssreflect.seq]
t:235 [in mathcomp.ssreflect.binomial]
T:2354 [in mathcomp.ssreflect.seq]
T:2358 [in mathcomp.ssreflect.seq]
t:236 [in mathcomp.ssreflect.binomial]
T:236 [in mathcomp.ssreflect.tuple]
T:236 [in mathcomp.ssreflect.choice]
T:236 [in mathcomp.ssreflect.path]
t:2360 [in mathcomp.algebra.ssrnum]
t:2361 [in mathcomp.algebra.ssrnum]
T:2363 [in mathcomp.ssreflect.seq]
T:2366 [in mathcomp.ssreflect.seq]
t:237 [in mathcomp.ssreflect.tuple]
T:237 [in mathcomp.ssreflect.choice]
t:237 [in mathcomp.solvable.extremal]
T:2371 [in mathcomp.ssreflect.seq]
t:238 [in mathcomp.ssreflect.binomial]
T:239 [in mathcomp.ssreflect.tuple]
T:239 [in mathcomp.ssreflect.path]
T:24 [in mathcomp.ssreflect.finset]
t:240 [in mathcomp.ssreflect.binomial]
T:2401 [in mathcomp.algebra.matrix]
t:241 [in mathcomp.ssreflect.binomial]
T:241 [in mathcomp.ssreflect.eqtype]
T:242 [in mathcomp.ssreflect.tuple]
t:242 [in mathcomp.solvable.extremal]
T:2423 [in mathcomp.algebra.matrix]
T:2427 [in mathcomp.algebra.matrix]
t:244 [in mathcomp.ssreflect.binomial]
t:244 [in mathcomp.solvable.extremal]
T:244 [in mathcomp.ssreflect.eqtype]
t:2444 [in mathcomp.ssreflect.seq]
T:245 [in mathcomp.ssreflect.choice]
t:245 [in mathcomp.solvable.extremal]
t:2452 [in mathcomp.ssreflect.seq]
t:2457 [in mathcomp.ssreflect.seq]
t:246 [in mathcomp.solvable.extremal]
t:2462 [in mathcomp.ssreflect.seq]
T:2463 [in mathcomp.algebra.matrix]
t:2465 [in mathcomp.ssreflect.seq]
t:2467 [in mathcomp.ssreflect.seq]
t:247 [in mathcomp.solvable.extremal]
t:2471 [in mathcomp.ssreflect.seq]
t:2473 [in mathcomp.ssreflect.seq]
t:248 [in mathcomp.solvable.extremal]
t:2480 [in mathcomp.ssreflect.seq]
T:2480 [in mathcomp.ssreflect.order]
T:2485 [in mathcomp.ssreflect.order]
T:2487 [in mathcomp.ssreflect.order]
T:2489 [in mathcomp.ssreflect.order]
t:249 [in mathcomp.solvable.extremal]
T:2491 [in mathcomp.ssreflect.order]
t:25 [in mathcomp.fingroup.perm]
t:25 [in mathcomp.ssreflect.tuple]
T:25 [in mathcomp.ssreflect.prime]
T:25 [in mathcomp.ssreflect.bigop]
t:252 [in mathcomp.ssreflect.binomial]
T:2533 [in mathcomp.ssreflect.order]
T:2535 [in mathcomp.ssreflect.order]
T:2552 [in mathcomp.ssreflect.order]
T:2554 [in mathcomp.ssreflect.order]
T:2556 [in mathcomp.ssreflect.order]
T:2558 [in mathcomp.ssreflect.order]
t:256 [in mathcomp.fingroup.perm]
T:2562 [in mathcomp.ssreflect.order]
T:2564 [in mathcomp.ssreflect.order]
T:2566 [in mathcomp.ssreflect.order]
T:2568 [in mathcomp.ssreflect.order]
T:2570 [in mathcomp.ssreflect.order]
T:2572 [in mathcomp.ssreflect.order]
T:2574 [in mathcomp.ssreflect.order]
T:2576 [in mathcomp.ssreflect.order]
T:2578 [in mathcomp.ssreflect.order]
T:2580 [in mathcomp.ssreflect.order]
T:2582 [in mathcomp.ssreflect.order]
T:2584 [in mathcomp.ssreflect.order]
T:2586 [in mathcomp.ssreflect.order]
t:2592 [in mathcomp.ssreflect.order]
t:2599 [in mathcomp.ssreflect.order]
T:2599 [in mathcomp.ssreflect.bigop]
T:26 [in mathcomp.ssreflect.order]
T:26 [in mathcomp.ssreflect.fintype]
T:261 [in mathcomp.ssreflect.eqtype]
T:2612 [in mathcomp.ssreflect.order]
t:2614 [in mathcomp.ssreflect.order]
t:2617 [in mathcomp.ssreflect.order]
t:2618 [in mathcomp.ssreflect.order]
t:2619 [in mathcomp.ssreflect.order]
t:2622 [in mathcomp.ssreflect.order]
t:2624 [in mathcomp.ssreflect.order]
t:2625 [in mathcomp.ssreflect.order]
t:2627 [in mathcomp.ssreflect.order]
T:2629 [in mathcomp.ssreflect.order]
T:2634 [in mathcomp.ssreflect.order]
T:2636 [in mathcomp.ssreflect.order]
T:2638 [in mathcomp.ssreflect.order]
t:264 [in mathcomp.ssreflect.binomial]
T:2640 [in mathcomp.ssreflect.order]
T:2648 [in mathcomp.algebra.matrix]
t:265 [in mathcomp.ssreflect.binomial]
T:266 [in mathcomp.ssreflect.eqtype]
T:2660 [in mathcomp.algebra.matrix]
T:2662 [in mathcomp.ssreflect.order]
T:2671 [in mathcomp.ssreflect.order]
T:2675 [in mathcomp.ssreflect.order]
T:2677 [in mathcomp.ssreflect.order]
T:2679 [in mathcomp.ssreflect.order]
t:268 [in mathcomp.ssreflect.binomial]
T:268 [in mathcomp.ssreflect.order]
T:2682 [in mathcomp.ssreflect.order]
T:2685 [in mathcomp.algebra.matrix]
T:2685 [in mathcomp.ssreflect.order]
T:2686 [in mathcomp.ssreflect.order]
T:2687 [in mathcomp.ssreflect.order]
T:27 [in mathcomp.ssreflect.generic_quotient]
T:27 [in mathcomp.ssreflect.eqtype]
T:2702 [in mathcomp.algebra.matrix]
T:2710 [in mathcomp.algebra.matrix]
t:272 [in mathcomp.ssreflect.binomial]
T:273 [in mathcomp.ssreflect.order]
T:2739 [in mathcomp.ssreflect.order]
T:2740 [in mathcomp.ssreflect.order]
T:2741 [in mathcomp.ssreflect.order]
T:2743 [in mathcomp.ssreflect.order]
T:2746 [in mathcomp.ssreflect.order]
T:2747 [in mathcomp.ssreflect.order]
T:2748 [in mathcomp.ssreflect.order]
t:276 [in mathcomp.ssreflect.binomial]
t:277 [in mathcomp.ssreflect.binomial]
T:277 [in mathcomp.fingroup.action]
T:277 [in mathcomp.ssreflect.order]
T:278 [in mathcomp.fingroup.action]
T:279 [in mathcomp.fingroup.action]
t:28 [in mathcomp.fingroup.perm]
T:28 [in mathcomp.ssreflect.fintype]
T:280 [in mathcomp.fingroup.action]
T:2806 [in mathcomp.ssreflect.order]
T:2808 [in mathcomp.ssreflect.order]
T:2809 [in mathcomp.ssreflect.order]
T:281 [in mathcomp.fingroup.action]
T:281 [in mathcomp.ssreflect.order]
T:2810 [in mathcomp.ssreflect.order]
T:2813 [in mathcomp.ssreflect.order]
T:2817 [in mathcomp.ssreflect.order]
T:2818 [in mathcomp.ssreflect.order]
T:2819 [in mathcomp.ssreflect.order]
T:2820 [in mathcomp.ssreflect.order]
T:2822 [in mathcomp.ssreflect.order]
T:2824 [in mathcomp.ssreflect.order]
T:2831 [in mathcomp.ssreflect.order]
T:285 [in mathcomp.ssreflect.order]
t:286 [in mathcomp.field.algebraics_fundamentals]
t:2868 [in mathcomp.ssreflect.order]
t:2871 [in mathcomp.ssreflect.order]
T:2875 [in mathcomp.ssreflect.order]
T:2877 [in mathcomp.ssreflect.order]
t:288 [in mathcomp.solvable.extremal]
t:2895 [in mathcomp.ssreflect.order]
t:2896 [in mathcomp.ssreflect.order]
t:2898 [in mathcomp.ssreflect.order]
t:2899 [in mathcomp.ssreflect.order]
T:29 [in mathcomp.field.closed_field]
T:2902 [in mathcomp.ssreflect.order]
T:2904 [in mathcomp.ssreflect.order]
T:2906 [in mathcomp.ssreflect.order]
T:2908 [in mathcomp.ssreflect.order]
T:2911 [in mathcomp.ssreflect.order]
T:2913 [in mathcomp.ssreflect.order]
T:2915 [in mathcomp.ssreflect.order]
T:2917 [in mathcomp.ssreflect.order]
T:2919 [in mathcomp.ssreflect.order]
T:2921 [in mathcomp.ssreflect.order]
T:2923 [in mathcomp.ssreflect.order]
T:2925 [in mathcomp.ssreflect.order]
T:2927 [in mathcomp.ssreflect.order]
T:2929 [in mathcomp.ssreflect.order]
T:2931 [in mathcomp.ssreflect.order]
T:2933 [in mathcomp.ssreflect.order]
T:2935 [in mathcomp.ssreflect.order]
T:2938 [in mathcomp.ssreflect.order]
T:2942 [in mathcomp.ssreflect.order]
T:2943 [in mathcomp.ssreflect.order]
T:2944 [in mathcomp.ssreflect.order]
T:2945 [in mathcomp.ssreflect.order]
T:2947 [in mathcomp.ssreflect.order]
T:2949 [in mathcomp.ssreflect.order]
T:2955 [in mathcomp.ssreflect.order]
T:296 [in mathcomp.ssreflect.order]
T:2961 [in mathcomp.ssreflect.order]
T:2968 [in mathcomp.ssreflect.order]
T:2970 [in mathcomp.ssreflect.order]
t:2973 [in mathcomp.ssreflect.order]
t:2976 [in mathcomp.ssreflect.order]
T:2979 [in mathcomp.ssreflect.order]
T:2982 [in mathcomp.ssreflect.order]
T:2984 [in mathcomp.ssreflect.order]
T:2986 [in mathcomp.ssreflect.order]
T:2988 [in mathcomp.ssreflect.order]
T:2990 [in mathcomp.ssreflect.order]
T:2992 [in mathcomp.ssreflect.order]
T:2994 [in mathcomp.ssreflect.order]
T:2996 [in mathcomp.ssreflect.order]
T:3 [in mathcomp.ssreflect.ssreflect]
T:30 [in mathcomp.ssreflect.order]
T:30 [in mathcomp.ssreflect.fintype]
T:300 [in mathcomp.ssreflect.order]
T:3000 [in mathcomp.ssreflect.order]
T:3002 [in mathcomp.ssreflect.order]
t:301 [in mathcomp.fingroup.perm]
t:301 [in mathcomp.field.closed_field]
T:3022 [in mathcomp.ssreflect.order]
T:3024 [in mathcomp.ssreflect.order]
T:3026 [in mathcomp.ssreflect.order]
T:3046 [in mathcomp.ssreflect.order]
t:306 [in mathcomp.field.closed_field]
T:307 [in mathcomp.ssreflect.order]
T:3075 [in mathcomp.ssreflect.order]
T:3084 [in mathcomp.ssreflect.order]
T:31 [in mathcomp.ssreflect.generic_quotient]
t:31 [in mathcomp.ssreflect.tuple]
t:31 [in mathcomp.ssreflect.choice]
t:31 [in mathcomp.solvable.primitive_action]
T:31 [in mathcomp.ssreflect.prime]
t:310 [in mathcomp.field.closed_field]
T:311 [in mathcomp.ssreflect.order]
T:316 [in mathcomp.ssreflect.order]
T:316 [in mathcomp.ssreflect.eqtype]
T:32 [in mathcomp.algebra.interval]
t:32 [in mathcomp.solvable.primitive_action]
T:32 [in mathcomp.ssreflect.bigop]
T:320 [in mathcomp.ssreflect.order]
T:324 [in mathcomp.ssreflect.order]
T:327 [in mathcomp.ssreflect.eqtype]
T:328 [in mathcomp.ssreflect.order]
t:33 [in mathcomp.fingroup.perm]
T:33 [in mathcomp.algebra.interval]
T:330 [in mathcomp.ssreflect.eqtype]
T:332 [in mathcomp.ssreflect.order]
t:336 [in mathcomp.field.closed_field]
T:336 [in mathcomp.ssreflect.order]
T:339 [in mathcomp.ssreflect.order]
T:34 [in mathcomp.ssreflect.generic_quotient]
T:34 [in mathcomp.algebra.interval]
t:34 [in mathcomp.solvable.primitive_action]
T:34 [in mathcomp.ssreflect.fintype]
T:340 [in mathcomp.ssreflect.eqtype]
t:341 [in mathcomp.field.closed_field]
T:348 [in mathcomp.ssreflect.eqtype]
T:35 [in mathcomp.algebra.interval]
t:35 [in mathcomp.ssreflect.choice]
T:35 [in mathcomp.field.closed_field]
T:355 [in mathcomp.ssreflect.tuple]
T:357 [in mathcomp.ssreflect.tuple]
t:358 [in mathcomp.ssreflect.tuple]
T:36 [in mathcomp.algebra.interval]
T:360 [in mathcomp.ssreflect.tuple]
T:363 [in mathcomp.ssreflect.tuple]
T:365 [in mathcomp.ssreflect.tuple]
T:367 [in mathcomp.ssreflect.tuple]
T:37 [in mathcomp.algebra.interval]
t:37 [in mathcomp.ssreflect.tuple]
T:371 [in mathcomp.ssreflect.tuple]
T:372 [in mathcomp.ssreflect.eqtype]
t:373 [in mathcomp.ssreflect.tuple]
T:375 [in mathcomp.ssreflect.tuple]
T:375 [in mathcomp.ssreflect.eqtype]
T:377 [in mathcomp.ssreflect.tuple]
T:379 [in mathcomp.ssreflect.ssrnat]
T:38 [in mathcomp.ssreflect.finset]
T:381 [in mathcomp.ssreflect.tuple]
T:381 [in mathcomp.ssreflect.eqtype]
T:383 [in mathcomp.ssreflect.tuple]
T:385 [in mathcomp.ssreflect.tuple]
T:385 [in mathcomp.ssreflect.eqtype]
t:388 [in mathcomp.ssreflect.seq]
T:390 [in mathcomp.ssreflect.eqtype]
t:391 [in mathcomp.ssreflect.seq]
t:394 [in mathcomp.ssreflect.seq]
T:4 [in mathcomp.algebra.interval]
T:4 [in mathcomp.ssreflect.fintype]
T:40 [in mathcomp.field.closed_field]
T:40 [in mathcomp.ssreflect.bigop]
t:400 [in mathcomp.ssreflect.seq]
t:402 [in mathcomp.algebra.ssrnum]
t:406 [in mathcomp.algebra.ssrnum]
t:41 [in mathcomp.ssreflect.tuple]
T:41 [in mathcomp.ssreflect.order]
t:410 [in mathcomp.algebra.ssrnum]
t:414 [in mathcomp.algebra.ssrnum]
t:418 [in mathcomp.algebra.ssrnum]
t:42 [in mathcomp.solvable.primitive_action]
T:42 [in mathcomp.algebra.ring_quotient]
T:42 [in mathcomp.fingroup.fingroup]
t:42 [in mathcomp.solvable.extremal]
T:420 [in mathcomp.ssreflect.seq]
t:422 [in mathcomp.algebra.ssrnum]
T:424 [in mathcomp.ssreflect.order]
t:425 [in mathcomp.ssreflect.seq]
t:426 [in mathcomp.algebra.ssrnum]
t:427 [in mathcomp.ssreflect.seq]
t:43 [in mathcomp.ssreflect.choice]
t:43 [in mathcomp.solvable.primitive_action]
T:43 [in mathcomp.fingroup.fingroup]
t:430 [in mathcomp.algebra.ssrnum]
t:433 [in mathcomp.ssreflect.order]
t:438 [in mathcomp.character.inertia]
T:45 [in mathcomp.ssreflect.bigop]
T:451 [in mathcomp.fingroup.action]
T:46 [in mathcomp.fingroup.fingroup]
t:47 [in mathcomp.ssreflect.choice]
t:47 [in mathcomp.solvable.primitive_action]
T:47 [in mathcomp.ssreflect.order]
t:472 [in mathcomp.fingroup.gproduct]
t:477 [in mathcomp.character.inertia]
t:494 [in mathcomp.ssreflect.path]
t:498 [in mathcomp.ssreflect.seq]
t:5 [in mathcomp.ssreflect.tuple]
t:5 [in mathcomp.fingroup.presentation]
T:5 [in mathcomp.ssreflect.eqtype]
t:50 [in mathcomp.solvable.primitive_action]
T:50 [in mathcomp.field.closed_field]
t:502 [in mathcomp.ssreflect.seq]
t:51 [in mathcomp.ssreflect.choice]
T:516 [in mathcomp.ssreflect.path]
T:53 [in mathcomp.solvable.alt]
t:53 [in mathcomp.ssreflect.tuple]
t:53 [in mathcomp.field.closed_field]
T:53 [in mathcomp.ssreflect.fintype]
T:532 [in mathcomp.ssreflect.fintype]
t:537 [in mathcomp.character.inertia]
T:539 [in mathcomp.ssreflect.path]
t:54 [in mathcomp.fingroup.perm]
t:54 [in mathcomp.solvable.primitive_action]
t:54 [in mathcomp.field.separable]
T:54 [in mathcomp.ssreflect.order]
T:54 [in mathcomp.ssreflect.bigop]
t:540 [in mathcomp.character.character]
T:540 [in mathcomp.ssreflect.fintype]
T:545 [in mathcomp.ssreflect.path]
t:55 [in mathcomp.ssreflect.tuple]
t:55 [in mathcomp.solvable.burnside_app]
T:55 [in mathcomp.ssreflect.fintype]
T:550 [in mathcomp.ssreflect.path]
t:551 [in mathcomp.character.character]
T:554 [in mathcomp.ssreflect.path]
t:557 [in mathcomp.character.character]
T:559 [in mathcomp.ssreflect.ssrnat]
t:57 [in mathcomp.solvable.primitive_action]
T:574 [in mathcomp.ssreflect.path]
T:58 [in mathcomp.ssreflect.choice]
T:580 [in mathcomp.ssreflect.path]
T:586 [in mathcomp.ssreflect.path]
t:59 [in mathcomp.ssreflect.tuple]
T:59 [in mathcomp.ssreflect.choice]
T:593 [in mathcomp.ssreflect.path]
T:599 [in mathcomp.ssreflect.path]
T:6 [in mathcomp.solvable.alt]
t:6 [in mathcomp.ssreflect.tuple]
T:6 [in mathcomp.ssreflect.finset]
T:6 [in mathcomp.ssreflect.bigop]
T:60 [in mathcomp.ssreflect.bigop]
T:622 [in mathcomp.ssreflect.ssrnat]
T:626 [in mathcomp.ssreflect.fintype]
t:631 [in mathcomp.ssreflect.seq]
t:631 [in mathcomp.ssreflect.path]
t:633 [in mathcomp.ssreflect.path]
t:635 [in mathcomp.ssreflect.path]
T:64 [in mathcomp.algebra.ring_quotient]
T:64 [in mathcomp.ssreflect.prime]
t:642 [in mathcomp.ssreflect.path]
t:644 [in mathcomp.ssreflect.path]
T:649 [in mathcomp.ssreflect.path]
T:65 [in mathcomp.ssreflect.bigop]
T:652 [in mathcomp.ssreflect.path]
T:656 [in mathcomp.ssreflect.path]
t:66 [in mathcomp.ssreflect.tuple]
T:660 [in mathcomp.ssreflect.path]
T:664 [in mathcomp.ssreflect.path]
t:67 [in mathcomp.ssreflect.ssrAC]
T:670 [in mathcomp.ssreflect.fintype]
T:674 [in mathcomp.ssreflect.path]
T:679 [in mathcomp.ssreflect.fintype]
t:68 [in mathcomp.ssreflect.tuple]
T:685 [in mathcomp.ssreflect.fintype]
T:693 [in mathcomp.ssreflect.fintype]
T:7 [in mathcomp.solvable.alt]
T:7 [in mathcomp.algebra.interval]
t:7 [in mathcomp.ssreflect.tuple]
T:70 [in mathcomp.ssreflect.ssrAC]
t:72 [in mathcomp.ssreflect.tuple]
T:722 [in mathcomp.ssreflect.fintype]
t:73 [in mathcomp.ssreflect.tuple]
T:73 [in mathcomp.ssreflect.choice]
T:731 [in mathcomp.ssreflect.seq]
T:731 [in mathcomp.ssreflect.fintype]
T:733 [in mathcomp.ssreflect.seq]
T:74 [in mathcomp.ssreflect.bigop]
T:740 [in mathcomp.ssreflect.fintype]
t:75 [in mathcomp.ssreflect.tuple]
T:751 [in mathcomp.ssreflect.fintype]
t:76 [in mathcomp.solvable.extremal]
t:77 [in mathcomp.ssreflect.tuple]
t:77 [in mathcomp.solvable.extremal]
T:77 [in mathcomp.ssreflect.ssrbool]
t:770 [in mathcomp.ssreflect.order]
T:771 [in mathcomp.ssreflect.seq]
t:774 [in mathcomp.ssreflect.order]
T:776 [in mathcomp.ssreflect.seq]
t:78 [in mathcomp.ssreflect.tuple]
T:785 [in mathcomp.ssreflect.path]
T:79 [in mathcomp.ssreflect.ssrAC]
T:8 [in mathcomp.solvable.alt]
T:8 [in mathcomp.fingroup.perm]
T:8 [in mathcomp.ssreflect.generic_quotient]
T:8 [in mathcomp.ssreflect.finset]
T:8 [in mathcomp.ssreflect.fintype]
t:80 [in mathcomp.ssreflect.tuple]
T:80 [in mathcomp.solvable.sylow]
T:80 [in mathcomp.ssreflect.bigop]
t:82 [in mathcomp.ssreflect.tuple]
t:83 [in mathcomp.ssreflect.tuple]
t:84 [in mathcomp.ssreflect.tuple]
T:845 [in mathcomp.ssreflect.fintype]
T:848 [in mathcomp.ssreflect.fintype]
t:85 [in mathcomp.ssreflect.tuple]
t:850 [in mathcomp.ssreflect.seq]
t:858 [in mathcomp.ssreflect.bigop]
t:86 [in mathcomp.ssreflect.tuple]
T:863 [in mathcomp.algebra.matrix]
t:87 [in mathcomp.ssreflect.tuple]
T:87 [in mathcomp.algebra.ring_quotient]
t:88 [in mathcomp.ssreflect.tuple]
T:88 [in mathcomp.ssreflect.bigop]
T:883 [in mathcomp.ssreflect.finset]
t:884 [in mathcomp.ssreflect.seq]
T:887 [in mathcomp.ssreflect.finset]
t:89 [in mathcomp.ssreflect.tuple]
T:890 [in mathcomp.ssreflect.finset]
T:895 [in mathcomp.ssreflect.finset]
T:9 [in mathcomp.ssreflect.eqtype]
t:90 [in mathcomp.ssreflect.tuple]
T:90 [in mathcomp.ssreflect.finfun]
t:901 [in mathcomp.ssreflect.bigop]
t:91 [in mathcomp.ssreflect.tuple]
t:93 [in mathcomp.ssreflect.tuple]
T:93 [in mathcomp.ssreflect.bigop]
t:94 [in mathcomp.ssreflect.finfun]
t:942 [in mathcomp.ssreflect.order]
t:946 [in mathcomp.ssreflect.order]
T:95 [in mathcomp.ssreflect.generic_quotient]
t:95 [in mathcomp.ssreflect.tuple]
t:950 [in mathcomp.ssreflect.order]
t:954 [in mathcomp.ssreflect.order]
T:957 [in mathcomp.ssreflect.order]
T:97 [in mathcomp.ssreflect.ssrAC]
t:98 [in mathcomp.ssreflect.tuple]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (71649 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1792 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (46193 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (266 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3623 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (91 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14204 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (259 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (134 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (44 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1276 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (682 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3041 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |