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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

## 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:778 [binder, in mathcomp.algebra.matrix]

wf_tally [definition, in mathcomp.ssreflect.seq]

wf_proj:1884 [binder, in mathcomp.algebra.ssralg]

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:27 [binder, in mathcomp.algebra.vector]

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':1049 [binder, in mathcomp.character.mxrepresentation]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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:209 [binder, in mathcomp.algebra.ssrnum]

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

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

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

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:2333 [binder, in mathcomp.algebra.ssralg]

W:2342 [binder, in mathcomp.algebra.ssralg]

W:2348 [binder, in mathcomp.algebra.ssralg]

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

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

W:2352 [binder, in mathcomp.algebra.ssralg]

W:2361 [binder, in mathcomp.algebra.ssralg]

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

W:2373 [binder, in mathcomp.algebra.ssralg]

W:2382 [binder, in mathcomp.algebra.ssralg]

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

W:2390 [binder, in mathcomp.algebra.ssralg]

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

W:2401 [binder, in mathcomp.algebra.ssralg]

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

W:2410 [binder, in mathcomp.algebra.ssralg]

W:2418 [binder, in mathcomp.algebra.ssralg]

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

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

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

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

W:2519 [binder, in mathcomp.algebra.ssralg]

W:2528 [binder, in mathcomp.algebra.ssralg]

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

W:2536 [binder, in mathcomp.algebra.ssralg]

W:2545 [binder, in mathcomp.algebra.ssralg]

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

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

W:2553 [binder, in mathcomp.algebra.ssralg]

W:2562 [binder, in mathcomp.algebra.ssralg]

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

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

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

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: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:290 [binder, in mathcomp.field.algebraics_fundamentals]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

W:655 [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:665 [binder, in mathcomp.character.mxrepresentation]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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