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 (75489 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 (1813 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 (45320 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 (382 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 (3967 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 (14046 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 (469 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 (128 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 (457 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 (1372 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 (1025 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 (6124 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 (250 entries)

H (lemma)

halfD [in mathcomp.ssreflect.ssrnat]
half_gt0 [in mathcomp.ssreflect.ssrnat]
half_leq [in mathcomp.ssreflect.ssrnat]
half_bit_double [in mathcomp.ssreflect.ssrnat]
HallJ [in mathcomp.solvable.pgroup]
HallP [in mathcomp.solvable.pgroup]
Hall_Witt_identity [in mathcomp.solvable.commutator]
Hall_setI_normal [in mathcomp.solvable.sylow]
Hall_psubJ [in mathcomp.solvable.sylow]
Hall_pJsub [in mathcomp.solvable.sylow]
Hall_max [in mathcomp.solvable.pgroup]
Hall_pi [in mathcomp.solvable.pgroup]
Hall_Frattini_arg [in mathcomp.solvable.hall]
Hall_Jsub [in mathcomp.solvable.hall]
Hall_subJ [in mathcomp.solvable.hall]
Hall_superset [in mathcomp.solvable.hall]
Hall_trans [in mathcomp.solvable.hall]
Hall_exists [in mathcomp.solvable.hall]
Hall_exists_subJ [in mathcomp.solvable.hall]
Hall1 [in mathcomp.solvable.pgroup]
hasNfind [in mathcomp.ssreflect.seq]
hasP [in mathcomp.ssreflect.seq]
hasPn [in mathcomp.ssreflect.seq]
hasPP [in mathcomp.ssreflect.seq]
has_tnthP [in mathcomp.ssreflect.tuple]
has_map [in mathcomp.ssreflect.seq]
has_mask [in mathcomp.ssreflect.seq]
has_mask_cons [in mathcomp.ssreflect.seq]
has_rotr [in mathcomp.ssreflect.seq]
has_nthP [in mathcomp.ssreflect.seq]
has_pred1 [in mathcomp.ssreflect.seq]
has_sym [in mathcomp.ssreflect.seq]
has_filter [in mathcomp.ssreflect.seq]
has_rev [in mathcomp.ssreflect.seq]
has_rot [in mathcomp.ssreflect.seq]
has_take_leq [in mathcomp.ssreflect.seq]
has_take [in mathcomp.ssreflect.seq]
has_predU [in mathcomp.ssreflect.seq]
has_predC [in mathcomp.ssreflect.seq]
has_predT [in mathcomp.ssreflect.seq]
has_pred0 [in mathcomp.ssreflect.seq]
has_rcons [in mathcomp.ssreflect.seq]
has_cat [in mathcomp.ssreflect.seq]
has_seqb [in mathcomp.ssreflect.seq]
has_nseq [in mathcomp.ssreflect.seq]
has_seq1 [in mathcomp.ssreflect.seq]
has_nil [in mathcomp.ssreflect.seq]
has_find [in mathcomp.ssreflect.seq]
has_count [in mathcomp.ssreflect.seq]
has_prim_root [in mathcomp.solvable.cyclic]
has_nonprincipal_irr [in mathcomp.character.character]
has_algid1 [in mathcomp.field.falgebra]
has_algidP [in mathcomp.field.falgebra]
has_non_scalar_mxP [in mathcomp.algebra.mxalgebra]
headI [in mathcomp.ssreflect.seq]
Hilbert's_theorem_90 [in mathcomp.field.galois]
homgP [in mathcomp.fingroup.morphism]
homGrp_trans [in mathcomp.fingroup.presentation]
homg_quotientS [in mathcomp.fingroup.quotient]
homg_trans [in mathcomp.fingroup.morphism]
homg_refl [in mathcomp.fingroup.morphism]
homocyclic_Ohm_Mho [in mathcomp.solvable.abelian]
homocyclic1 [in mathcomp.solvable.abelian]
homoLR_in [in mathcomp.ssreflect.ssrbool]
homoRL_in [in mathcomp.ssreflect.ssrbool]
homoW [in mathcomp.ssreflect.eqtype]
homoW_in [in mathcomp.ssreflect.eqtype]
homo_leq [in mathcomp.ssreflect.ssrnat]
homo_leq_in [in mathcomp.ssreflect.ssrnat]
homo_ltn [in mathcomp.ssreflect.ssrnat]
homo_ltn_in [in mathcomp.ssreflect.ssrnat]
homo_sort_map_in [in mathcomp.ssreflect.path]
homo_sort_map [in mathcomp.ssreflect.path]
homo_sorted [in mathcomp.ssreflect.path]
homo_cycle [in mathcomp.ssreflect.path]
homo_path [in mathcomp.ssreflect.path]
homo_sorted_in [in mathcomp.ssreflect.path]
homo_cycle_in [in mathcomp.ssreflect.path]
homo_path_in [in mathcomp.ssreflect.path]
homo_mono_in [in mathcomp.ssreflect.ssrbool]
homo_sym_in11 [in mathcomp.ssreflect.ssrbool]
homo_sym_in [in mathcomp.ssreflect.ssrbool]
homo_sym [in mathcomp.ssreflect.ssrbool]
hom_component_mx [in mathcomp.character.mxrepresentation]
hom_component_mx_iso [in mathcomp.character.mxrepresentation]
hom_mxsemisimple_iso [in mathcomp.character.mxrepresentation]
hom_mxsemisimple [in mathcomp.character.mxrepresentation]
hom_cyclic_mx [in mathcomp.character.mxrepresentation]
hom_mxmodule [in mathcomp.character.mxrepresentation]
hom_envelop_mxC [in mathcomp.character.mxrepresentation]
hom_mxP [in mathcomp.character.mxrepresentation]
hornerC [in mathcomp.algebra.poly]
hornerCM [in mathcomp.algebra.poly]
hornerD [in mathcomp.algebra.poly]
hornerM [in mathcomp.algebra.poly]
hornerMn [in mathcomp.algebra.poly]
hornerMX [in mathcomp.algebra.poly]
hornerMXaddC [in mathcomp.algebra.poly]
hornerMz [in mathcomp.algebra.ssrint]
hornerM_comm [in mathcomp.algebra.poly]
hornerN [in mathcomp.algebra.poly]
hornerX [in mathcomp.algebra.poly]
hornerXn [in mathcomp.algebra.poly]
hornerXsubC [in mathcomp.algebra.poly]
hornerZ [in mathcomp.algebra.poly]
horner_mx_uconjC [in mathcomp.algebra.mxpoly]
horner_mx_uconj [in mathcomp.algebra.mxpoly]
horner_mx_conj [in mathcomp.algebra.mxpoly]
horner_rVpoly_inj [in mathcomp.algebra.mxpoly]
horner_mxK [in mathcomp.algebra.mxpoly]
horner_rVpolyK [in mathcomp.algebra.mxpoly]
horner_mx_mem [in mathcomp.algebra.mxpoly]
horner_mx_stable [in mathcomp.algebra.mxpoly]
horner_mx_diag [in mathcomp.algebra.mxpoly]
horner_rVpoly [in mathcomp.algebra.mxpoly]
horner_mxZ [in mathcomp.algebra.mxpoly]
horner_mx_X [in mathcomp.algebra.mxpoly]
horner_mx_C [in mathcomp.algebra.mxpoly]
horner_int [in mathcomp.algebra.ssrint]
horner_poly_XmY [in mathcomp.algebra.polyXY]
horner_poly_XaY [in mathcomp.algebra.polyXY]
horner_polyC [in mathcomp.algebra.polyXY]
horner_swapXY [in mathcomp.algebra.polyXY]
horner_comp [in mathcomp.algebra.poly]
horner_alg_is_lrmorphism [in mathcomp.algebra.poly]
horner_algX [in mathcomp.algebra.poly]
horner_algC [in mathcomp.algebra.poly]
horner_eval_is_lrmorphism [in mathcomp.algebra.poly]
horner_evalE [in mathcomp.algebra.poly]
horner_prod [in mathcomp.algebra.poly]
horner_exp [in mathcomp.algebra.poly]
horner_is_lrmorphism [in mathcomp.algebra.poly]
horner_morphX [in mathcomp.algebra.poly]
horner_morphC [in mathcomp.algebra.poly]
horner_map [in mathcomp.algebra.poly]
horner_exp_comm [in mathcomp.algebra.poly]
horner_sum [in mathcomp.algebra.poly]
horner_poly [in mathcomp.algebra.poly]
horner_coef_wide [in mathcomp.algebra.poly]
horner_coef [in mathcomp.algebra.poly]
horner_Poly [in mathcomp.algebra.poly]
horner_coef0 [in mathcomp.algebra.poly]
horner_cons [in mathcomp.algebra.poly]
horner0 [in mathcomp.algebra.poly]
horner2_swapXY [in mathcomp.algebra.polyXY]
hsubmxK [in mathcomp.algebra.matrix]



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 (75489 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 (1813 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 (45320 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 (382 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 (3967 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 (14046 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 (469 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 (128 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 (457 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 (1372 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 (1025 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 (6124 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 (250 entries)