Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (78577 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1807 entries) |

Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48032 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (375 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3995 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (91 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14468 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (223 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (133 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (451 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1387 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1144 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6179 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (247 entries) |

## W

W [abbreviation, in mathcomp.character.character]W [abbreviation, in mathcomp.character.character]

weak_second_isog [lemma, in mathcomp.fingroup.quotient]

Wedderburn_center [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_subring_center [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_min_ideal [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_is_ring [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_closed [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_is_id [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_id_mem [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_sum_id [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_id [definition, in mathcomp.character.mxrepresentation]

Wedderburn_sum [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_mulmx0 [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_annihilate [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_disjoint [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_direct [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_ideal [lemma, in mathcomp.character.mxrepresentation]

Wedderburn_subring [definition, in mathcomp.character.mxrepresentation]

Wedderburn_id_expansion [lemma, in mathcomp.character.character]

weight:791 [binder, in mathcomp.algebra.matrix]

wf_tally [definition, in mathcomp.ssreflect.seq]

widen_bseq_in_bseq [lemma, in mathcomp.ssreflect.tuple]

widen_bseq_trans [lemma, in mathcomp.ssreflect.tuple]

widen_bseqK [lemma, in mathcomp.ssreflect.tuple]

widen_bseq_id [lemma, in mathcomp.ssreflect.tuple]

widen_bseq [definition, in mathcomp.ssreflect.tuple]

widen_partn [lemma, in mathcomp.ssreflect.prime]

widen_ord [definition, in mathcomp.ssreflect.fintype]

widen_ord_proof [lemma, in mathcomp.ssreflect.fintype]

Wilson [lemma, in mathcomp.ssreflect.binomial]

Wi:244 [binder, in mathcomp.character.character]

wT:35 [binder, in mathcomp.algebra.vector]

W':1040 [binder, in mathcomp.character.mxrepresentation]

W':1041 [binder, in mathcomp.character.mxrepresentation]

W':1042 [binder, in mathcomp.character.mxrepresentation]

W':1043 [binder, in mathcomp.character.mxrepresentation]

W':1044 [binder, in mathcomp.character.mxrepresentation]

W':1045 [binder, in mathcomp.character.mxrepresentation]

W':1046 [binder, in mathcomp.character.mxrepresentation]

W':1047 [binder, in mathcomp.character.mxrepresentation]

W':1048 [binder, in mathcomp.character.mxrepresentation]

W':640 [binder, in mathcomp.character.mxrepresentation]

W1:568 [binder, in mathcomp.character.classfun]

W1:902 [binder, in mathcomp.character.mxrepresentation]

W2:569 [binder, in mathcomp.character.classfun]

W2:903 [binder, in mathcomp.character.mxrepresentation]

W:100 [binder, in mathcomp.character.mxrepresentation]

W:1000 [binder, in mathcomp.character.mxrepresentation]

W:1000 [binder, in mathcomp.character.character]

W:1001 [binder, in mathcomp.character.character]

W:1002 [binder, in mathcomp.character.character]

W:1003 [binder, in mathcomp.character.character]

W:1017 [binder, in mathcomp.character.mxrepresentation]

W:1022 [binder, in mathcomp.character.mxrepresentation]

W:1028 [binder, in mathcomp.character.mxrepresentation]

w:1029 [binder, in mathcomp.algebra.vector]

w:1031 [binder, in mathcomp.algebra.vector]

w:1035 [binder, in mathcomp.algebra.vector]

w:1037 [binder, in mathcomp.algebra.vector]

W:1056 [binder, in mathcomp.character.mxrepresentation]

W:1058 [binder, in mathcomp.character.mxrepresentation]

w:1059 [binder, in mathcomp.algebra.vector]

W:1060 [binder, in mathcomp.character.mxrepresentation]

W:1061 [binder, in mathcomp.character.mxrepresentation]

W:1078 [binder, in mathcomp.character.mxrepresentation]

w:11 [binder, in mathcomp.character.integral_char]

W:1134 [binder, in mathcomp.character.mxrepresentation]

W:1141 [binder, in mathcomp.character.mxrepresentation]

W:1142 [binder, in mathcomp.character.mxrepresentation]

W:1169 [binder, in mathcomp.algebra.mxalgebra]

W:1174 [binder, in mathcomp.algebra.mxalgebra]

W:1179 [binder, in mathcomp.algebra.mxalgebra]

W:118 [binder, in mathcomp.character.character]

W:1184 [binder, in mathcomp.algebra.mxalgebra]

W:1189 [binder, in mathcomp.algebra.mxalgebra]

w:12 [binder, in mathcomp.character.integral_char]

W:128 [binder, in mathcomp.character.character]

w:1281 [binder, in mathcomp.algebra.ssrnum]

w:1284 [binder, in mathcomp.algebra.ssrnum]

w:1286 [binder, in mathcomp.algebra.ssrnum]

w:1288 [binder, in mathcomp.algebra.ssrnum]

w:1290 [binder, in mathcomp.algebra.ssrnum]

w:1292 [binder, in mathcomp.algebra.ssrnum]

w:1306 [binder, in mathcomp.algebra.poly]

w:1307 [binder, in mathcomp.algebra.poly]

w:1308 [binder, in mathcomp.algebra.poly]

w:1309 [binder, in mathcomp.algebra.poly]

w:1310 [binder, in mathcomp.algebra.poly]

w:1311 [binder, in mathcomp.algebra.poly]

w:1327 [binder, in mathcomp.character.mxrepresentation]

w:1328 [binder, in mathcomp.character.mxrepresentation]

W:1332 [binder, in mathcomp.character.mxrepresentation]

W:1375 [binder, in mathcomp.algebra.mxalgebra]

W:1385 [binder, in mathcomp.character.mxrepresentation]

W:1391 [binder, in mathcomp.character.mxrepresentation]

W:1392 [binder, in mathcomp.character.mxrepresentation]

W:1393 [binder, in mathcomp.character.mxrepresentation]

w:146 [binder, in mathcomp.field.galois]

w:147 [binder, in mathcomp.field.galois]

w:148 [binder, in mathcomp.field.galois]

W:1501 [binder, in mathcomp.character.mxrepresentation]

W:1504 [binder, in mathcomp.character.mxrepresentation]

W:1507 [binder, in mathcomp.character.mxrepresentation]

W:1508 [binder, in mathcomp.character.mxrepresentation]

W:1509 [binder, in mathcomp.character.mxrepresentation]

w:151 [binder, in mathcomp.field.algnum]

W:1510 [binder, in mathcomp.character.mxrepresentation]

W:1520 [binder, in mathcomp.character.mxrepresentation]

W:1521 [binder, in mathcomp.character.mxrepresentation]

w:1522 [binder, in mathcomp.character.mxrepresentation]

W:1525 [binder, in mathcomp.character.mxrepresentation]

W:1527 [binder, in mathcomp.character.mxrepresentation]

W:1529 [binder, in mathcomp.character.mxrepresentation]

W:1538 [binder, in mathcomp.character.mxrepresentation]

W:1539 [binder, in mathcomp.character.mxrepresentation]

W:155 [binder, in mathcomp.character.character]

W:1552 [binder, in mathcomp.character.mxrepresentation]

W:1553 [binder, in mathcomp.character.mxrepresentation]

W:1556 [binder, in mathcomp.character.mxrepresentation]

W:1557 [binder, in mathcomp.character.mxrepresentation]

w:163 [binder, in mathcomp.field.algebraics_fundamentals]

w:164 [binder, in mathcomp.field.algebraics_fundamentals]

W:177 [binder, in mathcomp.character.mxrepresentation]

W:180 [binder, in mathcomp.character.mxrepresentation]

W:193 [binder, in mathcomp.field.separable]

W:195 [binder, in mathcomp.field.separable]

w:196 [binder, in mathcomp.field.falgebra]

W:199 [binder, in mathcomp.character.character]

W:201 [binder, in mathcomp.character.character]

W:202 [binder, in mathcomp.character.mxrepresentation]

W:203 [binder, in mathcomp.character.character]

w:215 [binder, in mathcomp.field.galois]

w:216 [binder, in mathcomp.field.galois]

w:217 [binder, in mathcomp.field.galois]

w:218 [binder, in mathcomp.field.galois]

w:219 [binder, in mathcomp.field.galois]

w:220 [binder, in mathcomp.field.galois]

w:2281 [binder, in mathcomp.algebra.ssrnum]

w:2282 [binder, in mathcomp.algebra.ssrnum]

w:238 [binder, in mathcomp.field.algebraics_fundamentals]

w:239 [binder, in mathcomp.character.mxabelem]

w:240 [binder, in mathcomp.character.mxabelem]

W:241 [binder, in mathcomp.character.mxrepresentation]

W:243 [binder, in mathcomp.character.mxrepresentation]

w:2435 [binder, in mathcomp.algebra.ssralg]

w:2443 [binder, in mathcomp.algebra.ssralg]

w:2444 [binder, in mathcomp.algebra.ssralg]

W:245 [binder, in mathcomp.character.mxrepresentation]

w:2472 [binder, in mathcomp.algebra.matrix]

W:251 [binder, in mathcomp.character.mxrepresentation]

W:253 [binder, in mathcomp.character.mxrepresentation]

W:255 [binder, in mathcomp.character.mxrepresentation]

W:257 [binder, in mathcomp.character.mxrepresentation]

w:258 [binder, in mathcomp.field.algebraics_fundamentals]

W:258 [binder, in mathcomp.algebra.vector]

W:259 [binder, in mathcomp.character.mxrepresentation]

W:265 [binder, in mathcomp.character.mxrepresentation]

W:267 [binder, in mathcomp.character.mxrepresentation]

W:269 [binder, in mathcomp.character.mxrepresentation]

W:275 [binder, in mathcomp.character.mxrepresentation]

w:275 [binder, in mathcomp.algebra.vector]

W:277 [binder, in mathcomp.character.mxrepresentation]

W:279 [binder, in mathcomp.character.mxrepresentation]

W:281 [binder, in mathcomp.character.mxrepresentation]

W:283 [binder, in mathcomp.character.mxrepresentation]

W:285 [binder, in mathcomp.character.mxrepresentation]

W:287 [binder, in mathcomp.character.mxrepresentation]

W:289 [binder, in mathcomp.character.mxrepresentation]

W:291 [binder, in mathcomp.character.mxrepresentation]

w:293 [binder, in mathcomp.field.algebraics_fundamentals]

w:294 [binder, in mathcomp.field.algebraics_fundamentals]

W:296 [binder, in mathcomp.character.mxrepresentation]

W:299 [binder, in mathcomp.character.mxrepresentation]

w:302 [binder, in mathcomp.field.algebraics_fundamentals]

W:302 [binder, in mathcomp.character.mxrepresentation]

w:303 [binder, in mathcomp.field.algebraics_fundamentals]

W:305 [binder, in mathcomp.character.mxrepresentation]

w:312 [binder, in mathcomp.field.falgebra]

w:313 [binder, in mathcomp.field.falgebra]

W:322 [binder, in mathcomp.algebra.vector]

W:325 [binder, in mathcomp.character.mxrepresentation]

W:330 [binder, in mathcomp.character.mxrepresentation]

w:331 [binder, in mathcomp.algebra.ssrnum]

W:334 [binder, in mathcomp.character.mxrepresentation]

w:335 [binder, in mathcomp.algebra.vector]

w:338 [binder, in mathcomp.algebra.vector]

W:343 [binder, in mathcomp.algebra.vector]

W:346 [binder, in mathcomp.algebra.vector]

W:353 [binder, in mathcomp.character.mxrepresentation]

w:373 [binder, in mathcomp.field.closed_field]

w:374 [binder, in mathcomp.field.closed_field]

W:383 [binder, in mathcomp.character.mxrepresentation]

w:403 [binder, in mathcomp.algebra.mxpoly]

W:411 [binder, in mathcomp.character.mxrepresentation]

W:456 [binder, in mathcomp.character.mxrepresentation]

W:460 [binder, in mathcomp.character.mxrepresentation]

w:48 [binder, in mathcomp.field.separable]

W:483 [binder, in mathcomp.character.mxrepresentation]

W:499 [binder, in mathcomp.character.mxrepresentation]

W:543 [binder, in mathcomp.character.mxrepresentation]

W:571 [binder, in mathcomp.character.mxrepresentation]

W:590 [binder, in mathcomp.character.mxrepresentation]

W:592 [binder, in mathcomp.character.mxrepresentation]

w:606 [binder, in mathcomp.field.galois]

w:607 [binder, in mathcomp.field.galois]

w:616 [binder, in mathcomp.field.galois]

W:616 [binder, in mathcomp.algebra.mxpoly]

w:617 [binder, in mathcomp.field.galois]

w:620 [binder, in mathcomp.field.galois]

w:621 [binder, in mathcomp.field.galois]

W:622 [binder, in mathcomp.algebra.mxpoly]

W:627 [binder, in mathcomp.character.mxrepresentation]

W:628 [binder, in mathcomp.character.mxrepresentation]

W:630 [binder, in mathcomp.character.mxrepresentation]

W:631 [binder, in mathcomp.character.mxrepresentation]

W:632 [binder, in mathcomp.character.mxrepresentation]

W:633 [binder, in mathcomp.character.mxrepresentation]

W:634 [binder, in mathcomp.character.mxrepresentation]

W:635 [binder, in mathcomp.algebra.mxpoly]

W:635 [binder, in mathcomp.character.mxrepresentation]

W:636 [binder, in mathcomp.character.mxrepresentation]

W:637 [binder, in mathcomp.character.mxrepresentation]

W:639 [binder, in mathcomp.character.mxrepresentation]

W:640 [binder, in mathcomp.algebra.mxpoly]

W:642 [binder, in mathcomp.character.mxrepresentation]

W:645 [binder, in mathcomp.algebra.mxpoly]

W:645 [binder, in mathcomp.character.mxrepresentation]

W:646 [binder, in mathcomp.character.mxrepresentation]

W:647 [binder, in mathcomp.character.mxrepresentation]

W:649 [binder, in mathcomp.algebra.mxpoly]

W:649 [binder, in mathcomp.character.mxrepresentation]

W:650 [binder, in mathcomp.character.mxrepresentation]

W:651 [binder, in mathcomp.character.mxrepresentation]

W:657 [binder, in mathcomp.character.mxrepresentation]

W:658 [binder, in mathcomp.character.mxrepresentation]

W:659 [binder, in mathcomp.character.mxrepresentation]

W:661 [binder, in mathcomp.character.mxrepresentation]

W:662 [binder, in mathcomp.character.mxrepresentation]

W:663 [binder, in mathcomp.character.mxrepresentation]

W:664 [binder, in mathcomp.character.mxrepresentation]

W:665 [binder, in mathcomp.character.mxrepresentation]

W:666 [binder, in mathcomp.character.mxrepresentation]

w:67 [binder, in mathcomp.field.fieldext]

W:671 [binder, in mathcomp.character.mxrepresentation]

W:696 [binder, in mathcomp.algebra.vector]

W:703 [binder, in mathcomp.algebra.mxpoly]

W:707 [binder, in mathcomp.algebra.mxpoly]

W:71 [binder, in mathcomp.field.falgebra]

W:754 [binder, in mathcomp.character.mxrepresentation]

W:756 [binder, in mathcomp.character.mxrepresentation]

W:758 [binder, in mathcomp.character.mxrepresentation]

W:762 [binder, in mathcomp.character.mxrepresentation]

W:764 [binder, in mathcomp.character.mxrepresentation]

W:766 [binder, in mathcomp.character.mxrepresentation]

w:794 [binder, in mathcomp.algebra.vector]

w:86 [binder, in mathcomp.field.algebraics_fundamentals]

w:880 [binder, in mathcomp.ssreflect.bigop]

w:892 [binder, in mathcomp.ssreflect.bigop]

W:900 [binder, in mathcomp.algebra.vector]

W:901 [binder, in mathcomp.character.mxrepresentation]

w:903 [binder, in mathcomp.ssreflect.bigop]

W:904 [binder, in mathcomp.algebra.vector]

W:906 [binder, in mathcomp.algebra.vector]

W:909 [binder, in mathcomp.algebra.vector]

w:913 [binder, in mathcomp.character.classfun]

w:914 [binder, in mathcomp.character.classfun]

w:914 [binder, in mathcomp.ssreflect.bigop]

w:915 [binder, in mathcomp.character.classfun]

w:916 [binder, in mathcomp.character.classfun]

w:917 [binder, in mathcomp.character.classfun]

W:917 [binder, in mathcomp.character.mxrepresentation]

W:925 [binder, in mathcomp.character.mxrepresentation]

w:930 [binder, in mathcomp.algebra.vector]

w:932 [binder, in mathcomp.algebra.vector]

w:934 [binder, in mathcomp.algebra.matrix]

w:935 [binder, in mathcomp.algebra.vector]

w:938 [binder, in mathcomp.algebra.vector]

w:938 [binder, in mathcomp.ssreflect.fintype]

w:944 [binder, in mathcomp.algebra.vector]

w:948 [binder, in mathcomp.algebra.vector]

W:952 [binder, in mathcomp.character.mxrepresentation]

w:952 [binder, in mathcomp.algebra.vector]

W:953 [binder, in mathcomp.character.mxrepresentation]

W:954 [binder, in mathcomp.character.mxrepresentation]

w:954 [binder, in mathcomp.algebra.vector]

W:955 [binder, in mathcomp.character.mxrepresentation]

w:959 [binder, in mathcomp.algebra.vector]

w:966 [binder, in mathcomp.algebra.vector]

w:970 [binder, in mathcomp.algebra.vector]

W:995 [binder, in mathcomp.character.mxrepresentation]

W:998 [binder, in mathcomp.character.mxrepresentation]

W:998 [binder, in mathcomp.character.character]

W:999 [binder, in mathcomp.character.character]

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (78577 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1807 entries) |

Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48032 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (375 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3995 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (91 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14468 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (223 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (133 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (451 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1387 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1144 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6179 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (247 entries) |