| 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 | (69505 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 | (1943 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 | (39748 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 | (379 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 | (3958 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 | (13542 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 | (480 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (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 | (452 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 | (1344 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 | (1014 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 | (6127 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 | (248 entries) |
T (binder)
takeD:2085 [in mathcomp.ssreflect.seq]take_addn:2084 [in mathcomp.ssreflect.seq]
tauS:190 [in mathcomp.character.vcharacter]
tauS:493 [in mathcomp.character.classfun]
tau:140 [in mathcomp.character.classfun]
tau:144 [in mathcomp.character.classfun]
tau:191 [in mathcomp.character.vcharacter]
tau:192 [in mathcomp.character.vcharacter]
tau:194 [in mathcomp.character.vcharacter]
tau:195 [in mathcomp.character.vcharacter]
tau:487 [in mathcomp.character.classfun]
tau:490 [in mathcomp.character.classfun]
tau:491 [in mathcomp.character.classfun]
tau:494 [in mathcomp.character.classfun]
tau:495 [in mathcomp.character.classfun]
tau:497 [in mathcomp.character.classfun]
test:16 [in mathcomp.ssreflect.ssreflect]
theta:365 [in mathcomp.character.inertia]
theta:406 [in mathcomp.character.inertia]
theta:418 [in mathcomp.character.inertia]
theta:452 [in mathcomp.character.inertia]
toL:354 [in mathcomp.field.fieldext]
toL:355 [in mathcomp.field.fieldext]
toPF:353 [in mathcomp.field.fieldext]
to':31 [in mathcomp.fingroup.action]
to:12 [in mathcomp.fingroup.action]
to:154 [in mathcomp.solvable.frobenius]
to:30 [in mathcomp.fingroup.action]
to:35 [in mathcomp.solvable.frobenius]
to:37 [in mathcomp.fingroup.action]
to:39 [in mathcomp.fingroup.action]
to:4 [in mathcomp.fingroup.action]
to:421 [in mathcomp.fingroup.action]
to:424 [in mathcomp.fingroup.action]
to:43 [in mathcomp.fingroup.action]
to:46 [in mathcomp.fingroup.action]
to:5 [in mathcomp.solvable.burnside_app]
to:503 [in mathcomp.fingroup.gproduct]
to:507 [in mathcomp.fingroup.gproduct]
to:51 [in mathcomp.fingroup.action]
to:56 [in mathcomp.fingroup.action]
to:580 [in mathcomp.fingroup.action]
to:584 [in mathcomp.fingroup.action]
to:591 [in mathcomp.fingroup.action]
to:595 [in mathcomp.fingroup.action]
to:598 [in mathcomp.fingroup.action]
to:60 [in mathcomp.fingroup.action]
to:601 [in mathcomp.fingroup.action]
to:64 [in mathcomp.fingroup.action]
to:69 [in mathcomp.fingroup.action]
to:72 [in mathcomp.fingroup.action]
to:8 [in mathcomp.fingroup.action]
tP:171 [in mathcomp.ssreflect.choice]
tP:174 [in mathcomp.ssreflect.choice]
tP:177 [in mathcomp.ssreflect.choice]
ts:208 [in mathcomp.fingroup.perm]
ts:210 [in mathcomp.fingroup.perm]
ts:215 [in mathcomp.fingroup.perm]
ts:320 [in mathcomp.field.closed_field]
tuple_permP:312 [in mathcomp.fingroup.perm]
tuple_perm_eqP:311 [in mathcomp.fingroup.perm]
Tx:134 [in mathcomp.character.inertia]
ty':2 [in mathcomp.ssreflect.ssrAC]
ty:1 [in mathcomp.ssreflect.ssrAC]
ty:5 [in mathcomp.ssreflect.ssrAC]
T':103 [in mathcomp.ssreflect.generic_quotient]
T':109 [in mathcomp.fingroup.perm]
T':1361 [in mathcomp.ssreflect.order]
T':142 [in mathcomp.ssreflect.fingraph]
t':1735 [in mathcomp.algebra.ssralg]
T':178 [in mathcomp.ssreflect.generic_quotient]
T':1936 [in mathcomp.ssreflect.seq]
T':205 [in mathcomp.ssreflect.tuple]
T':2188 [in mathcomp.ssreflect.order]
T':2193 [in mathcomp.ssreflect.order]
T':2195 [in mathcomp.ssreflect.order]
T':2197 [in mathcomp.ssreflect.order]
T':2199 [in mathcomp.ssreflect.order]
T':2241 [in mathcomp.ssreflect.order]
T':2243 [in mathcomp.ssreflect.order]
T':2260 [in mathcomp.ssreflect.order]
T':2262 [in mathcomp.ssreflect.order]
T':2264 [in mathcomp.ssreflect.order]
T':2266 [in mathcomp.ssreflect.order]
T':2270 [in mathcomp.ssreflect.order]
T':2272 [in mathcomp.ssreflect.order]
T':2274 [in mathcomp.ssreflect.order]
T':2276 [in mathcomp.ssreflect.order]
T':2278 [in mathcomp.ssreflect.order]
T':2280 [in mathcomp.ssreflect.order]
T':2282 [in mathcomp.ssreflect.order]
T':2284 [in mathcomp.ssreflect.order]
T':2286 [in mathcomp.ssreflect.order]
T':2288 [in mathcomp.ssreflect.order]
T':2290 [in mathcomp.ssreflect.order]
T':2292 [in mathcomp.ssreflect.order]
T':2294 [in mathcomp.ssreflect.order]
T':2337 [in mathcomp.ssreflect.order]
T':2340 [in mathcomp.ssreflect.order]
T':2343 [in mathcomp.ssreflect.order]
T':2346 [in mathcomp.ssreflect.order]
T':2350 [in mathcomp.ssreflect.order]
T':2355 [in mathcomp.ssreflect.order]
T':2357 [in mathcomp.ssreflect.order]
T':2359 [in mathcomp.ssreflect.order]
T':2361 [in mathcomp.ssreflect.order]
T':2389 [in mathcomp.ssreflect.order]
T':2391 [in mathcomp.ssreflect.order]
T':2393 [in mathcomp.ssreflect.order]
T':2395 [in mathcomp.ssreflect.order]
T':2398 [in mathcomp.ssreflect.order]
T':2402 [in mathcomp.ssreflect.order]
T':2404 [in mathcomp.ssreflect.order]
T':2406 [in mathcomp.ssreflect.order]
T':2408 [in mathcomp.ssreflect.order]
T':2410 [in mathcomp.ssreflect.order]
T':2412 [in mathcomp.ssreflect.order]
T':2414 [in mathcomp.ssreflect.order]
T':2416 [in mathcomp.ssreflect.order]
T':2418 [in mathcomp.ssreflect.order]
T':2420 [in mathcomp.ssreflect.order]
T':2422 [in mathcomp.ssreflect.order]
T':2424 [in mathcomp.ssreflect.order]
T':430 [in mathcomp.ssreflect.fintype]
T':438 [in mathcomp.ssreflect.fintype]
T':684 [in mathcomp.ssreflect.path]
T':740 [in mathcomp.ssreflect.fintype]
T':745 [in mathcomp.ssreflect.fintype]
t':76 [in mathcomp.solvable.primitive_action]
t':77 [in mathcomp.solvable.primitive_action]
T':871 [in mathcomp.ssreflect.order]
T0:1 [in mathcomp.ssreflect.order]
T0:166 [in mathcomp.ssreflect.order]
T0:203 [in mathcomp.ssreflect.order]
T0:258 [in mathcomp.ssreflect.order]
T0:286 [in mathcomp.ssreflect.order]
T0:317 [in mathcomp.ssreflect.order]
T0:82 [in mathcomp.ssreflect.order]
t1:108 [in mathcomp.solvable.burnside_app]
T1:1155 [in mathcomp.algebra.mxalgebra]
T1:1214 [in mathcomp.ssreflect.seq]
T1:1233 [in mathcomp.ssreflect.seq]
T1:1294 [in mathcomp.ssreflect.order]
t1:13 [in mathcomp.ssreflect.tuple]
t1:1456 [in mathcomp.ssreflect.seq]
t1:155 [in mathcomp.ssreflect.tuple]
t1:1648 [in mathcomp.ssreflect.seq]
t1:1715 [in mathcomp.algebra.ssralg]
t1:1748 [in mathcomp.ssreflect.seq]
t1:1776 [in mathcomp.ssreflect.seq]
t1:1870 [in mathcomp.ssreflect.seq]
T1:192 [in mathcomp.ssreflect.choice]
T1:194 [in mathcomp.ssreflect.choice]
T1:196 [in mathcomp.ssreflect.choice]
T1:198 [in mathcomp.ssreflect.choice]
t1:2576 [in mathcomp.ssreflect.order]
t1:2581 [in mathcomp.ssreflect.order]
t1:2587 [in mathcomp.ssreflect.order]
t1:2590 [in mathcomp.ssreflect.order]
t1:2593 [in mathcomp.ssreflect.order]
t1:2596 [in mathcomp.ssreflect.order]
t1:2600 [in mathcomp.ssreflect.order]
t1:2603 [in mathcomp.ssreflect.order]
t1:2605 [in mathcomp.ssreflect.order]
t1:2608 [in mathcomp.ssreflect.order]
t1:2625 [in mathcomp.ssreflect.order]
t1:2628 [in mathcomp.ssreflect.order]
t1:2631 [in mathcomp.ssreflect.order]
t1:2633 [in mathcomp.ssreflect.order]
t1:2635 [in mathcomp.ssreflect.order]
t1:2697 [in mathcomp.ssreflect.order]
t1:2703 [in mathcomp.ssreflect.order]
t1:2709 [in mathcomp.ssreflect.order]
T1:273 [in mathcomp.ssreflect.choice]
T1:275 [in mathcomp.ssreflect.choice]
T1:277 [in mathcomp.ssreflect.choice]
T1:279 [in mathcomp.ssreflect.choice]
T1:380 [in mathcomp.ssreflect.eqtype]
T1:4 [in mathcomp.field.closed_field]
T1:43 [in mathcomp.field.closed_field]
T1:7 [in mathcomp.field.closed_field]
T1:764 [in mathcomp.ssreflect.order]
t1:791 [in mathcomp.ssreflect.seq]
t1:804 [in mathcomp.ssreflect.seq]
t2:109 [in mathcomp.solvable.burnside_app]
T2:1156 [in mathcomp.algebra.mxalgebra]
T2:1215 [in mathcomp.ssreflect.seq]
T2:1234 [in mathcomp.ssreflect.seq]
T2:1295 [in mathcomp.ssreflect.order]
t2:14 [in mathcomp.ssreflect.tuple]
t2:1457 [in mathcomp.ssreflect.seq]
t2:156 [in mathcomp.ssreflect.tuple]
t2:1649 [in mathcomp.ssreflect.seq]
t2:1750 [in mathcomp.ssreflect.seq]
t2:1777 [in mathcomp.ssreflect.seq]
t2:1872 [in mathcomp.ssreflect.seq]
T2:193 [in mathcomp.ssreflect.choice]
T2:195 [in mathcomp.ssreflect.choice]
T2:197 [in mathcomp.ssreflect.choice]
T2:199 [in mathcomp.ssreflect.choice]
t2:2577 [in mathcomp.ssreflect.order]
t2:2582 [in mathcomp.ssreflect.order]
t2:2588 [in mathcomp.ssreflect.order]
t2:2591 [in mathcomp.ssreflect.order]
t2:2594 [in mathcomp.ssreflect.order]
t2:2597 [in mathcomp.ssreflect.order]
t2:2599 [in mathcomp.ssreflect.order]
t2:2604 [in mathcomp.ssreflect.order]
t2:2606 [in mathcomp.ssreflect.order]
t2:2609 [in mathcomp.ssreflect.order]
t2:2626 [in mathcomp.ssreflect.order]
t2:2629 [in mathcomp.ssreflect.order]
t2:2632 [in mathcomp.ssreflect.order]
t2:2634 [in mathcomp.ssreflect.order]
t2:2636 [in mathcomp.ssreflect.order]
t2:2698 [in mathcomp.ssreflect.order]
t2:2704 [in mathcomp.ssreflect.order]
t2:2710 [in mathcomp.ssreflect.order]
T2:274 [in mathcomp.ssreflect.choice]
T2:276 [in mathcomp.ssreflect.choice]
T2:278 [in mathcomp.ssreflect.choice]
T2:280 [in mathcomp.ssreflect.choice]
T2:381 [in mathcomp.ssreflect.eqtype]
T2:45 [in mathcomp.field.closed_field]
T2:765 [in mathcomp.ssreflect.order]
t2:792 [in mathcomp.ssreflect.seq]
T2:8 [in mathcomp.field.closed_field]
t2:805 [in mathcomp.ssreflect.seq]
T:1 [in mathcomp.algebra.interval]
T:1 [in mathcomp.fingroup.fingroup]
T:1 [in mathcomp.ssreflect.ssrbool]
T:1 [in mathcomp.ssreflect.fingraph]
T:1 [in mathcomp.ssreflect.ssrfun]
T:1 [in mathcomp.ssreflect.eqtype]
T:10 [in mathcomp.fingroup.perm]
t:10 [in mathcomp.ssreflect.tuple]
T:10 [in mathcomp.ssreflect.finset]
T:10 [in mathcomp.algebra.finalg]
t:100 [in mathcomp.ssreflect.tuple]
T:1009 [in mathcomp.ssreflect.order]
T:102 [in mathcomp.ssreflect.generic_quotient]
t:103 [in mathcomp.ssreflect.tuple]
t:104 [in mathcomp.ssreflect.tuple]
T:1052 [in mathcomp.algebra.ssralg]
t:106 [in mathcomp.ssreflect.tuple]
T:1066 [in mathcomp.ssreflect.finset]
t:107 [in mathcomp.field.closed_field]
T:1070 [in mathcomp.algebra.ssralg]
T:108 [in mathcomp.fingroup.perm]
t:1089 [in mathcomp.ssreflect.order]
t:109 [in mathcomp.ssreflect.tuple]
t:112 [in mathcomp.ssreflect.tuple]
T:112 [in mathcomp.ssreflect.path]
T:112 [in mathcomp.ssreflect.order]
t:112 [in mathcomp.solvable.extremal]
T:113 [in mathcomp.ssreflect.finfun]
T:1134 [in mathcomp.ssreflect.seq]
t:1136 [in mathcomp.ssreflect.order]
T:1137 [in mathcomp.ssreflect.seq]
T:114 [in mathcomp.fingroup.perm]
T:1141 [in mathcomp.ssreflect.seq]
T:1148 [in mathcomp.ssreflect.order]
T:115 [in mathcomp.ssreflect.fintype]
t:116 [in mathcomp.ssreflect.tuple]
T:118 [in mathcomp.fingroup.perm]
t:118 [in mathcomp.ssreflect.tuple]
T:118 [in mathcomp.ssreflect.fintype]
t:1185 [in mathcomp.ssreflect.order]
t:1189 [in mathcomp.ssreflect.order]
T:119 [in mathcomp.ssreflect.eqtype]
T:1190 [in mathcomp.algebra.mxalgebra]
t:1193 [in mathcomp.ssreflect.order]
t:1197 [in mathcomp.ssreflect.order]
t:12 [in mathcomp.ssreflect.tuple]
T:12 [in mathcomp.algebra.countalg]
T:12 [in mathcomp.ssreflect.finset]
T:12 [in mathcomp.fingroup.fingroup]
t:1205 [in mathcomp.ssreflect.seq]
t:121 [in mathcomp.fingroup.perm]
t:121 [in mathcomp.ssreflect.tuple]
T:121 [in mathcomp.ssreflect.fintype]
t:1213 [in mathcomp.ssreflect.seq]
T:122 [in mathcomp.fingroup.action]
T:1238 [in mathcomp.ssreflect.seq]
T:1239 [in mathcomp.algebra.ssralg]
t:125 [in mathcomp.ssreflect.tuple]
t:1254 [in mathcomp.ssreflect.seq]
T:1257 [in mathcomp.algebra.ssralg]
T:126 [in mathcomp.ssreflect.fintype]
T:127 [in mathcomp.ssreflect.eqtype]
t:1271 [in mathcomp.ssreflect.seq]
t:128 [in mathcomp.ssreflect.tuple]
T:129 [in mathcomp.ssreflect.order]
t:1298 [in mathcomp.ssreflect.order]
T:13 [in mathcomp.fingroup.perm]
T:13 [in mathcomp.ssreflect.generic_quotient]
t:13 [in mathcomp.fingroup.presentation]
t:1301 [in mathcomp.ssreflect.order]
t:1304 [in mathcomp.ssreflect.order]
t:1307 [in mathcomp.ssreflect.order]
T:131 [in mathcomp.ssreflect.binomial]
T:131 [in mathcomp.ssreflect.order]
t:1310 [in mathcomp.ssreflect.order]
t:1313 [in mathcomp.ssreflect.order]
t:1316 [in mathcomp.ssreflect.order]
t:1319 [in mathcomp.ssreflect.order]
t:1322 [in mathcomp.ssreflect.order]
t:1325 [in mathcomp.ssreflect.order]
t:1329 [in mathcomp.ssreflect.order]
T:133 [in mathcomp.ssreflect.tuple]
t:1331 [in mathcomp.ssreflect.seq]
t:1333 [in mathcomp.ssreflect.order]
t:1337 [in mathcomp.ssreflect.order]
t:134 [in mathcomp.ssreflect.binomial]
t:134 [in mathcomp.ssreflect.tuple]
t:1341 [in mathcomp.ssreflect.order]
t:1345 [in mathcomp.ssreflect.order]
t:1349 [in mathcomp.ssreflect.order]
t:135 [in mathcomp.ssreflect.binomial]
T:135 [in mathcomp.ssreflect.order]
t:1353 [in mathcomp.ssreflect.order]
t:1357 [in mathcomp.ssreflect.order]
t:136 [in mathcomp.ssreflect.binomial]
T:1360 [in mathcomp.ssreflect.seq]
T:1360 [in mathcomp.ssreflect.order]
t:137 [in mathcomp.ssreflect.binomial]
T:137 [in mathcomp.ssreflect.tuple]
t:138 [in mathcomp.ssreflect.binomial]
t:138 [in mathcomp.ssreflect.tuple]
T:139 [in mathcomp.algebra.ssrnum]
T:14 [in mathcomp.field.closed_field]
T:14 [in mathcomp.fingroup.fingroup]
T:14 [in mathcomp.ssreflect.eqtype]
T:140 [in mathcomp.ssreflect.binomial]
t:142 [in mathcomp.ssreflect.tuple]
T:1427 [in mathcomp.ssreflect.order]
t:1427 [in mathcomp.character.mxrepresentation]
T:1433 [in mathcomp.ssreflect.order]
t:1434 [in mathcomp.ssreflect.seq]
t:1439 [in mathcomp.ssreflect.seq]
t:1439 [in mathcomp.character.mxrepresentation]
T:144 [in mathcomp.ssreflect.binomial]
T:1440 [in mathcomp.ssreflect.order]
t:1445 [in mathcomp.ssreflect.seq]
t:1447 [in mathcomp.ssreflect.seq]
t:1449 [in mathcomp.ssreflect.seq]
t:145 [in mathcomp.ssreflect.tuple]
t:1451 [in mathcomp.ssreflect.seq]
t:1453 [in mathcomp.ssreflect.seq]
T:146 [in mathcomp.ssreflect.binomial]
t:1461 [in mathcomp.ssreflect.seq]
t:1465 [in mathcomp.ssreflect.seq]
t:1468 [in mathcomp.ssreflect.seq]
t:1472 [in mathcomp.ssreflect.seq]
T:1473 [in mathcomp.ssreflect.order]
t:1474 [in mathcomp.ssreflect.seq]
t:148 [in mathcomp.ssreflect.tuple]
T:1496 [in mathcomp.ssreflect.order]
T:15 [in mathcomp.fingroup.perm]
t:15 [in mathcomp.ssreflect.tuple]
T:15 [in mathcomp.algebra.finalg]
T:15 [in mathcomp.ssreflect.eqtype]
T:1502 [in mathcomp.ssreflect.order]
T:1509 [in mathcomp.ssreflect.order]
t:151 [in mathcomp.ssreflect.tuple]
T:153 [in mathcomp.ssreflect.order]
t:1537 [in mathcomp.ssreflect.order]
t:1541 [in mathcomp.ssreflect.order]
T:155 [in mathcomp.ssreflect.generic_quotient]
T:1551 [in mathcomp.ssreflect.seq]
t:1553 [in mathcomp.ssreflect.order]
T:1555 [in mathcomp.ssreflect.seq]
T:1560 [in mathcomp.ssreflect.seq]
T:1563 [in mathcomp.ssreflect.seq]
T:1564 [in mathcomp.ssreflect.order]
t:1568 [in mathcomp.ssreflect.order]
T:157 [in mathcomp.ssreflect.generic_quotient]
t:1572 [in mathcomp.ssreflect.order]
t:158 [in mathcomp.ssreflect.tuple]
t:1584 [in mathcomp.ssreflect.order]
T:159 [in mathcomp.ssreflect.generic_quotient]
t:1597 [in mathcomp.ssreflect.seq]
T:16 [in mathcomp.solvable.alt]
t:16 [in mathcomp.field.closed_field]
t:160 [in mathcomp.ssreflect.tuple]
t:160 [in mathcomp.algebra.matrix]
t:1602 [in mathcomp.ssreflect.seq]
t:1607 [in mathcomp.ssreflect.seq]
T:161 [in mathcomp.ssreflect.generic_quotient]
t:161 [in mathcomp.field.algebraics_fundamentals]
t:1616 [in mathcomp.ssreflect.seq]
t:162 [in mathcomp.ssreflect.tuple]
t:162 [in mathcomp.solvable.extremal]
t:1629 [in mathcomp.ssreflect.seq]
t:163 [in mathcomp.algebra.matrix]
t:1639 [in mathcomp.ssreflect.seq]
t:164 [in mathcomp.ssreflect.tuple]
t:164 [in mathcomp.solvable.extremal]
t:1645 [in mathcomp.ssreflect.order]
t:1650 [in mathcomp.algebra.matrix]
t:1658 [in mathcomp.ssreflect.seq]
t:1658 [in mathcomp.algebra.ssralg]
t:166 [in mathcomp.algebra.matrix]
t:1668 [in mathcomp.ssreflect.seq]
t:1668 [in mathcomp.algebra.ssralg]
t:1675 [in mathcomp.algebra.ssralg]
t:1677 [in mathcomp.ssreflect.seq]
t:1677 [in mathcomp.algebra.ssralg]
T:168 [in mathcomp.ssreflect.order]
t:1686 [in mathcomp.ssreflect.seq]
T:169 [in mathcomp.ssreflect.binomial]
t:169 [in mathcomp.fingroup.perm]
t:169 [in mathcomp.solvable.extremal]
T:1692 [in mathcomp.ssreflect.seq]
t:1698 [in mathcomp.ssreflect.seq]
t:1698 [in mathcomp.algebra.ssralg]
T:17 [in mathcomp.ssreflect.generic_quotient]
T:17 [in mathcomp.ssreflect.fintype]
T:17 [in mathcomp.ssreflect.eqtype]
t:170 [in mathcomp.solvable.extremal]
t:170 [in mathcomp.algebra.ssrnum]
t:1704 [in mathcomp.algebra.ssralg]
t:1707 [in mathcomp.algebra.ssralg]
t:1708 [in mathcomp.ssreflect.seq]
T:171 [in mathcomp.ssreflect.tuple]
t:1712 [in mathcomp.ssreflect.seq]
t:1712 [in mathcomp.algebra.ssralg]
T:172 [in mathcomp.ssreflect.order]
t:172 [in mathcomp.solvable.extremal]
t:1722 [in mathcomp.ssreflect.seq]
T:173 [in mathcomp.ssreflect.tuple]
t:1732 [in mathcomp.ssreflect.seq]
t:174 [in mathcomp.ssreflect.binomial]
t:174 [in mathcomp.solvable.extremal]
t:1740 [in mathcomp.ssreflect.seq]
t:175 [in mathcomp.ssreflect.binomial]
T:175 [in mathcomp.ssreflect.tuple]
t:1758 [in mathcomp.ssreflect.seq]
T:177 [in mathcomp.ssreflect.tuple]
t:177 [in mathcomp.solvable.extremal]
t:1771 [in mathcomp.algebra.ssralg]
t:1773 [in mathcomp.algebra.ssralg]
t:1787 [in mathcomp.ssreflect.seq]
T:179 [in mathcomp.ssreflect.tuple]
t:179 [in mathcomp.solvable.extremal]
t:179 [in mathcomp.solvable.burnside_app]
t:1797 [in mathcomp.ssreflect.seq]
t:18 [in mathcomp.ssreflect.tuple]
T:18 [in mathcomp.ssreflect.ssreflect]
T:18 [in mathcomp.ssreflect.eqtype]
t:180 [in mathcomp.solvable.extremal]
t:1805 [in mathcomp.ssreflect.seq]
t:181 [in mathcomp.solvable.extremal]
t:1815 [in mathcomp.ssreflect.seq]
t:182 [in mathcomp.ssreflect.binomial]
t:182 [in mathcomp.solvable.extremal]
T:1822 [in mathcomp.ssreflect.order]
t:1823 [in mathcomp.ssreflect.seq]
t:183 [in mathcomp.solvable.extremal]
T:1831 [in mathcomp.ssreflect.seq]
T:1832 [in mathcomp.ssreflect.order]
t:1838 [in mathcomp.ssreflect.seq]
T:184 [in mathcomp.ssreflect.choice]
t:184 [in mathcomp.solvable.extremal]
t:1848 [in mathcomp.ssreflect.seq]
t:185 [in mathcomp.ssreflect.binomial]
T:185 [in mathcomp.ssreflect.choice]
t:185 [in mathcomp.solvable.extremal]
t:185 [in mathcomp.solvable.burnside_app]
T:1850 [in mathcomp.ssreflect.order]
t:1855 [in mathcomp.ssreflect.seq]
T:186 [in mathcomp.ssreflect.choice]
t:1863 [in mathcomp.ssreflect.seq]
t:187 [in mathcomp.ssreflect.binomial]
t:187 [in mathcomp.solvable.extremal]
t:1879 [in mathcomp.ssreflect.seq]
T:189 [in mathcomp.ssreflect.choice]
T:1892 [in mathcomp.ssreflect.order]
T:19 [in mathcomp.ssreflect.ssreflect]
t:190 [in mathcomp.ssreflect.binomial]
T:190 [in mathcomp.ssreflect.order]
t:191 [in mathcomp.ssreflect.binomial]
T:1917 [in mathcomp.ssreflect.seq]
T:1924 [in mathcomp.ssreflect.order]
T:1925 [in mathcomp.ssreflect.seq]
T:1929 [in mathcomp.ssreflect.seq]
t:193 [in mathcomp.ssreflect.binomial]
t:193 [in mathcomp.solvable.extremal]
T:1935 [in mathcomp.ssreflect.seq]
t:194 [in mathcomp.solvable.extremal]
T:1943 [in mathcomp.ssreflect.seq]
t:195 [in mathcomp.ssreflect.binomial]
t:195 [in mathcomp.ssreflect.tuple]
t:195 [in mathcomp.solvable.extremal]
t:195 [in mathcomp.solvable.burnside_app]
T:1952 [in mathcomp.ssreflect.seq]
t:196 [in mathcomp.ssreflect.binomial]
t:197 [in mathcomp.solvable.extremal]
t:199 [in mathcomp.ssreflect.binomial]
T:2 [in mathcomp.field.fieldext]
T:2 [in mathcomp.algebra.ssrnum]
T:2 [in mathcomp.ssreflect.ssrfun]
T:20 [in mathcomp.ssreflect.ssreflect]
T:20 [in mathcomp.ssreflect.prime]
T:20 [in mathcomp.ssreflect.eqtype]
T:200 [in mathcomp.ssreflect.choice]
t:200 [in mathcomp.solvable.extremal]
T:201 [in mathcomp.ssreflect.choice]
t:201 [in mathcomp.fingroup.gproduct]
T:2019 [in mathcomp.ssreflect.order]
T:202 [in mathcomp.ssreflect.choice]
t:2023 [in mathcomp.ssreflect.seq]
T:2027 [in mathcomp.ssreflect.order]
t:203 [in mathcomp.solvable.extremal]
t:2031 [in mathcomp.ssreflect.seq]
T:2033 [in mathcomp.ssreflect.order]
t:2036 [in mathcomp.ssreflect.seq]
t:2041 [in mathcomp.ssreflect.seq]
t:2044 [in mathcomp.ssreflect.seq]
t:2046 [in mathcomp.ssreflect.seq]
t:205 [in mathcomp.ssreflect.binomial]
T:205 [in mathcomp.ssreflect.order]
t:205 [in mathcomp.solvable.extremal]
t:205 [in mathcomp.solvable.burnside_app]
t:2050 [in mathcomp.ssreflect.seq]
t:2052 [in mathcomp.ssreflect.seq]
t:2059 [in mathcomp.ssreflect.seq]
t:206 [in mathcomp.fingroup.perm]
t:206 [in mathcomp.solvable.extremal]
T:207 [in mathcomp.ssreflect.choice]
T:207 [in mathcomp.ssreflect.order]
t:207 [in mathcomp.solvable.extremal]
t:208 [in mathcomp.solvable.extremal]
t:209 [in mathcomp.fingroup.perm]
T:209 [in mathcomp.ssreflect.choice]
t:209 [in mathcomp.solvable.extremal]
T:21 [in mathcomp.ssreflect.tuple]
t:21 [in mathcomp.solvable.primitive_action]
T:21 [in mathcomp.ssreflect.fintype]
T:2102 [in mathcomp.ssreflect.seq]
t:211 [in mathcomp.ssreflect.binomial]
T:211 [in mathcomp.ssreflect.choice]
t:212 [in mathcomp.ssreflect.binomial]
t:212 [in mathcomp.solvable.extremal]
T:2127 [in mathcomp.algebra.ssralg]
t:215 [in mathcomp.ssreflect.binomial]
t:2157 [in mathcomp.algebra.ssrnum]
t:2158 [in mathcomp.algebra.ssrnum]
t:216 [in mathcomp.fingroup.perm]
t:2164 [in mathcomp.algebra.ssrnum]
t:2165 [in mathcomp.algebra.ssrnum]
t:217 [in mathcomp.ssreflect.binomial]
t:217 [in mathcomp.solvable.extremal]
t:217 [in mathcomp.solvable.burnside_app]
t:2177 [in mathcomp.algebra.ssrnum]
t:2178 [in mathcomp.algebra.ssrnum]
T:2182 [in mathcomp.algebra.ssralg]
T:2187 [in mathcomp.ssreflect.order]
t:219 [in mathcomp.ssreflect.binomial]
T:2192 [in mathcomp.ssreflect.order]
T:2194 [in mathcomp.ssreflect.order]
T:2196 [in mathcomp.ssreflect.order]
T:2197 [in mathcomp.algebra.ssralg]
T:2198 [in mathcomp.ssreflect.order]
t:22 [in mathcomp.fingroup.perm]
t:220 [in mathcomp.ssreflect.binomial]
t:2202 [in mathcomp.algebra.ssrnum]
t:2203 [in mathcomp.algebra.ssrnum]
t:222 [in mathcomp.solvable.extremal]
T:2223 [in mathcomp.algebra.ssralg]
T:224 [in mathcomp.ssreflect.choice]
T:224 [in mathcomp.ssreflect.order]
T:2240 [in mathcomp.ssreflect.order]
T:2242 [in mathcomp.ssreflect.order]
T:2246 [in mathcomp.algebra.ssrnum]
T:225 [in mathcomp.ssreflect.choice]
T:2250 [in mathcomp.algebra.ssrnum]
T:2259 [in mathcomp.ssreflect.order]
T:2261 [in mathcomp.algebra.matrix]
T:2261 [in mathcomp.ssreflect.order]
T:2263 [in mathcomp.ssreflect.order]
T:2265 [in mathcomp.ssreflect.order]
T:2269 [in mathcomp.ssreflect.order]
t:227 [in mathcomp.solvable.extremal]
T:2271 [in mathcomp.ssreflect.order]
T:2273 [in mathcomp.ssreflect.order]
T:2275 [in mathcomp.ssreflect.order]
T:2277 [in mathcomp.ssreflect.order]
T:2279 [in mathcomp.algebra.matrix]
T:2279 [in mathcomp.ssreflect.order]
T:228 [in mathcomp.ssreflect.order]
T:2281 [in mathcomp.ssreflect.order]
T:2283 [in mathcomp.algebra.matrix]
T:2283 [in mathcomp.ssreflect.order]
T:2285 [in mathcomp.ssreflect.order]
T:2287 [in mathcomp.ssreflect.order]
T:2289 [in mathcomp.ssreflect.order]
t:229 [in mathcomp.solvable.extremal]
T:2291 [in mathcomp.ssreflect.order]
T:2293 [in mathcomp.ssreflect.order]
t:2299 [in mathcomp.ssreflect.order]
T:23 [in mathcomp.ssreflect.tuple]
T:23 [in mathcomp.ssreflect.eqtype]
t:230 [in mathcomp.solvable.extremal]
t:2306 [in mathcomp.ssreflect.order]
t:231 [in mathcomp.solvable.extremal]
t:232 [in mathcomp.solvable.extremal]
t:2321 [in mathcomp.ssreflect.order]
t:2322 [in mathcomp.ssreflect.order]
t:2323 [in mathcomp.ssreflect.order]
t:2324 [in mathcomp.ssreflect.order]
t:2325 [in mathcomp.ssreflect.order]
t:2328 [in mathcomp.ssreflect.order]
t:233 [in mathcomp.solvable.extremal]
t:2330 [in mathcomp.ssreflect.order]
t:2331 [in mathcomp.ssreflect.order]
t:2332 [in mathcomp.ssreflect.order]
t:2334 [in mathcomp.ssreflect.order]
t:2335 [in mathcomp.ssreflect.order]
T:2336 [in mathcomp.ssreflect.order]
t:2338 [in mathcomp.ssreflect.order]
T:2339 [in mathcomp.ssreflect.order]
t:234 [in mathcomp.solvable.extremal]
t:2341 [in mathcomp.ssreflect.order]
T:2342 [in mathcomp.ssreflect.order]
t:2344 [in mathcomp.ssreflect.order]
T:2345 [in mathcomp.ssreflect.order]
t:2347 [in mathcomp.ssreflect.order]
T:2349 [in mathcomp.ssreflect.order]
T:2354 [in mathcomp.ssreflect.order]
T:2356 [in mathcomp.ssreflect.order]
T:2358 [in mathcomp.ssreflect.order]
T:2360 [in mathcomp.ssreflect.order]
T:2388 [in mathcomp.ssreflect.order]
T:2390 [in mathcomp.ssreflect.order]
T:2392 [in mathcomp.ssreflect.order]
T:2394 [in mathcomp.ssreflect.order]
T:2397 [in mathcomp.ssreflect.order]
T:2401 [in mathcomp.ssreflect.order]
T:2403 [in mathcomp.ssreflect.order]
T:2405 [in mathcomp.ssreflect.order]
T:2407 [in mathcomp.ssreflect.order]
T:2409 [in mathcomp.ssreflect.order]
T:241 [in mathcomp.ssreflect.order]
T:2411 [in mathcomp.ssreflect.order]
T:2413 [in mathcomp.ssreflect.order]
T:2415 [in mathcomp.ssreflect.order]
T:2417 [in mathcomp.ssreflect.order]
T:2419 [in mathcomp.ssreflect.order]
T:242 [in mathcomp.ssreflect.eqtype]
T:2421 [in mathcomp.ssreflect.order]
T:2423 [in mathcomp.ssreflect.order]
T:2426 [in mathcomp.ssreflect.order]
T:2429 [in mathcomp.ssreflect.order]
T:2430 [in mathcomp.ssreflect.order]
T:2431 [in mathcomp.ssreflect.order]
T:245 [in mathcomp.ssreflect.order]
T:2483 [in mathcomp.ssreflect.order]
T:2484 [in mathcomp.ssreflect.order]
T:2485 [in mathcomp.ssreflect.order]
T:2486 [in mathcomp.ssreflect.order]
T:2487 [in mathcomp.ssreflect.order]
T:2489 [in mathcomp.ssreflect.order]
t:249 [in mathcomp.fingroup.perm]
T:2492 [in mathcomp.ssreflect.order]
T:2493 [in mathcomp.ssreflect.order]
T:2494 [in mathcomp.ssreflect.order]
t:25 [in mathcomp.ssreflect.tuple]
T:25 [in mathcomp.ssreflect.prime]
T:2552 [in mathcomp.ssreflect.order]
T:2554 [in mathcomp.ssreflect.order]
T:2555 [in mathcomp.ssreflect.order]
T:2556 [in mathcomp.ssreflect.order]
T:2557 [in mathcomp.ssreflect.order]
T:2558 [in mathcomp.ssreflect.order]
T:2559 [in mathcomp.ssreflect.order]
T:2562 [in mathcomp.ssreflect.order]
T:2566 [in mathcomp.ssreflect.order]
T:2567 [in mathcomp.ssreflect.order]
T:2568 [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:2580 [in mathcomp.ssreflect.order]
T:259 [in mathcomp.fingroup.action]
T:26 [in mathcomp.ssreflect.finset]
T:260 [in mathcomp.ssreflect.order]
t:2613 [in mathcomp.ssreflect.order]
t:2616 [in mathcomp.ssreflect.order]
T:262 [in mathcomp.ssreflect.choice]
T:2620 [in mathcomp.ssreflect.order]
T:2622 [in mathcomp.ssreflect.order]
T:263 [in mathcomp.ssreflect.choice]
T:264 [in mathcomp.ssreflect.choice]
t:2640 [in mathcomp.ssreflect.order]
t:2641 [in mathcomp.ssreflect.order]
t:2643 [in mathcomp.ssreflect.order]
t:2644 [in mathcomp.ssreflect.order]
T:2647 [in mathcomp.ssreflect.order]
T:2649 [in mathcomp.ssreflect.order]
T:2651 [in mathcomp.ssreflect.order]
T:2653 [in mathcomp.ssreflect.order]
T:2656 [in mathcomp.ssreflect.order]
T:2658 [in mathcomp.ssreflect.order]
T:2660 [in mathcomp.ssreflect.order]
T:2662 [in mathcomp.ssreflect.order]
T:2664 [in mathcomp.ssreflect.order]
T:2666 [in mathcomp.ssreflect.order]
T:2668 [in mathcomp.ssreflect.order]
T:267 [in mathcomp.ssreflect.choice]
T:267 [in mathcomp.ssreflect.order]
T:2670 [in mathcomp.ssreflect.order]
T:2672 [in mathcomp.ssreflect.order]
T:2674 [in mathcomp.ssreflect.order]
T:2676 [in mathcomp.ssreflect.order]
T:2678 [in mathcomp.ssreflect.order]
T:2680 [in mathcomp.ssreflect.order]
T:2683 [in mathcomp.ssreflect.order]
T:2687 [in mathcomp.ssreflect.order]
T:2688 [in mathcomp.ssreflect.order]
T:2689 [in mathcomp.ssreflect.order]
T:2690 [in mathcomp.ssreflect.order]
T:2692 [in mathcomp.ssreflect.order]
T:2694 [in mathcomp.ssreflect.order]
T:2696 [in mathcomp.ssreflect.order]
T:27 [in mathcomp.ssreflect.ssrbool]
T:270 [in mathcomp.ssreflect.choice]
T:2702 [in mathcomp.ssreflect.order]
T:2708 [in mathcomp.ssreflect.order]
t:2718 [in mathcomp.ssreflect.order]
t:2721 [in mathcomp.ssreflect.order]
T:2723 [in mathcomp.ssreflect.order]
T:2725 [in mathcomp.ssreflect.order]
T:2727 [in mathcomp.ssreflect.order]
T:2729 [in mathcomp.ssreflect.order]
t:273 [in mathcomp.solvable.extremal]
T:2732 [in mathcomp.ssreflect.order]
T:2735 [in mathcomp.ssreflect.order]
T:2737 [in mathcomp.ssreflect.order]
T:2739 [in mathcomp.ssreflect.order]
t:274 [in mathcomp.field.algebraics_fundamentals]
T:2741 [in mathcomp.ssreflect.order]
T:2743 [in mathcomp.ssreflect.order]
T:2745 [in mathcomp.ssreflect.order]
T:2747 [in mathcomp.ssreflect.order]
T:2749 [in mathcomp.ssreflect.order]
T:2751 [in mathcomp.ssreflect.order]
T:2753 [in mathcomp.ssreflect.order]
T:2755 [in mathcomp.ssreflect.order]
T:2757 [in mathcomp.ssreflect.order]
T:2761 [in mathcomp.ssreflect.order]
T:28 [in mathcomp.ssreflect.eqtype]
T:281 [in mathcomp.ssreflect.choice]
T:282 [in mathcomp.ssreflect.choice]
T:285 [in mathcomp.ssreflect.order]
T:288 [in mathcomp.ssreflect.order]
t:2886 [in mathcomp.algebra.ssrnum]
t:2890 [in mathcomp.algebra.ssrnum]
t:2894 [in mathcomp.algebra.ssrnum]
t:2898 [in mathcomp.algebra.ssrnum]
T:29 [in mathcomp.algebra.interval]
t:29 [in mathcomp.solvable.primitive_action]
T:29 [in mathcomp.field.closed_field]
T:293 [in mathcomp.ssreflect.order]
t:294 [in mathcomp.fingroup.perm]
t:297 [in mathcomp.field.closed_field]
T:298 [in mathcomp.ssreflect.order]
T:3 [in mathcomp.ssreflect.order]
T:3 [in mathcomp.ssreflect.ssrbool]
T:30 [in mathcomp.algebra.interval]
t:30 [in mathcomp.solvable.primitive_action]
T:30 [in mathcomp.algebra.ssrnum]
t:302 [in mathcomp.field.closed_field]
t:306 [in mathcomp.field.closed_field]
T:308 [in mathcomp.ssreflect.eqtype]
T:31 [in mathcomp.algebra.interval]
t:31 [in mathcomp.ssreflect.tuple]
t:31 [in mathcomp.ssreflect.choice]
T:31 [in mathcomp.fingroup.fingroup]
T:31 [in mathcomp.ssreflect.prime]
T:316 [in mathcomp.ssreflect.order]
T:318 [in mathcomp.ssreflect.eqtype]
T:319 [in mathcomp.ssreflect.order]
t:32 [in mathcomp.fingroup.perm]
T:32 [in mathcomp.algebra.interval]
t:32 [in mathcomp.solvable.primitive_action]
T:320 [in mathcomp.ssreflect.order]
T:321 [in mathcomp.ssreflect.eqtype]
T:33 [in mathcomp.algebra.interval]
t:33 [in mathcomp.solvable.extremal]
t:330 [in mathcomp.field.closed_field]
T:331 [in mathcomp.ssreflect.eqtype]
t:335 [in mathcomp.field.closed_field]
T:337 [in mathcomp.ssreflect.order]
T:339 [in mathcomp.ssreflect.eqtype]
T:34 [in mathcomp.ssreflect.generic_quotient]
T:34 [in mathcomp.algebra.interval]
T:341 [in mathcomp.ssreflect.order]
t:35 [in mathcomp.fingroup.perm]
t:35 [in mathcomp.ssreflect.choice]
T:35 [in mathcomp.field.closed_field]
T:35 [in mathcomp.fingroup.fingroup]
T:354 [in mathcomp.ssreflect.order]
T:356 [in mathcomp.ssreflect.eqtype]
T:358 [in mathcomp.ssreflect.order]
T:36 [in mathcomp.algebra.ssrnum]
T:365 [in mathcomp.ssreflect.ssrnat]
t:366 [in mathcomp.character.inertia]
t:37 [in mathcomp.ssreflect.tuple]
T:371 [in mathcomp.ssreflect.order]
t:374 [in mathcomp.ssreflect.seq]
T:375 [in mathcomp.ssreflect.order]
t:377 [in mathcomp.ssreflect.seq]
T:38 [in mathcomp.ssreflect.generic_quotient]
t:380 [in mathcomp.ssreflect.seq]
t:385 [in mathcomp.ssreflect.seq]
T:388 [in mathcomp.ssreflect.order]
T:39 [in mathcomp.ssreflect.fintype]
T:392 [in mathcomp.ssreflect.order]
t:398 [in mathcomp.character.inertia]
T:4 [in mathcomp.algebra.interval]
t:40 [in mathcomp.fingroup.perm]
t:40 [in mathcomp.solvable.primitive_action]
T:40 [in mathcomp.field.closed_field]
T:40 [in mathcomp.fingroup.fingroup]
T:405 [in mathcomp.ssreflect.seq]
T:405 [in mathcomp.ssreflect.order]
t:406 [in mathcomp.fingroup.gproduct]
t:408 [in mathcomp.ssreflect.seq]
T:409 [in mathcomp.fingroup.action]
T:409 [in mathcomp.ssreflect.order]
T:41 [in mathcomp.ssreflect.generic_quotient]
t:41 [in mathcomp.ssreflect.tuple]
t:41 [in mathcomp.solvable.primitive_action]
T:41 [in mathcomp.ssreflect.fintype]
t:412 [in mathcomp.ssreflect.seq]
T:422 [in mathcomp.ssreflect.order]
t:425 [in mathcomp.ssreflect.path]
T:429 [in mathcomp.ssreflect.fintype]
t:43 [in mathcomp.ssreflect.choice]
T:43 [in mathcomp.ssreflect.fintype]
T:437 [in mathcomp.ssreflect.fintype]
t:45 [in mathcomp.solvable.primitive_action]
t:451 [in mathcomp.character.inertia]
T:451 [in mathcomp.ssreflect.order]
t:466 [in mathcomp.character.character]
T:468 [in mathcomp.ssreflect.path]
t:47 [in mathcomp.ssreflect.choice]
T:47 [in mathcomp.ssreflect.fintype]
t:470 [in mathcomp.ssreflect.seq]
T:472 [in mathcomp.ssreflect.path]
t:474 [in mathcomp.ssreflect.seq]
t:477 [in mathcomp.character.character]
T:479 [in mathcomp.ssreflect.path]
t:48 [in mathcomp.solvable.primitive_action]
T:483 [in mathcomp.ssreflect.path]
t:483 [in mathcomp.character.character]
T:49 [in mathcomp.fingroup.fingroup]
t:5 [in mathcomp.ssreflect.tuple]
T:5 [in mathcomp.ssreflect.ssreflect]
T:5 [in mathcomp.algebra.finalg]
T:5 [in mathcomp.ssreflect.ssrbool]
T:5 [in mathcomp.ssreflect.ssrfun]
t:5 [in mathcomp.fingroup.presentation]
T:5 [in mathcomp.ssreflect.eqtype]
T:50 [in mathcomp.field.closed_field]
t:508 [in mathcomp.algebra.ssrnum]
t:51 [in mathcomp.ssreflect.choice]
t:51 [in mathcomp.field.separable]
t:512 [in mathcomp.algebra.ssrnum]
T:516 [in mathcomp.ssreflect.path]
t:516 [in mathcomp.algebra.ssrnum]
t:52 [in mathcomp.solvable.primitive_action]
T:52 [in mathcomp.fingroup.fingroup]
t:520 [in mathcomp.algebra.ssrnum]
t:520 [in mathcomp.ssreflect.bigop]
T:522 [in mathcomp.ssreflect.path]
t:524 [in mathcomp.algebra.ssrnum]
T:528 [in mathcomp.ssreflect.path]
t:528 [in mathcomp.algebra.ssrnum]
T:53 [in mathcomp.solvable.alt]
t:53 [in mathcomp.ssreflect.tuple]
t:53 [in mathcomp.field.closed_field]
t:53 [in mathcomp.solvable.burnside_app]
t:532 [in mathcomp.algebra.ssrnum]
T:535 [in mathcomp.ssreflect.path]
t:536 [in mathcomp.algebra.ssrnum]
T:54 [in mathcomp.algebra.ssrnum]
T:542 [in mathcomp.ssreflect.ssrnat]
t:547 [in mathcomp.ssreflect.bigop]
t:55 [in mathcomp.ssreflect.tuple]
t:55 [in mathcomp.solvable.primitive_action]
t:567 [in mathcomp.ssreflect.path]
t:569 [in mathcomp.ssreflect.path]
T:57 [in mathcomp.ssreflect.bigop]
t:571 [in mathcomp.ssreflect.path]
t:578 [in mathcomp.ssreflect.path]
T:58 [in mathcomp.ssreflect.choice]
t:580 [in mathcomp.ssreflect.path]
T:585 [in mathcomp.algebra.ssralg]
T:59 [in mathcomp.ssreflect.choice]
T:599 [in mathcomp.ssreflect.fintype]
T:6 [in mathcomp.solvable.alt]
t:6 [in mathcomp.ssreflect.tuple]
T:6 [in mathcomp.algebra.countalg]
T:6 [in mathcomp.ssreflect.finset]
T:6 [in mathcomp.ssreflect.ssreflect]
T:6 [in mathcomp.ssreflect.ssrbool]
T:6 [in mathcomp.algebra.ssralg]
T:60 [in mathcomp.ssreflect.choice]
T:60 [in mathcomp.ssreflect.fintype]
t:603 [in mathcomp.ssreflect.seq]
T:605 [in mathcomp.ssreflect.ssrnat]
T:608 [in mathcomp.ssreflect.fintype]
t:61 [in mathcomp.fingroup.perm]
T:61 [in mathcomp.ssreflect.fintype]
T:615 [in mathcomp.ssreflect.fintype]
t:62 [in mathcomp.ssreflect.tuple]
T:626 [in mathcomp.ssreflect.fintype]
t:64 [in mathcomp.ssreflect.tuple]
T:64 [in mathcomp.ssreflect.prime]
T:65 [in mathcomp.ssreflect.fintype]
t:66 [in mathcomp.ssreflect.ssrAC]
t:67 [in mathcomp.solvable.extremal]
t:68 [in mathcomp.ssreflect.tuple]
t:68 [in mathcomp.solvable.extremal]
T:683 [in mathcomp.ssreflect.path]
t:687 [in mathcomp.ssreflect.order]
t:69 [in mathcomp.ssreflect.tuple]
T:69 [in mathcomp.ssreflect.ssrAC]
t:691 [in mathcomp.ssreflect.order]
T:7 [in mathcomp.solvable.alt]
t:7 [in mathcomp.ssreflect.tuple]
T:7 [in mathcomp.field.algebraics_fundamentals]
T:701 [in mathcomp.ssreflect.seq]
T:703 [in mathcomp.ssreflect.seq]
t:71 [in mathcomp.ssreflect.tuple]
T:71 [in mathcomp.ssreflect.choice]
T:72 [in mathcomp.algebra.ssrnum]
T:722 [in mathcomp.ssreflect.seq]
T:722 [in mathcomp.ssreflect.path]
T:727 [in mathcomp.ssreflect.seq]
T:727 [in mathcomp.ssreflect.path]
t:73 [in mathcomp.ssreflect.tuple]
T:732 [in mathcomp.ssreflect.path]
T:737 [in mathcomp.ssreflect.path]
t:74 [in mathcomp.ssreflect.tuple]
T:74 [in mathcomp.solvable.sylow]
t:76 [in mathcomp.ssreflect.tuple]
T:766 [in mathcomp.ssreflect.finset]
T:770 [in mathcomp.ssreflect.finset]
T:773 [in mathcomp.ssreflect.finset]
T:778 [in mathcomp.ssreflect.finset]
t:78 [in mathcomp.ssreflect.tuple]
T:78 [in mathcomp.ssreflect.ssrAC]
t:79 [in mathcomp.ssreflect.tuple]
T:8 [in mathcomp.solvable.alt]
T:8 [in mathcomp.fingroup.perm]
T:8 [in mathcomp.algebra.countalg]
T:8 [in mathcomp.ssreflect.finset]
T:8 [in mathcomp.algebra.finalg]
T:8 [in mathcomp.field.falgebra]
t:80 [in mathcomp.ssreflect.tuple]
t:801 [in mathcomp.ssreflect.seq]
t:81 [in mathcomp.ssreflect.tuple]
T:81 [in mathcomp.ssreflect.bigop]
t:82 [in mathcomp.ssreflect.tuple]
T:82 [in mathcomp.ssreflect.bigop]
t:83 [in mathcomp.ssreflect.tuple]
t:835 [in mathcomp.ssreflect.seq]
t:84 [in mathcomp.ssreflect.tuple]
T:84 [in mathcomp.ssreflect.choice]
T:84 [in mathcomp.ssreflect.order]
T:84 [in mathcomp.ssreflect.bigop]
t:85 [in mathcomp.ssreflect.tuple]
t:855 [in mathcomp.ssreflect.order]
T:856 [in mathcomp.algebra.matrix]
t:859 [in mathcomp.ssreflect.order]
t:86 [in mathcomp.ssreflect.tuple]
T:86 [in mathcomp.ssreflect.bigop]
t:863 [in mathcomp.ssreflect.order]
t:867 [in mathcomp.ssreflect.order]
t:87 [in mathcomp.ssreflect.tuple]
T:870 [in mathcomp.ssreflect.order]
t:89 [in mathcomp.ssreflect.tuple]
T:9 [in mathcomp.ssreflect.order]
T:9 [in mathcomp.ssreflect.ssrbool]
T:90 [in mathcomp.ssreflect.finfun]
t:91 [in mathcomp.ssreflect.tuple]
t:912 [in mathcomp.character.mxrepresentation]
t:94 [in mathcomp.ssreflect.tuple]
t:94 [in mathcomp.ssreflect.finfun]
T:94 [in mathcomp.ssreflect.ssrAC]
T:94 [in mathcomp.ssreflect.order]
t:97 [in mathcomp.ssreflect.tuple]
T:991 [in mathcomp.ssreflect.order]
T:992 [in mathcomp.ssreflect.order]
T:993 [in mathcomp.ssreflect.order]
T:994 [in mathcomp.ssreflect.order]
| 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 | (69505 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 | (1943 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 | (39748 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 | (379 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 | (3958 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 | (13542 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 | (480 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (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 | (452 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 | (1344 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 | (1014 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 | (6127 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 | (248 entries) |