| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74637 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1852 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48381 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (277 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3804 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (91 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14415 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (132 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1342 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1003 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3033 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
T (binder)
tauS:264 [in mathcomp.character.vcharacter]tauS:575 [in mathcomp.character.classfun]
tau:167 [in mathcomp.character.classfun]
tau:171 [in mathcomp.character.classfun]
tau:265 [in mathcomp.character.vcharacter]
tau:266 [in mathcomp.character.vcharacter]
tau:268 [in mathcomp.character.vcharacter]
tau:269 [in mathcomp.character.vcharacter]
tau:569 [in mathcomp.character.classfun]
tau:572 [in mathcomp.character.classfun]
tau:573 [in mathcomp.character.classfun]
tau:576 [in mathcomp.character.classfun]
tau:577 [in mathcomp.character.classfun]
tau:579 [in mathcomp.character.classfun]
theta:440 [in mathcomp.character.inertia]
theta:488 [in mathcomp.character.inertia]
theta:499 [in mathcomp.character.inertia]
theta:541 [in mathcomp.character.inertia]
toL:368 [in mathcomp.field.fieldext]
toL:369 [in mathcomp.field.fieldext]
toPF:367 [in mathcomp.field.fieldext]
top:222 [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:219 [in mathcomp.fingroup.perm]
ts:223 [in mathcomp.fingroup.perm]
ts:228 [in mathcomp.fingroup.perm]
ts:326 [in mathcomp.field.closed_field]
Tx:142 [in mathcomp.character.inertia]
Tx:143 [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':112 [in mathcomp.fingroup.perm]
T':1280 [in mathcomp.ssreflect.finset]
T':150 [in mathcomp.ssreflect.fingraph]
T':155 [in mathcomp.ssreflect.generic_quotient]
t':1644 [in mathcomp.algebra.ssralg]
T':2036 [in mathcomp.ssreflect.order]
T':214 [in mathcomp.ssreflect.tuple]
T':2467 [in mathcomp.ssreflect.seq]
T':2552 [in mathcomp.ssreflect.seq]
T':2702 [in mathcomp.ssreflect.order]
T':2733 [in mathcomp.ssreflect.order]
T':2740 [in mathcomp.ssreflect.order]
T':2756 [in mathcomp.ssreflect.order]
T':2785 [in mathcomp.ssreflect.order]
T':2804 [in mathcomp.ssreflect.order]
T':2813 [in mathcomp.ssreflect.order]
T':2824 [in mathcomp.ssreflect.order]
T':2852 [in mathcomp.ssreflect.order]
T':2861 [in mathcomp.ssreflect.order]
T':2870 [in mathcomp.ssreflect.order]
T':2881 [in mathcomp.ssreflect.order]
T':2892 [in mathcomp.ssreflect.order]
T':2899 [in mathcomp.ssreflect.order]
T':2906 [in mathcomp.ssreflect.order]
T':2913 [in mathcomp.ssreflect.order]
T':2925 [in mathcomp.ssreflect.order]
T':2959 [in mathcomp.ssreflect.order]
T':2970 [in mathcomp.ssreflect.order]
T':2981 [in mathcomp.ssreflect.order]
T':2988 [in mathcomp.ssreflect.order]
T':2995 [in mathcomp.ssreflect.order]
T':4001 [in mathcomp.ssreflect.order]
T':4006 [in mathcomp.ssreflect.order]
T':4008 [in mathcomp.ssreflect.order]
T':4010 [in mathcomp.ssreflect.order]
T':4012 [in mathcomp.ssreflect.order]
T':4054 [in mathcomp.ssreflect.order]
T':4056 [in mathcomp.ssreflect.order]
T':4073 [in mathcomp.ssreflect.order]
T':4075 [in mathcomp.ssreflect.order]
T':4077 [in mathcomp.ssreflect.order]
T':4079 [in mathcomp.ssreflect.order]
T':4083 [in mathcomp.ssreflect.order]
T':4085 [in mathcomp.ssreflect.order]
T':4087 [in mathcomp.ssreflect.order]
T':4089 [in mathcomp.ssreflect.order]
T':4091 [in mathcomp.ssreflect.order]
T':4093 [in mathcomp.ssreflect.order]
T':4095 [in mathcomp.ssreflect.order]
T':4097 [in mathcomp.ssreflect.order]
T':4099 [in mathcomp.ssreflect.order]
T':4101 [in mathcomp.ssreflect.order]
T':4103 [in mathcomp.ssreflect.order]
T':4105 [in mathcomp.ssreflect.order]
T':4107 [in mathcomp.ssreflect.order]
T':4133 [in mathcomp.ssreflect.order]
T':4150 [in mathcomp.ssreflect.order]
T':4155 [in mathcomp.ssreflect.order]
T':4157 [in mathcomp.ssreflect.order]
T':4159 [in mathcomp.ssreflect.order]
T':4161 [in mathcomp.ssreflect.order]
T':4183 [in mathcomp.ssreflect.order]
T':4192 [in mathcomp.ssreflect.order]
T':4196 [in mathcomp.ssreflect.order]
T':4198 [in mathcomp.ssreflect.order]
T':4200 [in mathcomp.ssreflect.order]
T':4611 [in mathcomp.ssreflect.order]
T':4621 [in mathcomp.ssreflect.order]
T':544 [in mathcomp.ssreflect.fintype]
T':559 [in mathcomp.ssreflect.fintype]
T':646 [in mathcomp.ssreflect.fintype]
T':667 [in mathcomp.ssreflect.path]
T':677 [in mathcomp.ssreflect.path]
t':78 [in mathcomp.solvable.primitive_action]
t':79 [in mathcomp.solvable.primitive_action]
T':790 [in mathcomp.ssreflect.path]
T':885 [in mathcomp.ssreflect.fintype]
T':890 [in mathcomp.ssreflect.fintype]
T':96 [in mathcomp.ssreflect.generic_quotient]
T':996 [in mathcomp.ssreflect.order]
t1:110 [in mathcomp.solvable.burnside_app]
T1:1254 [in mathcomp.algebra.mxalgebra]
T1:1291 [in mathcomp.ssreflect.seq]
t1:13 [in mathcomp.ssreflect.tuple]
t1:1580 [in mathcomp.ssreflect.seq]
t1:1624 [in mathcomp.algebra.ssralg]
t1:167 [in mathcomp.ssreflect.tuple]
T1:171 [in mathcomp.ssreflect.choice]
T1:173 [in mathcomp.ssreflect.choice]
T1:1969 [in mathcomp.ssreflect.order]
t1:2023 [in mathcomp.ssreflect.seq]
t1:2162 [in mathcomp.ssreflect.seq]
t1:2176 [in mathcomp.ssreflect.seq]
t1:2212 [in mathcomp.ssreflect.seq]
t1:2348 [in mathcomp.ssreflect.seq]
t1:2361 [in mathcomp.ssreflect.seq]
T1:243 [in mathcomp.ssreflect.choice]
T1:245 [in mathcomp.ssreflect.choice]
T1:398 [in mathcomp.ssreflect.eqtype]
T1:4 [in mathcomp.field.closed_field]
T1:43 [in mathcomp.field.closed_field]
t1:4348 [in mathcomp.ssreflect.order]
t1:4355 [in mathcomp.ssreflect.order]
t1:4365 [in mathcomp.ssreflect.order]
t1:4369 [in mathcomp.ssreflect.order]
t1:4373 [in mathcomp.ssreflect.order]
t1:4376 [in mathcomp.ssreflect.order]
t1:4380 [in mathcomp.ssreflect.order]
t1:4383 [in mathcomp.ssreflect.order]
t1:4385 [in mathcomp.ssreflect.order]
t1:4389 [in mathcomp.ssreflect.order]
t1:4407 [in mathcomp.ssreflect.order]
t1:4411 [in mathcomp.ssreflect.order]
t1:4414 [in mathcomp.ssreflect.order]
t1:4416 [in mathcomp.ssreflect.order]
t1:4418 [in mathcomp.ssreflect.order]
t1:4482 [in mathcomp.ssreflect.order]
t1:4488 [in mathcomp.ssreflect.order]
t1:4494 [in mathcomp.ssreflect.order]
T1:7 [in mathcomp.field.closed_field]
t1:847 [in mathcomp.ssreflect.seq]
t1:860 [in mathcomp.ssreflect.seq]
T1:889 [in mathcomp.ssreflect.order]
t2:111 [in mathcomp.solvable.burnside_app]
T2:1255 [in mathcomp.algebra.mxalgebra]
T2:1292 [in mathcomp.ssreflect.seq]
t2:14 [in mathcomp.ssreflect.tuple]
t2:1581 [in mathcomp.ssreflect.seq]
t2:168 [in mathcomp.ssreflect.tuple]
T2:172 [in mathcomp.ssreflect.choice]
T2:174 [in mathcomp.ssreflect.choice]
T2:1970 [in mathcomp.ssreflect.order]
t2:2024 [in mathcomp.ssreflect.seq]
t2:2164 [in mathcomp.ssreflect.seq]
t2:2178 [in mathcomp.ssreflect.seq]
t2:2213 [in mathcomp.ssreflect.seq]
t2:2350 [in mathcomp.ssreflect.seq]
t2:2363 [in mathcomp.ssreflect.seq]
T2:244 [in mathcomp.ssreflect.choice]
T2:246 [in mathcomp.ssreflect.choice]
T2:399 [in mathcomp.ssreflect.eqtype]
t2:4349 [in mathcomp.ssreflect.order]
t2:4356 [in mathcomp.ssreflect.order]
t2:4366 [in mathcomp.ssreflect.order]
t2:4370 [in mathcomp.ssreflect.order]
t2:4374 [in mathcomp.ssreflect.order]
t2:4377 [in mathcomp.ssreflect.order]
t2:4379 [in mathcomp.ssreflect.order]
t2:4384 [in mathcomp.ssreflect.order]
t2:4386 [in mathcomp.ssreflect.order]
t2:4390 [in mathcomp.ssreflect.order]
t2:4408 [in mathcomp.ssreflect.order]
t2:4412 [in mathcomp.ssreflect.order]
t2:4415 [in mathcomp.ssreflect.order]
t2:4417 [in mathcomp.ssreflect.order]
t2:4419 [in mathcomp.ssreflect.order]
t2:4483 [in mathcomp.ssreflect.order]
t2:4489 [in mathcomp.ssreflect.order]
t2:4495 [in mathcomp.ssreflect.order]
T2:45 [in mathcomp.field.closed_field]
T2:8 [in mathcomp.field.closed_field]
t2:848 [in mathcomp.ssreflect.seq]
t2:861 [in mathcomp.ssreflect.seq]
T2:890 [in mathcomp.ssreflect.order]
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:1025 [in mathcomp.character.mxrepresentation]
T:103 [in mathcomp.ssreflect.ssrbool]
t:104 [in mathcomp.ssreflect.tuple]
t:107 [in mathcomp.ssreflect.tuple]
t:108 [in mathcomp.ssreflect.tuple]
t:108 [in mathcomp.field.closed_field]
T:108 [in mathcomp.ssreflect.ssrbool]
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:110 [in mathcomp.ssreflect.finfun]
T:111 [in mathcomp.fingroup.perm]
T:111 [in mathcomp.ssreflect.generic_quotient]
T:1112 [in mathcomp.ssreflect.order]
T:1113 [in mathcomp.ssreflect.order]
T:1114 [in mathcomp.ssreflect.order]
T:1115 [in mathcomp.ssreflect.order]
t:113 [in mathcomp.ssreflect.tuple]
T:113 [in mathcomp.algebra.ring_quotient]
T:113 [in mathcomp.ssreflect.ssrbool]
T:1130 [in mathcomp.ssreflect.order]
T:116 [in mathcomp.ssreflect.generic_quotient]
t:116 [in mathcomp.ssreflect.tuple]
T:117 [in mathcomp.fingroup.perm]
T:118 [in mathcomp.ssreflect.ssrbool]
T:118 [in mathcomp.ssreflect.eqtype]
T:119 [in mathcomp.ssreflect.generic_quotient]
t:119 [in mathcomp.ssreflect.tuple]
t:12 [in mathcomp.ssreflect.tuple]
T:12 [in mathcomp.ssreflect.fintype]
T:1202 [in mathcomp.ssreflect.seq]
T:1205 [in mathcomp.ssreflect.seq]
T:1209 [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:1210 [in mathcomp.ssreflect.order]
T:123 [in mathcomp.ssreflect.ssrbool]
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:1257 [in mathcomp.ssreflect.order]
t:126 [in mathcomp.ssreflect.tuple]
T:126 [in mathcomp.ssreflect.eqtype]
t:1267 [in mathcomp.ssreflect.seq]
t:1268 [in mathcomp.ssreflect.seq]
T:1269 [in mathcomp.ssreflect.order]
t:127 [in mathcomp.solvable.extremal]
t:1277 [in mathcomp.ssreflect.seq]
T:129 [in mathcomp.fingroup.perm]
t:129 [in mathcomp.ssreflect.tuple]
t:1290 [in mathcomp.ssreflect.seq]
T:1293 [in mathcomp.algebra.mxalgebra]
t:13 [in mathcomp.fingroup.presentation]
T:13 [in mathcomp.ssreflect.eqtype]
T:1315 [in mathcomp.ssreflect.seq]
T:1319 [in mathcomp.ssreflect.seq]
T:132 [in mathcomp.fingroup.perm]
t:1325 [in mathcomp.ssreflect.order]
t:1329 [in mathcomp.ssreflect.order]
t:133 [in mathcomp.ssreflect.tuple]
t:1333 [in mathcomp.ssreflect.order]
t:1335 [in mathcomp.ssreflect.seq]
t:1337 [in mathcomp.ssreflect.order]
T:135 [in mathcomp.fingroup.perm]
t:1359 [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:141 [in mathcomp.ssreflect.tuple]
T:141 [in mathcomp.ssreflect.bigop]
t:142 [in mathcomp.ssreflect.tuple]
T:142 [in mathcomp.ssreflect.bigop]
T:144 [in mathcomp.ssreflect.order]
T:144 [in mathcomp.ssreflect.bigop]
t:1440 [in mathcomp.ssreflect.seq]
T:145 [in mathcomp.ssreflect.tuple]
t:146 [in mathcomp.ssreflect.tuple]
T:146 [in mathcomp.ssreflect.bigop]
t:147 [in mathcomp.algebra.matrix]
T:1472 [in mathcomp.ssreflect.seq]
T:148 [in mathcomp.ssreflect.order]
t:15 [in mathcomp.fingroup.perm]
t:15 [in mathcomp.ssreflect.tuple]
T:15 [in mathcomp.ssreflect.bigop]
t:150 [in mathcomp.ssreflect.tuple]
t:150 [in mathcomp.algebra.matrix]
T:1524 [in mathcomp.ssreflect.finset]
t:153 [in mathcomp.algebra.matrix]
T:153 [in mathcomp.ssreflect.fintype]
T:1530 [in mathcomp.ssreflect.finset]
t:155 [in mathcomp.ssreflect.tuple]
t:1558 [in mathcomp.ssreflect.seq]
T:156 [in mathcomp.field.galois]
T:156 [in mathcomp.ssreflect.fintype]
t:1563 [in mathcomp.ssreflect.seq]
t:1567 [in mathcomp.algebra.ssralg]
t:1569 [in mathcomp.ssreflect.seq]
t:1571 [in mathcomp.ssreflect.seq]
t:1573 [in mathcomp.ssreflect.seq]
t:1575 [in mathcomp.ssreflect.seq]
t:1577 [in mathcomp.ssreflect.seq]
t:1577 [in mathcomp.algebra.ssralg]
t:1584 [in mathcomp.algebra.ssralg]
t:1585 [in mathcomp.ssreflect.seq]
t:1586 [in mathcomp.algebra.ssralg]
t:1589 [in mathcomp.ssreflect.seq]
T:159 [in mathcomp.ssreflect.fintype]
t:1592 [in mathcomp.ssreflect.seq]
t:1596 [in mathcomp.ssreflect.seq]
t:1598 [in mathcomp.ssreflect.seq]
T:16 [in mathcomp.solvable.alt]
t:16 [in mathcomp.field.closed_field]
t:160 [in mathcomp.ssreflect.tuple]
T:1606 [in mathcomp.ssreflect.seq]
t:1606 [in mathcomp.character.mxrepresentation]
t:1607 [in mathcomp.algebra.ssralg]
t:1608 [in mathcomp.ssreflect.seq]
T:1610 [in mathcomp.ssreflect.seq]
t:1613 [in mathcomp.algebra.ssralg]
t:1616 [in mathcomp.algebra.ssralg]
t:1618 [in mathcomp.character.mxrepresentation]
t:1621 [in mathcomp.algebra.ssralg]
t:163 [in mathcomp.ssreflect.tuple]
T:166 [in mathcomp.ssreflect.order]
t:1682 [in mathcomp.algebra.ssralg]
t:1684 [in mathcomp.algebra.ssralg]
T:1695 [in mathcomp.ssreflect.seq]
T:1699 [in mathcomp.ssreflect.seq]
T:17 [in mathcomp.ssreflect.eqtype]
T:170 [in mathcomp.ssreflect.choice]
T:1705 [in mathcomp.ssreflect.seq]
T:1708 [in mathcomp.ssreflect.seq]
T:172 [in mathcomp.ssreflect.binomial]
t:172 [in mathcomp.ssreflect.tuple]
T:173 [in mathcomp.ssreflect.order]
t:1733 [in mathcomp.algebra.matrix]
t:174 [in mathcomp.ssreflect.tuple]
t:174 [in mathcomp.field.algebraics_fundamentals]
t:175 [in mathcomp.ssreflect.binomial]
t:175 [in mathcomp.fingroup.perm]
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:177 [in mathcomp.ssreflect.binomial]
T:177 [in mathcomp.ssreflect.order]
t:177 [in mathcomp.solvable.extremal]
t:178 [in mathcomp.ssreflect.binomial]
t:178 [in mathcomp.ssreflect.tuple]
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:18 [in mathcomp.ssreflect.ssrbool]
t:180 [in mathcomp.fingroup.perm]
T:181 [in mathcomp.ssreflect.binomial]
T:181 [in mathcomp.ssreflect.choice]
t:181 [in mathcomp.solvable.burnside_app]
t:184 [in mathcomp.ssreflect.tuple]
t:184 [in mathcomp.solvable.extremal]
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:1918 [in mathcomp.algebra.ssralg]
t:192 [in mathcomp.solvable.extremal]
T:193 [in mathcomp.ssreflect.choice]
t:194 [in mathcomp.solvable.extremal]
t:1948 [in mathcomp.ssreflect.seq]
t:195 [in mathcomp.solvable.extremal]
t:1955 [in mathcomp.ssreflect.seq]
t:196 [in mathcomp.solvable.extremal]
t:1963 [in mathcomp.ssreflect.seq]
t:197 [in mathcomp.solvable.extremal]
t:197 [in mathcomp.solvable.burnside_app]
t:1973 [in mathcomp.ssreflect.order]
t:1976 [in mathcomp.ssreflect.seq]
t:1976 [in mathcomp.ssreflect.order]
t:1979 [in mathcomp.ssreflect.order]
T:198 [in mathcomp.ssreflect.choice]
t:198 [in mathcomp.solvable.extremal]
t:1982 [in mathcomp.ssreflect.order]
t:1985 [in mathcomp.ssreflect.order]
t:1988 [in mathcomp.ssreflect.order]
t:199 [in mathcomp.solvable.extremal]
t:1991 [in mathcomp.ssreflect.order]
t:1994 [in mathcomp.ssreflect.order]
t:1995 [in mathcomp.ssreflect.seq]
t:1997 [in mathcomp.ssreflect.order]
T:2 [in mathcomp.field.fieldext]
T:2 [in mathcomp.ssreflect.order]
T:20 [in mathcomp.ssreflect.prime]
t:200 [in mathcomp.solvable.extremal]
t:2000 [in mathcomp.ssreflect.order]
t:2004 [in mathcomp.ssreflect.order]
t:2008 [in mathcomp.ssreflect.order]
t:201 [in mathcomp.fingroup.gproduct]
t:2010 [in mathcomp.ssreflect.seq]
t:2012 [in mathcomp.ssreflect.order]
t:2016 [in mathcomp.ssreflect.order]
t:202 [in mathcomp.solvable.extremal]
t:2020 [in mathcomp.ssreflect.order]
t:2024 [in mathcomp.ssreflect.order]
t:2028 [in mathcomp.ssreflect.order]
t:2032 [in mathcomp.ssreflect.order]
T:2035 [in mathcomp.ssreflect.order]
t:2037 [in mathcomp.ssreflect.seq]
t:204 [in mathcomp.ssreflect.tuple]
t:2053 [in mathcomp.ssreflect.seq]
T:2059 [in mathcomp.algebra.ssralg]
t:2067 [in mathcomp.ssreflect.seq]
t:207 [in mathcomp.solvable.burnside_app]
t:208 [in mathcomp.solvable.extremal]
t:2080 [in mathcomp.ssreflect.seq]
T:2083 [in mathcomp.ssreflect.order]
t:209 [in mathcomp.solvable.extremal]
T:2090 [in mathcomp.ssreflect.seq]
T:2091 [in mathcomp.ssreflect.order]
t:2096 [in mathcomp.ssreflect.seq]
T:21 [in mathcomp.ssreflect.tuple]
t:210 [in mathcomp.solvable.extremal]
t:2110 [in mathcomp.ssreflect.seq]
t:2116 [in mathcomp.ssreflect.seq]
T:212 [in mathcomp.ssreflect.binomial]
t:212 [in mathcomp.solvable.extremal]
T:2124 [in mathcomp.ssreflect.order]
t:2128 [in mathcomp.ssreflect.seq]
t:2140 [in mathcomp.ssreflect.seq]
t:215 [in mathcomp.solvable.extremal]
t:2150 [in mathcomp.ssreflect.seq]
t:217 [in mathcomp.ssreflect.binomial]
t:217 [in mathcomp.fingroup.perm]
t:218 [in mathcomp.ssreflect.binomial]
t:218 [in mathcomp.solvable.extremal]
t:218 [in mathcomp.solvable.burnside_app]
T:2188 [in mathcomp.ssreflect.order]
t:2190 [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.fingroup.perm]
t:220 [in mathcomp.solvable.extremal]
T:2203 [in mathcomp.ssreflect.order]
t:221 [in mathcomp.fingroup.perm]
T:221 [in mathcomp.ssreflect.order]
t:221 [in mathcomp.solvable.extremal]
t:222 [in mathcomp.fingroup.perm]
t:222 [in mathcomp.solvable.extremal]
t:2229 [in mathcomp.ssreflect.seq]
t:223 [in mathcomp.solvable.extremal]
T:2236 [in mathcomp.ssreflect.order]
t:224 [in mathcomp.solvable.extremal]
t:2245 [in mathcomp.ssreflect.seq]
t:2258 [in mathcomp.ssreflect.seq]
T:226 [in mathcomp.ssreflect.choice]
t:227 [in mathcomp.ssreflect.binomial]
t:227 [in mathcomp.solvable.extremal]
t:2273 [in mathcomp.ssreflect.seq]
T:228 [in mathcomp.ssreflect.order]
t:2283 [in mathcomp.algebra.ssrnum]
t:2284 [in mathcomp.algebra.ssrnum]
t:2286 [in mathcomp.ssreflect.seq]
t:229 [in mathcomp.fingroup.perm]
T:229 [in mathcomp.ssreflect.tuple]
t:2296 [in mathcomp.algebra.ssrnum]
t:2297 [in mathcomp.algebra.ssrnum]
T:2299 [in mathcomp.ssreflect.seq]
T:23 [in mathcomp.algebra.interval]
T:23 [in mathcomp.ssreflect.tuple]
t:23 [in mathcomp.solvable.primitive_action]
t:230 [in mathcomp.ssreflect.binomial]
t:230 [in mathcomp.fingroup.perm]
t:2302 [in mathcomp.ssreflect.order]
t:2306 [in mathcomp.ssreflect.seq]
t:2306 [in mathcomp.ssreflect.order]
t:231 [in mathcomp.fingroup.perm]
T:231 [in mathcomp.ssreflect.tuple]
t:2318 [in mathcomp.ssreflect.seq]
t:2318 [in mathcomp.ssreflect.order]
t:232 [in mathcomp.ssreflect.binomial]
T:232 [in mathcomp.ssreflect.order]
t:232 [in mathcomp.solvable.extremal]
t:2320 [in mathcomp.algebra.ssrnum]
t:2321 [in mathcomp.algebra.ssrnum]
t:2327 [in mathcomp.ssreflect.seq]
t:233 [in mathcomp.ssreflect.tuple]
T:2333 [in mathcomp.ssreflect.order]
t:2337 [in mathcomp.ssreflect.seq]
t:2337 [in mathcomp.ssreflect.order]
t:2341 [in mathcomp.ssreflect.order]
t:235 [in mathcomp.ssreflect.binomial]
t:2353 [in mathcomp.ssreflect.order]
t:236 [in mathcomp.ssreflect.binomial]
T:236 [in mathcomp.ssreflect.tuple]
T:236 [in mathcomp.ssreflect.path]
T:236 [in mathcomp.ssreflect.order]
t:2360 [in mathcomp.algebra.ssrnum]
t:2361 [in mathcomp.algebra.ssrnum]
t:237 [in mathcomp.ssreflect.tuple]
t:237 [in mathcomp.solvable.extremal]
t:2374 [in mathcomp.ssreflect.seq]
t:238 [in mathcomp.ssreflect.binomial]
T:238 [in mathcomp.ssreflect.choice]
T:239 [in mathcomp.ssreflect.tuple]
T:239 [in mathcomp.ssreflect.choice]
T:239 [in mathcomp.ssreflect.path]
T:24 [in mathcomp.algebra.interval]
T:24 [in mathcomp.ssreflect.finset]
t:240 [in mathcomp.ssreflect.binomial]
T:240 [in mathcomp.ssreflect.order]
t:241 [in mathcomp.ssreflect.binomial]
T:241 [in mathcomp.ssreflect.eqtype]
t:2416 [in mathcomp.ssreflect.order]
T:242 [in mathcomp.ssreflect.tuple]
t:242 [in mathcomp.solvable.extremal]
T:2430 [in mathcomp.ssreflect.seq]
t:244 [in mathcomp.ssreflect.binomial]
t:244 [in mathcomp.solvable.extremal]
T:244 [in mathcomp.ssreflect.eqtype]
T:2440 [in mathcomp.ssreflect.seq]
T:2448 [in mathcomp.ssreflect.seq]
t:245 [in mathcomp.solvable.extremal]
T:2456 [in mathcomp.ssreflect.seq]
t:246 [in mathcomp.solvable.extremal]
T:2460 [in mathcomp.ssreflect.seq]
T:2466 [in mathcomp.ssreflect.seq]
T:247 [in mathcomp.ssreflect.choice]
t:247 [in mathcomp.solvable.extremal]
T:2474 [in mathcomp.ssreflect.seq]
t:248 [in mathcomp.solvable.extremal]
T:2483 [in mathcomp.ssreflect.seq]
t:249 [in mathcomp.solvable.extremal]
T:2490 [in mathcomp.ssreflect.seq]
T:2494 [in mathcomp.ssreflect.seq]
t:25 [in mathcomp.fingroup.perm]
T:25 [in mathcomp.algebra.interval]
t:25 [in mathcomp.ssreflect.tuple]
T:25 [in mathcomp.ssreflect.prime]
T:25 [in mathcomp.ssreflect.bigop]
T:2510 [in mathcomp.ssreflect.order]
t:252 [in mathcomp.ssreflect.binomial]
T:2530 [in mathcomp.ssreflect.order]
T:2534 [in mathcomp.ssreflect.seq]
T:2534 [in mathcomp.ssreflect.order]
T:2539 [in mathcomp.ssreflect.seq]
T:2539 [in mathcomp.ssreflect.order]
T:2543 [in mathcomp.ssreflect.seq]
T:2547 [in mathcomp.ssreflect.order]
T:2548 [in mathcomp.ssreflect.seq]
T:2551 [in mathcomp.ssreflect.seq]
T:2552 [in mathcomp.ssreflect.order]
T:2556 [in mathcomp.ssreflect.seq]
T:2568 [in mathcomp.ssreflect.order]
T:2594 [in mathcomp.ssreflect.order]
T:2598 [in mathcomp.ssreflect.order]
T:26 [in mathcomp.algebra.interval]
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.algebra.matrix]
t:2634 [in mathcomp.ssreflect.seq]
T:2634 [in mathcomp.ssreflect.order]
t:2635 [in mathcomp.ssreflect.seq]
T:2636 [in mathcomp.algebra.matrix]
t:264 [in mathcomp.ssreflect.binomial]
t:264 [in mathcomp.fingroup.perm]
T:2640 [in mathcomp.algebra.matrix]
t:2643 [in mathcomp.ssreflect.seq]
t:2644 [in mathcomp.ssreflect.seq]
t:2649 [in mathcomp.ssreflect.seq]
t:265 [in mathcomp.ssreflect.binomial]
T:2654 [in mathcomp.ssreflect.order]
t:2655 [in mathcomp.ssreflect.seq]
t:2656 [in mathcomp.ssreflect.seq]
t:2659 [in mathcomp.ssreflect.seq]
T:266 [in mathcomp.ssreflect.eqtype]
t:2661 [in mathcomp.ssreflect.seq]
t:2662 [in mathcomp.ssreflect.seq]
t:2667 [in mathcomp.ssreflect.seq]
T:2668 [in mathcomp.ssreflect.order]
t:2669 [in mathcomp.ssreflect.seq]
t:2676 [in mathcomp.ssreflect.seq]
T:2676 [in mathcomp.algebra.matrix]
t:268 [in mathcomp.ssreflect.binomial]
T:2690 [in mathcomp.ssreflect.order]
T:27 [in mathcomp.ssreflect.generic_quotient]
T:27 [in mathcomp.algebra.interval]
T:27 [in mathcomp.ssreflect.eqtype]
T:2700 [in mathcomp.ssreflect.order]
T:2712 [in mathcomp.ssreflect.order]
t:272 [in mathcomp.ssreflect.binomial]
T:2731 [in mathcomp.ssreflect.order]
T:2738 [in mathcomp.ssreflect.order]
T:2754 [in mathcomp.ssreflect.order]
t:276 [in mathcomp.ssreflect.binomial]
T:2769 [in mathcomp.ssreflect.order]
t:277 [in mathcomp.ssreflect.binomial]
T:277 [in mathcomp.fingroup.action]
T:278 [in mathcomp.fingroup.action]
T:2783 [in mathcomp.ssreflect.order]
T:279 [in mathcomp.fingroup.action]
T:2798 [in mathcomp.ssreflect.order]
t:28 [in mathcomp.fingroup.perm]
T:28 [in mathcomp.algebra.interval]
T:28 [in mathcomp.ssreflect.fintype]
T:280 [in mathcomp.fingroup.action]
T:2802 [in mathcomp.ssreflect.order]
T:281 [in mathcomp.fingroup.action]
T:2811 [in mathcomp.ssreflect.order]
T:2822 [in mathcomp.ssreflect.order]
T:2830 [in mathcomp.ssreflect.bigop]
T:284 [in mathcomp.ssreflect.order]
T:2850 [in mathcomp.ssreflect.order]
T:2859 [in mathcomp.ssreflect.order]
T:2861 [in mathcomp.algebra.matrix]
T:2868 [in mathcomp.ssreflect.order]
t:287 [in mathcomp.field.algebraics_fundamentals]
T:2873 [in mathcomp.algebra.matrix]
T:2879 [in mathcomp.ssreflect.order]
t:288 [in mathcomp.solvable.extremal]
T:289 [in mathcomp.ssreflect.order]
T:2890 [in mathcomp.ssreflect.order]
T:2897 [in mathcomp.ssreflect.order]
T:2898 [in mathcomp.algebra.matrix]
T:29 [in mathcomp.algebra.interval]
T:29 [in mathcomp.field.closed_field]
T:2904 [in mathcomp.ssreflect.order]
T:2911 [in mathcomp.ssreflect.order]
T:2915 [in mathcomp.algebra.matrix]
T:2923 [in mathcomp.algebra.matrix]
T:2923 [in mathcomp.ssreflect.order]
T:293 [in mathcomp.ssreflect.order]
T:2957 [in mathcomp.ssreflect.order]
T:2968 [in mathcomp.ssreflect.order]
T:297 [in mathcomp.ssreflect.order]
T:2979 [in mathcomp.ssreflect.order]
T:2986 [in mathcomp.ssreflect.order]
T:2993 [in mathcomp.ssreflect.order]
T:30 [in mathcomp.algebra.interval]
T:30 [in mathcomp.ssreflect.order]
T:30 [in mathcomp.ssreflect.fintype]
T:301 [in mathcomp.ssreflect.order]
t:303 [in mathcomp.field.closed_field]
T:3033 [in mathcomp.ssreflect.order]
T:3040 [in mathcomp.ssreflect.order]
T:3047 [in mathcomp.ssreflect.order]
T:3054 [in mathcomp.ssreflect.order]
T:3061 [in mathcomp.ssreflect.order]
T:3068 [in mathcomp.ssreflect.order]
T:3075 [in mathcomp.ssreflect.order]
t:308 [in mathcomp.field.closed_field]
T:3082 [in mathcomp.ssreflect.order]
T:3089 [in mathcomp.ssreflect.order]
t:309 [in mathcomp.fingroup.perm]
T:3096 [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:3103 [in mathcomp.ssreflect.order]
T:3110 [in mathcomp.ssreflect.order]
T:3117 [in mathcomp.ssreflect.order]
t:312 [in mathcomp.field.closed_field]
T:312 [in mathcomp.ssreflect.order]
T:3125 [in mathcomp.ssreflect.order]
T:3131 [in mathcomp.ssreflect.order]
T:3141 [in mathcomp.ssreflect.order]
T:316 [in mathcomp.ssreflect.order]
T:316 [in mathcomp.ssreflect.eqtype]
T:3179 [in mathcomp.ssreflect.order]
T:3194 [in mathcomp.ssreflect.order]
t:32 [in mathcomp.solvable.primitive_action]
T:32 [in mathcomp.ssreflect.bigop]
T:3201 [in mathcomp.ssreflect.order]
T:3210 [in mathcomp.ssreflect.order]
T:3220 [in mathcomp.ssreflect.order]
T:323 [in mathcomp.ssreflect.order]
T:3230 [in mathcomp.ssreflect.order]
T:3235 [in mathcomp.ssreflect.order]
T:3250 [in mathcomp.ssreflect.order]
T:3265 [in mathcomp.ssreflect.order]
T:327 [in mathcomp.ssreflect.order]
T:327 [in mathcomp.ssreflect.eqtype]
T:3272 [in mathcomp.ssreflect.order]
T:3279 [in mathcomp.ssreflect.order]
T:3286 [in mathcomp.ssreflect.order]
T:3293 [in mathcomp.ssreflect.order]
t:33 [in mathcomp.fingroup.perm]
T:330 [in mathcomp.ssreflect.eqtype]
T:3300 [in mathcomp.ssreflect.order]
T:3307 [in mathcomp.ssreflect.order]
T:3314 [in mathcomp.ssreflect.order]
T:332 [in mathcomp.ssreflect.order]
T:332 [in mathcomp.ssreflect.eqtype]
T:3321 [in mathcomp.ssreflect.order]
T:3328 [in mathcomp.ssreflect.order]
T:3335 [in mathcomp.ssreflect.order]
T:3342 [in mathcomp.ssreflect.order]
T:3349 [in mathcomp.ssreflect.order]
T:3356 [in mathcomp.ssreflect.order]
T:336 [in mathcomp.ssreflect.order]
T:3363 [in mathcomp.ssreflect.order]
T:3370 [in mathcomp.ssreflect.order]
T:3377 [in mathcomp.ssreflect.order]
t:338 [in mathcomp.field.closed_field]
T:3382 [in mathcomp.ssreflect.order]
T:3387 [in mathcomp.ssreflect.order]
T:3399 [in mathcomp.ssreflect.order]
T:34 [in mathcomp.ssreflect.generic_quotient]
t:34 [in mathcomp.solvable.primitive_action]
T:34 [in mathcomp.ssreflect.fintype]
T:340 [in mathcomp.ssreflect.order]
T:340 [in mathcomp.ssreflect.eqtype]
T:3415 [in mathcomp.ssreflect.order]
T:3427 [in mathcomp.ssreflect.order]
t:343 [in mathcomp.field.closed_field]
T:3437 [in mathcomp.ssreflect.order]
T:344 [in mathcomp.ssreflect.order]
T:3448 [in mathcomp.ssreflect.order]
T:3455 [in mathcomp.ssreflect.order]
T:3462 [in mathcomp.ssreflect.order]
T:3469 [in mathcomp.ssreflect.order]
T:3476 [in mathcomp.ssreflect.order]
T:348 [in mathcomp.ssreflect.order]
T:3481 [in mathcomp.ssreflect.order]
T:3492 [in mathcomp.ssreflect.order]
t:35 [in mathcomp.ssreflect.choice]
T:35 [in mathcomp.field.closed_field]
T:3505 [in mathcomp.ssreflect.order]
T:3518 [in mathcomp.ssreflect.order]
T:352 [in mathcomp.ssreflect.order]
T:3528 [in mathcomp.ssreflect.order]
T:3539 [in mathcomp.ssreflect.order]
T:3546 [in mathcomp.ssreflect.order]
T:355 [in mathcomp.ssreflect.tuple]
T:355 [in mathcomp.ssreflect.order]
T:3553 [in mathcomp.ssreflect.order]
T:3560 [in mathcomp.ssreflect.order]
T:3567 [in mathcomp.ssreflect.order]
T:357 [in mathcomp.ssreflect.tuple]
T:3572 [in mathcomp.ssreflect.order]
t:358 [in mathcomp.ssreflect.tuple]
T:3583 [in mathcomp.ssreflect.order]
T:3596 [in mathcomp.ssreflect.order]
T:360 [in mathcomp.ssreflect.tuple]
T:3609 [in mathcomp.ssreflect.order]
T:3619 [in mathcomp.ssreflect.order]
T:3626 [in mathcomp.ssreflect.order]
T:363 [in mathcomp.ssreflect.tuple]
T:3631 [in mathcomp.ssreflect.order]
T:364 [in mathcomp.ssreflect.eqtype]
T:3643 [in mathcomp.ssreflect.order]
T:365 [in mathcomp.ssreflect.tuple]
T:3653 [in mathcomp.ssreflect.order]
T:3667 [in mathcomp.ssreflect.order]
T:367 [in mathcomp.ssreflect.tuple]
T:367 [in mathcomp.ssreflect.eqtype]
T:3677 [in mathcomp.ssreflect.order]
T:3684 [in mathcomp.ssreflect.order]
T:3694 [in mathcomp.ssreflect.order]
t:37 [in mathcomp.ssreflect.tuple]
T:3704 [in mathcomp.ssreflect.order]
T:371 [in mathcomp.ssreflect.tuple]
T:3714 [in mathcomp.ssreflect.order]
T:3724 [in mathcomp.ssreflect.order]
t:373 [in mathcomp.ssreflect.tuple]
T:373 [in mathcomp.ssreflect.eqtype]
T:3730 [in mathcomp.ssreflect.order]
T:375 [in mathcomp.ssreflect.tuple]
T:377 [in mathcomp.ssreflect.tuple]
T:377 [in mathcomp.ssreflect.eqtype]
T:38 [in mathcomp.ssreflect.finset]
T:381 [in mathcomp.ssreflect.tuple]
T:382 [in mathcomp.ssreflect.eqtype]
T:383 [in mathcomp.ssreflect.tuple]
T:385 [in mathcomp.ssreflect.tuple]
t:393 [in mathcomp.ssreflect.seq]
t:396 [in mathcomp.ssreflect.seq]
t:399 [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:4000 [in mathcomp.ssreflect.order]
T:4005 [in mathcomp.ssreflect.order]
T:4007 [in mathcomp.ssreflect.order]
T:4009 [in mathcomp.ssreflect.order]
T:4011 [in mathcomp.ssreflect.order]
t:402 [in mathcomp.algebra.ssrnum]
t:405 [in mathcomp.ssreflect.seq]
T:4053 [in mathcomp.ssreflect.order]
T:4055 [in mathcomp.ssreflect.order]
t:406 [in mathcomp.algebra.ssrnum]
T:4072 [in mathcomp.ssreflect.order]
T:4074 [in mathcomp.ssreflect.order]
T:4076 [in mathcomp.ssreflect.order]
T:4078 [in mathcomp.ssreflect.order]
T:4082 [in mathcomp.ssreflect.order]
T:4084 [in mathcomp.ssreflect.order]
T:4086 [in mathcomp.ssreflect.order]
T:4088 [in mathcomp.ssreflect.order]
T:4090 [in mathcomp.ssreflect.order]
T:4092 [in mathcomp.ssreflect.order]
T:4094 [in mathcomp.ssreflect.order]
T:4096 [in mathcomp.ssreflect.order]
T:4098 [in mathcomp.ssreflect.order]
t:41 [in mathcomp.ssreflect.tuple]
T:41 [in mathcomp.ssreflect.order]
t:410 [in mathcomp.algebra.ssrnum]
T:4100 [in mathcomp.ssreflect.order]
T:4102 [in mathcomp.ssreflect.order]
T:4104 [in mathcomp.ssreflect.order]
T:4106 [in mathcomp.ssreflect.order]
t:4112 [in mathcomp.ssreflect.order]
t:4119 [in mathcomp.ssreflect.order]
T:4132 [in mathcomp.ssreflect.order]
t:4134 [in mathcomp.ssreflect.order]
t:4137 [in mathcomp.ssreflect.order]
t:4138 [in mathcomp.ssreflect.order]
t:4139 [in mathcomp.ssreflect.order]
t:414 [in mathcomp.algebra.ssrnum]
t:4142 [in mathcomp.ssreflect.order]
t:4144 [in mathcomp.ssreflect.order]
t:4145 [in mathcomp.ssreflect.order]
t:4147 [in mathcomp.ssreflect.order]
T:4149 [in mathcomp.ssreflect.order]
T:4154 [in mathcomp.ssreflect.order]
T:4156 [in mathcomp.ssreflect.order]
T:4158 [in mathcomp.ssreflect.order]
T:4160 [in mathcomp.ssreflect.order]
t:418 [in mathcomp.algebra.ssrnum]
T:4182 [in mathcomp.ssreflect.order]
T:4191 [in mathcomp.ssreflect.order]
T:4195 [in mathcomp.ssreflect.order]
T:4197 [in mathcomp.ssreflect.order]
T:4199 [in mathcomp.ssreflect.order]
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:4202 [in mathcomp.ssreflect.order]
T:4205 [in mathcomp.ssreflect.order]
T:4206 [in mathcomp.ssreflect.order]
T:4207 [in mathcomp.ssreflect.order]
t:422 [in mathcomp.algebra.ssrnum]
t:426 [in mathcomp.algebra.ssrnum]
T:4260 [in mathcomp.ssreflect.order]
T:4261 [in mathcomp.ssreflect.order]
T:4262 [in mathcomp.ssreflect.order]
T:4264 [in mathcomp.ssreflect.order]
T:4267 [in mathcomp.ssreflect.order]
T:4268 [in mathcomp.ssreflect.order]
T:4269 [in mathcomp.ssreflect.order]
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:432 [in mathcomp.ssreflect.seq]
T:4327 [in mathcomp.ssreflect.order]
T:4329 [in mathcomp.ssreflect.order]
T:4330 [in mathcomp.ssreflect.order]
T:4331 [in mathcomp.ssreflect.order]
T:4334 [in mathcomp.ssreflect.order]
T:4338 [in mathcomp.ssreflect.order]
T:4339 [in mathcomp.ssreflect.order]
t:434 [in mathcomp.ssreflect.seq]
T:434 [in mathcomp.ssreflect.ssrnat]
T:4340 [in mathcomp.ssreflect.order]
T:4341 [in mathcomp.ssreflect.order]
T:4343 [in mathcomp.ssreflect.order]
T:4345 [in mathcomp.ssreflect.order]
T:4347 [in mathcomp.ssreflect.order]
T:4354 [in mathcomp.ssreflect.order]
t:4395 [in mathcomp.ssreflect.order]
t:4398 [in mathcomp.ssreflect.order]
T:440 [in mathcomp.ssreflect.order]
T:4402 [in mathcomp.ssreflect.order]
T:4404 [in mathcomp.ssreflect.order]
t:441 [in mathcomp.character.inertia]
t:4424 [in mathcomp.ssreflect.order]
t:4425 [in mathcomp.ssreflect.order]
t:4427 [in mathcomp.ssreflect.order]
t:4428 [in mathcomp.ssreflect.order]
T:4432 [in mathcomp.ssreflect.order]
T:4434 [in mathcomp.ssreflect.order]
T:4436 [in mathcomp.ssreflect.order]
T:4438 [in mathcomp.ssreflect.order]
T:4441 [in mathcomp.ssreflect.order]
T:4443 [in mathcomp.ssreflect.order]
T:4445 [in mathcomp.ssreflect.order]
T:4447 [in mathcomp.ssreflect.order]
T:4449 [in mathcomp.ssreflect.order]
T:4451 [in mathcomp.ssreflect.order]
T:4453 [in mathcomp.ssreflect.order]
T:4455 [in mathcomp.ssreflect.order]
T:4457 [in mathcomp.ssreflect.order]
T:4459 [in mathcomp.ssreflect.order]
T:4461 [in mathcomp.ssreflect.order]
T:4463 [in mathcomp.ssreflect.order]
T:4465 [in mathcomp.ssreflect.order]
T:4468 [in mathcomp.ssreflect.order]
T:4472 [in mathcomp.ssreflect.order]
T:4473 [in mathcomp.ssreflect.order]
T:4474 [in mathcomp.ssreflect.order]
T:4475 [in mathcomp.ssreflect.order]
T:4477 [in mathcomp.ssreflect.order]
T:4479 [in mathcomp.ssreflect.order]
T:4481 [in mathcomp.ssreflect.order]
T:4487 [in mathcomp.ssreflect.order]
t:449 [in mathcomp.ssreflect.order]
T:4493 [in mathcomp.ssreflect.order]
T:45 [in mathcomp.ssreflect.bigop]
T:4500 [in mathcomp.ssreflect.order]
T:4502 [in mathcomp.ssreflect.order]
T:4504 [in mathcomp.ssreflect.order]
t:4507 [in mathcomp.ssreflect.order]
T:451 [in mathcomp.fingroup.action]
t:4510 [in mathcomp.ssreflect.order]
T:4513 [in mathcomp.ssreflect.order]
T:4516 [in mathcomp.ssreflect.order]
T:4518 [in mathcomp.ssreflect.order]
T:4520 [in mathcomp.ssreflect.order]
T:4522 [in mathcomp.ssreflect.order]
T:4524 [in mathcomp.ssreflect.order]
T:4526 [in mathcomp.ssreflect.order]
T:4528 [in mathcomp.ssreflect.order]
T:4530 [in mathcomp.ssreflect.order]
T:4534 [in mathcomp.ssreflect.order]
T:4536 [in mathcomp.ssreflect.order]
T:4556 [in mathcomp.ssreflect.order]
T:4558 [in mathcomp.ssreflect.order]
T:4560 [in mathcomp.ssreflect.order]
T:4580 [in mathcomp.ssreflect.order]
T:46 [in mathcomp.fingroup.fingroup]
T:4610 [in mathcomp.ssreflect.order]
T:4620 [in mathcomp.ssreflect.order]
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:480 [in mathcomp.character.inertia]
t:494 [in mathcomp.ssreflect.path]
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:505 [in mathcomp.ssreflect.seq]
t:509 [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: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.inertia]
t:542 [in mathcomp.character.character]
T:543 [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:553 [in mathcomp.character.character]
T:554 [in mathcomp.ssreflect.path]
T:558 [in mathcomp.ssreflect.fintype]
t:559 [in mathcomp.character.character]
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:614 [in mathcomp.ssreflect.ssrnat]
t:633 [in mathcomp.ssreflect.path]
t:635 [in mathcomp.ssreflect.path]
t:637 [in mathcomp.ssreflect.path]
t:638 [in mathcomp.ssreflect.seq]
T:639 [in mathcomp.algebra.ssralg]
T:64 [in mathcomp.algebra.ring_quotient]
T:64 [in mathcomp.ssreflect.prime]
T:640 [in mathcomp.algebra.ssralg]
t:644 [in mathcomp.ssreflect.path]
T:645 [in mathcomp.ssreflect.fintype]
t:646 [in mathcomp.ssreflect.path]
T:65 [in mathcomp.ssreflect.ssrfun]
T:65 [in mathcomp.ssreflect.bigop]
T:651 [in mathcomp.ssreflect.path]
T:654 [in mathcomp.ssreflect.path]
T:658 [in mathcomp.ssreflect.path]
t:66 [in mathcomp.ssreflect.tuple]
T:662 [in mathcomp.ssreflect.path]
T:666 [in mathcomp.ssreflect.path]
t:67 [in mathcomp.ssreflect.ssrAC]
T:676 [in mathcomp.ssreflect.path]
T:677 [in mathcomp.ssreflect.ssrnat]
t:68 [in mathcomp.ssreflect.tuple]
T:689 [in mathcomp.ssreflect.fintype]
T:698 [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:704 [in mathcomp.ssreflect.fintype]
T:71 [in mathcomp.ssreflect.ssrbool]
T:712 [in mathcomp.ssreflect.fintype]
t:72 [in mathcomp.ssreflect.tuple]
t:73 [in mathcomp.ssreflect.tuple]
T:73 [in mathcomp.ssreflect.choice]
T:738 [in mathcomp.ssreflect.seq]
T:74 [in mathcomp.ssreflect.bigop]
T:740 [in mathcomp.ssreflect.seq]
T:741 [in mathcomp.ssreflect.fintype]
t:75 [in mathcomp.ssreflect.tuple]
T:750 [in mathcomp.ssreflect.fintype]
T:759 [in mathcomp.ssreflect.fintype]
t:76 [in mathcomp.solvable.extremal]
t:77 [in mathcomp.ssreflect.tuple]
t:77 [in mathcomp.solvable.extremal]
T:771 [in mathcomp.ssreflect.fintype]
T:778 [in mathcomp.ssreflect.seq]
t:78 [in mathcomp.ssreflect.tuple]
T:783 [in mathcomp.ssreflect.seq]
t:786 [in mathcomp.ssreflect.order]
T:789 [in mathcomp.ssreflect.path]
T:79 [in mathcomp.ssreflect.ssrAC]
t:790 [in mathcomp.ssreflect.order]
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:85 [in mathcomp.ssreflect.tuple]
t:857 [in mathcomp.ssreflect.seq]
t:86 [in mathcomp.ssreflect.tuple]
T:863 [in mathcomp.algebra.matrix]
T:867 [in mathcomp.ssreflect.fintype]
t:87 [in mathcomp.ssreflect.tuple]
T:87 [in mathcomp.ssreflect.finfun]
T:87 [in mathcomp.algebra.ring_quotient]
T:870 [in mathcomp.ssreflect.fintype]
t:88 [in mathcomp.ssreflect.tuple]
T:88 [in mathcomp.ssreflect.bigop]
T:885 [in mathcomp.algebra.matrix]
t:887 [in mathcomp.ssreflect.bigop]
t:89 [in mathcomp.ssreflect.tuple]
t:891 [in mathcomp.ssreflect.seq]
T:9 [in mathcomp.ssreflect.eqtype]
t:90 [in mathcomp.ssreflect.tuple]
t:91 [in mathcomp.ssreflect.tuple]
t:91 [in mathcomp.ssreflect.finfun]
t:93 [in mathcomp.ssreflect.tuple]
T:93 [in mathcomp.ssreflect.bigop]
t:930 [in mathcomp.ssreflect.bigop]
T:942 [in mathcomp.algebra.matrix]
T:95 [in mathcomp.ssreflect.generic_quotient]
t:95 [in mathcomp.ssreflect.tuple]
T:953 [in mathcomp.ssreflect.finset]
T:957 [in mathcomp.ssreflect.finset]
T:960 [in mathcomp.ssreflect.finset]
T:965 [in mathcomp.ssreflect.finset]
T:97 [in mathcomp.ssreflect.ssrAC]
T:971 [in mathcomp.algebra.matrix]
t:98 [in mathcomp.ssreflect.tuple]
t:980 [in mathcomp.ssreflect.order]
t:984 [in mathcomp.ssreflect.order]
t:988 [in mathcomp.ssreflect.order]
t:992 [in mathcomp.ssreflect.order]
T:995 [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 | (74637 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1852 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48381 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (277 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3804 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (91 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14415 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (132 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1342 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1003 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3033 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |