W (Global Index)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
W
W [abbrev, in mathcomp.group_representation.character]W [abbrev, in mathcomp.group_representation.character]
weak_second_isog [prf, in mathcomp.finite_group.quotient]
Wedderburn_annihilate [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_center [abbrev, in mathcomp.group_representation.mxrepresentation]
Wedderburn_center_pchar [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_closed [abbrev, in mathcomp.group_representation.mxrepresentation]
Wedderburn_closed_pchar [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_direct [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_disjoint [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_id [def, in mathcomp.group_representation.mxrepresentation]
Wedderburn_id_expansion [prf, in mathcomp.group_representation.character]
Wedderburn_id_mem [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_ideal [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_is_id [abbrev, in mathcomp.group_representation.mxrepresentation]
Wedderburn_is_id_pchar [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_is_ring [abbrev, in mathcomp.group_representation.mxrepresentation]
Wedderburn_is_ring_pchar [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_min_ideal [abbrev, in mathcomp.group_representation.mxrepresentation]
Wedderburn_min_ideal_pchar [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_mulmx0 [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_subring [def, in mathcomp.group_representation.mxrepresentation]
Wedderburn_subring_center [abbrev, in mathcomp.group_representation.mxrepresentation]
Wedderburn_subring_center_pchar [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_sum [abbrev, in mathcomp.group_representation.mxrepresentation]
Wedderburn_sum_id [abbrev, in mathcomp.group_representation.mxrepresentation]
Wedderburn_sum_id_pchar [prf, in mathcomp.group_representation.mxrepresentation]
Wedderburn_sum_pchar [prf, in mathcomp.group_representation.mxrepresentation]
wf_tally [def, in mathcomp.boot.seq]
widen_bseq [def, in mathcomp.boot.tuple]
widen_bseq_id [prf, in mathcomp.boot.tuple]
widen_bseq_in_bseq [prf, in mathcomp.boot.tuple]
widen_bseq_trans [prf, in mathcomp.boot.tuple]
widen_bseqK [prf, in mathcomp.boot.tuple]
widen_itv [def, in mathcomp.algebra.interval_inference]
widen_itvE [prf, in mathcomp.algebra.interval_inference]
widen_natitv [def, in mathcomp.algebra.interval_inference]
widen_natitvE [prf, in mathcomp.algebra.interval_inference]
widen_ord [def, in mathcomp.boot.fintype]
widen_ord_proof [prf, in mathcomp.boot.fintype]
widen_partn [prf, in mathcomp.boot.prime]
Wilson [prf, in mathcomp.boot.binomial]