H (Lemmas)
| 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 |
H (Lemmas)
half_bit_double [prf, in mathcomp.boot.ssrnat]half_gt0 [prf, in mathcomp.boot.ssrnat]
half_leq [prf, in mathcomp.boot.ssrnat]
halfD [prf, in mathcomp.boot.ssrnat]
halfK [prf, in mathcomp.boot.ssrnat]
Hall1 [prf, in mathcomp.solvable.pgroup]
Hall_exists [prf, in mathcomp.solvable.hall]
Hall_exists_subJ [prf, in mathcomp.solvable.hall]
Hall_Frattini_arg [prf, in mathcomp.solvable.hall]
Hall_Jsub [prf, in mathcomp.solvable.hall]
Hall_max [prf, in mathcomp.solvable.pgroup]
Hall_pi [prf, in mathcomp.solvable.pgroup]
Hall_pJsub [prf, in mathcomp.solvable.sylow]
Hall_psubJ [prf, in mathcomp.solvable.sylow]
Hall_setI_normal [prf, in mathcomp.solvable.sylow]
Hall_subJ [prf, in mathcomp.solvable.hall]
Hall_superset [prf, in mathcomp.solvable.hall]
Hall_trans [prf, in mathcomp.solvable.hall]
Hall_Witt_identity [prf, in mathcomp.solvable.commutator]
HallJ [prf, in mathcomp.solvable.pgroup]
HallP [prf, in mathcomp.solvable.pgroup]
has_algid1 [prf, in mathcomp.field.falgebra]
has_algidP [prf, in mathcomp.field.falgebra]
has_cat [prf, in mathcomp.boot.seq]
has_count [prf, in mathcomp.boot.seq]
has_filter [prf, in mathcomp.boot.seq]
has_find [prf, in mathcomp.boot.seq]
has_map [prf, in mathcomp.boot.seq]
has_mask [prf, in mathcomp.boot.seq]
has_mask_cons [prf, in mathcomp.boot.seq]
has_nil [prf, in mathcomp.boot.seq]
has_non_scalar_mxP [prf, in mathcomp.algebra.mxalgebra]
has_nonprincipal_irr [prf, in mathcomp.group_representation.character]
has_nseq [prf, in mathcomp.boot.seq]
has_nthP [prf, in mathcomp.boot.seq]
has_pred0 [prf, in mathcomp.boot.seq]
has_pred1 [prf, in mathcomp.boot.seq]
has_predC [prf, in mathcomp.boot.seq]
has_predT [prf, in mathcomp.boot.seq]
has_predU [prf, in mathcomp.boot.seq]
has_prim_root [prf, in mathcomp.solvable.cyclic]
has_rcons [prf, in mathcomp.boot.seq]
has_rev [prf, in mathcomp.boot.seq]
has_rot [prf, in mathcomp.boot.seq]
has_rotr [prf, in mathcomp.boot.seq]
has_seq1 [prf, in mathcomp.boot.seq]
has_seqb [prf, in mathcomp.boot.seq]
has_set1 [prf, in mathcomp.boot.finset]
has_setU [prf, in mathcomp.boot.finset]
has_sym [prf, in mathcomp.boot.seq]
has_take [prf, in mathcomp.boot.seq]
has_take_leq [prf, in mathcomp.boot.seq]
has_tnthP [prf, in mathcomp.boot.tuple]
has_undup [prf, in mathcomp.boot.seq]
hasNfind [prf, in mathcomp.boot.seq]
hasP [prf, in mathcomp.boot.seq]
hasPn [prf, in mathcomp.boot.seq]
hasPP [prf, in mathcomp.boot.seq]
headI [prf, in mathcomp.boot.seq]
herm_eq0C [prf, in mathcomp.algebra.sesquilinear]
hermC [prf, in mathcomp.algebra.sesquilinear]
hermitian_normalmx [prf, in mathcomp.algebra.spectral]
hermitian_spectral_diag_real [prf, in mathcomp.algebra.spectral]
hermitianmx_key [prf, in mathcomp.algebra.sesquilinear]
hermitianmxE [prf, in mathcomp.algebra.sesquilinear]
hermmx_eq0P [prf, in mathcomp.algebra.sesquilinear]
Hilbert's_theorem_90 [prf, in mathcomp.field.galois]
hnorm_sign [prf, in mathcomp.algebra.sesquilinear]
hnormB [prf, in mathcomp.algebra.sesquilinear]
hnormBd [prf, in mathcomp.algebra.sesquilinear]
hnormD [prf, in mathcomp.algebra.sesquilinear]
hnormDd [prf, in mathcomp.algebra.sesquilinear]
hnormN [prf, in mathcomp.algebra.sesquilinear]
hom_component_mx [prf, in mathcomp.group_representation.mxrepresentation]
hom_component_mx_iso [prf, in mathcomp.group_representation.mxrepresentation]
hom_cyclic_mx [prf, in mathcomp.group_representation.mxrepresentation]
hom_envelop_mxC [prf, in mathcomp.group_representation.mxrepresentation]
hom_mxmodule [prf, in mathcomp.group_representation.mxrepresentation]
hom_mxP [prf, in mathcomp.group_representation.mxrepresentation]
hom_mxsemisimple [prf, in mathcomp.group_representation.mxrepresentation]
hom_mxsemisimple_iso [prf, in mathcomp.group_representation.mxrepresentation]
homg_quotientS [prf, in mathcomp.finite_group.quotient]
homg_refl [prf, in mathcomp.finite_group.morphism]
homg_trans [prf, in mathcomp.finite_group.morphism]
homgP [prf, in mathcomp.finite_group.morphism]
homGrp_trans [prf, in mathcomp.finite_group.presentation]
homo_cycle [prf, in mathcomp.boot.path]
homo_cycle_in [prf, in mathcomp.boot.path]
homo_leq [prf, in mathcomp.boot.ssrnat]
homo_leq_in [prf, in mathcomp.boot.ssrnat]
homo_ltn [prf, in mathcomp.boot.ssrnat]
homo_ltn_in [prf, in mathcomp.boot.ssrnat]
homo_mono1 [prf, in mathcomp.boot.ssrbool]
homo_path [prf, in mathcomp.boot.path]
homo_path_in [prf, in mathcomp.boot.path]
homo_sort_map [prf, in mathcomp.boot.path]
homo_sort_map_in [prf, in mathcomp.boot.path]
homo_sorted [prf, in mathcomp.boot.path]
homo_sorted_in [prf, in mathcomp.boot.path]
homocyclic1 [prf, in mathcomp.solvable.abelian]
homocyclic_Ohm_Mho [prf, in mathcomp.solvable.abelian]
homoW [prf, in mathcomp.boot.eqtype]
homoW_in [prf, in mathcomp.boot.eqtype]
horner0 [prf, in mathcomp.algebra.poly]
horner2_swapXY [prf, in mathcomp.algebra.polyXY]
horner_algC [prf, in mathcomp.algebra.poly]
horner_algX [prf, in mathcomp.algebra.poly]
horner_coef [prf, in mathcomp.algebra.poly]
horner_coef0 [prf, in mathcomp.algebra.poly]
horner_coef_wide [prf, in mathcomp.algebra.poly]
horner_comp [prf, in mathcomp.algebra.poly]
horner_cons [prf, in mathcomp.algebra.poly]
horner_eval_is_linear [prf, in mathcomp.algebra.poly]
horner_eval_is_monoid_morphism [prf, in mathcomp.algebra.poly]
horner_evalE [prf, in mathcomp.algebra.poly]
horner_exp [prf, in mathcomp.algebra.poly]
horner_exp_comm [prf, in mathcomp.algebra.poly]
horner_int [prf, in mathcomp.algebra.ssrint]
horner_is_linear [prf, in mathcomp.algebra.poly]
horner_is_monoid_morphism [prf, in mathcomp.algebra.poly]
horner_is_semilinear [prf, in mathcomp.algebra.poly]
horner_map [prf, in mathcomp.algebra.poly]
horner_morphC [prf, in mathcomp.algebra.poly]
horner_morphX [prf, in mathcomp.algebra.poly]
horner_mx_C [prf, in mathcomp.algebra.mxpoly]
horner_mx_conj [prf, in mathcomp.algebra.mxred]
horner_mx_conj [prf, in mathcomp.algebra.mxpoly]
horner_mx_diag [prf, in mathcomp.algebra.mxpoly]
horner_mx_mem [prf, in mathcomp.algebra.mxpoly]
horner_mx_stable [prf, in mathcomp.algebra.mxpoly]
horner_mx_uconj [prf, in mathcomp.algebra.mxred]
horner_mx_uconj [prf, in mathcomp.algebra.mxpoly]
horner_mx_uconjC [prf, in mathcomp.algebra.mxred]
horner_mx_uconjC [prf, in mathcomp.algebra.mxpoly]
horner_mx_X [prf, in mathcomp.algebra.mxpoly]
horner_mxK [prf, in mathcomp.algebra.mxpoly]
horner_mxZ [prf, in mathcomp.algebra.mxpoly]
horner_poly [prf, in mathcomp.algebra.poly]
horner_Poly [prf, in mathcomp.algebra.poly]
horner_poly_XaY [prf, in mathcomp.algebra.polyXY]
horner_poly_XmY [prf, in mathcomp.algebra.polyXY]
horner_polyC [prf, in mathcomp.algebra.polyXY]
horner_prod [prf, in mathcomp.algebra.poly]
horner_rVpoly [prf, in mathcomp.algebra.mxpoly]
horner_rVpoly_inj [prf, in mathcomp.algebra.mxpoly]
horner_rVpolyK [prf, in mathcomp.algebra.mxpoly]
horner_sum [prf, in mathcomp.algebra.poly]
horner_swapXY [prf, in mathcomp.algebra.polyXY]
hornerC [prf, in mathcomp.algebra.poly]
hornerCM [prf, in mathcomp.algebra.poly]
hornerD [prf, in mathcomp.algebra.poly]
hornerM [prf, in mathcomp.algebra.poly]
hornerM_comm [prf, in mathcomp.algebra.poly]
hornerMn [prf, in mathcomp.algebra.poly]
hornerMX [prf, in mathcomp.algebra.poly]
hornerMXaddC [prf, in mathcomp.algebra.poly]
hornerMz [prf, in mathcomp.algebra.ssrint]
hornerN [prf, in mathcomp.algebra.poly]
hornerX [prf, in mathcomp.algebra.poly]
hornerXn [prf, in mathcomp.algebra.poly]
hornerXsubC [prf, in mathcomp.algebra.poly]
hornerZ [prf, in mathcomp.algebra.poly]
hsubmxK [prf, in mathcomp.algebra.matrix]