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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)

W

weak_second_isog [lemma, in quotient]
Wedderburn_id_mem [lemma, in mxrepresentation]
Wedderburn_subring [definition, in mxrepresentation]
Wedderburn_closed [lemma, in mxrepresentation]
Wedderburn_direct [lemma, in mxrepresentation]
Wedderburn_disjoint [lemma, in mxrepresentation]
Wedderburn_subring_center [lemma, in mxrepresentation]
Wedderburn_id [definition, in mxrepresentation]
Wedderburn_mulmx0 [lemma, in mxrepresentation]
Wedderburn_is_ring [lemma, in mxrepresentation]
Wedderburn_ideal [lemma, in mxrepresentation]
Wedderburn_sum [lemma, in mxrepresentation]
Wedderburn_min_ideal [lemma, in mxrepresentation]
Wedderburn_is_id [lemma, in mxrepresentation]
Wedderburn_center [lemma, in mxrepresentation]
Wedderburn_sum_id [lemma, in mxrepresentation]
Wedderburn_annihilate [lemma, in mxrepresentation]
widen_partn [lemma, in prime]
widen_ord_proof [lemma, in fintype]
widen_ord [definition, in fintype]
Wilson [lemma, in binomial]
wlog_neg [lemma, in ssrbool]
wrap [definition, in ssrfun]
Wrap [constructor, in ssrfun]
wrapped [record, in ssrfun]