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)

K

ker [definition, in morphism]
kercoset_rcoset [lemma, in quotient]
kerE [lemma, in morphism]
kerHK [definition, in center]
kermx [definition, in mxalgebra]
kermx_hom_module [lemma, in mxrepresentation]
kermx_eq0 [lemma, in mxalgebra]
kermx_centg_module [lemma, in mxrepresentation]
kerP [lemma, in morphism]
ker_cprodm [lemma, in gproduct]
ker_cprod_by_central [lemma, in center]
ker_reprGLm [lemma, in mxabelem]
ker_in_cprod [lemma, in center]
ker_autm [lemma, in automorphism]
ker_sub_pre [lemma, in morphism]
ker_ifactm [lemma, in morphism]
ker_group [definition, in morphism]
ker_invm [lemma, in morphism]
ker_restrm [lemma, in morphism]
ker_dprodm [lemma, in gproduct]
ker_norm [lemma, in morphism]
ker_quotm [lemma, in quotient]
ker_comp [lemma, in morphism]
ker_trivm [lemma, in morphism]
ker_factm_loc [lemma, in morphism]
ker_factm [lemma, in morphism]
ker_coset [lemma, in quotient]
ker_irr_comp_op [lemma, in mxrepresentation]
ker_sgval [lemma, in morphism]
ker_eltm [lemma, in cyclic]
ker_normal_pre [lemma, in morphism]
ker_actperm [lemma, in action]
ker_subg [lemma, in morphism]
ker_conj_aut [lemma, in automorphism]
ker_trivg_morphim [lemma, in morphism]
ker_cprod_by [definition, in center]
ker_cprod_by_group [definition, in center]
ker_coset_prim [lemma, in quotient]
ker_restr_perm [lemma, in action]
ker_pprodm [lemma, in gproduct]
ker_idm [lemma, in morphism]
ker_cprod_by_is_group [lemma, in center]
ker_sdprodm [lemma, in gproduct]
ker_injm [lemma, in morphism]
ker_normal [lemma, in morphism]
ker_rcoset [lemma, in morphism]
kquo_repr_coset [lemma, in mxrepresentation]
kquo_repr [definition, in mxrepresentation]
kquo_mxE [lemma, in mxrepresentation]
kquo_mx [definition, in mxrepresentation]
kquo_mx_faithful [lemma, in 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 (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)