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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

wf_tally [definition, in mathcomp.ssreflect.seq]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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