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)

H

H [abbreviation, in quotient]
half [definition, in ssrnat]
half_add [lemma, in ssrnat]
half_double [definition, in ssrnat]
half_leq [lemma, in ssrnat]
half_gt0 [lemma, in ssrnat]
half_bit_double [lemma, in ssrnat]
Hall [definition, in pgroup]
Hall [section, in hall]
hall [library]
HallCorollaries [section, in hall]
HallCorollaries.gT [variable, in hall]
HallJ [lemma, in pgroup]
HallP [lemma, in pgroup]
Hall_subJ [lemma, in hall]
Hall_exists [lemma, in hall]
Hall_max [lemma, in pgroup]
Hall_pJsub [lemma, in sylow]
Hall_Frattini_arg [lemma, in hall]
Hall_psubJ [lemma, in sylow]
Hall_trans [lemma, in hall]
Hall_setI_normal [lemma, in sylow]
Hall_pi [lemma, in pgroup]
Hall_Witt_identity [lemma, in commutator]
Hall_exists_subJ [lemma, in hall]
Hall_superset [lemma, in hall]
Hall_Jsub [lemma, in hall]
Hall1 [lemma, in pgroup]
has [definition, in seq]
HasFrobeniusAction [constructor, in frobenius]
hasP [lemma, in seq]
hasPn [lemma, in seq]
has_rot [lemma, in seq]
has_rotr [lemma, in seq]
has_nil [lemma, in seq]
has_filter [lemma, in seq]
has_pred1 [lemma, in seq]
has_non_scalar_mxP [lemma, in mxalgebra]
has_sym [lemma, in seq]
has_predU [lemma, in seq]
has_predC [lemma, in seq]
has_prim_root [lemma, in cyclic]
has_Frobenius_action [inductive, in frobenius]
has_nthP [lemma, in seq]
has_pred0 [lemma, in seq]
has_cat [lemma, in seq]
has_map [lemma, in seq]
has_mask_cons [lemma, in seq]
has_count [lemma, in seq]
has_seq1 [lemma, in seq]
has_seqb [lemma, in seq]
has_rcons [lemma, in seq]
has_mxring_id [definition, in mxalgebra]
has_predT [lemma, in seq]
has_find [lemma, in seq]
head [definition, in seq]
headI [lemma, in seq]
head_coef_mul [lemma, in poly]
Hf [definition, in fingraph]
holds [abbreviation, in mxrepresentation]
homg [definition, in morphism]
Homg [section, in morphism]
homgP [lemma, in morphism]
homGrp_trans [lemma, in presentation]
homg_refl [lemma, in morphism]
homg_trans [lemma, in morphism]
homg_quotientS [lemma, in quotient]
homocyclic [definition, in abelian]
homocyclic_Ohm_Mho [lemma, in abelian]
hom_mxsemisimple [lemma, in mxrepresentation]
hom_mxmodule [lemma, in mxrepresentation]
hom_is_linear [lemma, in vector]
hom_component_mx [lemma, in mxrepresentation]
hom_envelop_mxC [lemma, in mxrepresentation]
hom_cyclic_mx [lemma, in mxrepresentation]
hom_mxP [lemma, in mxrepresentation]
hom_component_mx_iso [lemma, in mxrepresentation]
hom_mxsemisimple_iso [lemma, in mxrepresentation]
hom_linear [definition, in vector]
Hom_G [abbreviation, in mxrepresentation]
horner [definition, in poly]
hornerC [lemma, in poly]
HornerMx [section, in mxpoly]
HornerMx.A [variable, in mxpoly]
HornerMx.n' [variable, in mxpoly]
HornerMx.R [variable, in mxpoly]
hornerX [lemma, in poly]
hornerXn [lemma, in poly]
horner_lin [definition, in poly]
horner_sum [lemma, in poly]
horner_amulX [lemma, in poly]
horner_mx_X [lemma, in mxpoly]
horner_rmorphism [definition, in poly]
horner_additive [definition, in poly]
horner_mx [definition, in mxpoly]
horner_exp_com [lemma, in poly]
horner_exp [lemma, in poly]
horner_rVpolyK [lemma, in mxpoly]
horner_mul_com [lemma, in poly]
horner_morphX [lemma, in poly]
horner_coef_wide [lemma, in poly]
horner_is_rmorphism [lemma, in poly]
horner_cons [lemma, in poly]
horner_mxZ [lemma, in mxpoly]
horner_coef [lemma, in poly]
horner_mx_mem [lemma, in mxpoly]
horner_add [lemma, in poly]
horner_mulX [lemma, in poly]
horner_opp [lemma, in poly]
horner_mul [lemma, in poly]
horner_Poly [lemma, in poly]
horner_prod [lemma, in poly]
horner_lin_com [definition, in poly]
horner_scaler [lemma, in poly]
horner_poly [lemma, in poly]
horner_morph [definition, in poly]
horner_mxK [lemma, in mxpoly]
horner_mulrn [lemma, in poly]
horner_morphC [lemma, in poly]
horner_map [lemma, in poly]
horner_Cmul [lemma, in poly]
horner_poly_comp [lemma, in poly]
horner_mx_lrmorphism [definition, in mxpoly]
horner_mx_linear [definition, in mxpoly]
horner_mx_rmorphism [definition, in mxpoly]
horner_mx_additive [definition, in mxpoly]
horner_rVpoly_inj [lemma, in mxpoly]
horner_mx_C [lemma, in mxpoly]
horner_rVpoly [lemma, in mxpoly]
horner0 [lemma, in poly]
hsubmxK [lemma, in matrix]
H_g_rcosets [definition, in finmodule]



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)