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 | (100113 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 | (1864 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 | (49278 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 | (1631 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 | (6978 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 | (94 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 | (14781 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 | (75 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) |

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 | (131 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 | (2030 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 | (2189 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 | (1149 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 | (19126 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 | (565 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:2019 [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:246 [binder, in mathcomp.character.character]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.ssrnum]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

w:162 [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:201 [binder, in mathcomp.field.separable]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

W:332 [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:378 [binder, in mathcomp.field.closed_field]

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

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

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

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

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.character.mxrepresentation]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 | (100113 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 | (1864 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 | (49278 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 | (1631 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 | (6978 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 | (94 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 | (14781 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 | (75 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) |

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 | (131 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 | (2030 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 | (2189 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 | (1149 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 | (19126 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 | (565 entries) |