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)
Hahn_decomposition [prf, in mathcomp.analysis.charge]hahn_decomposition_lemma [prf, in mathcomp.analysis.charge]
Hahn_decomposition_uniq [prf, in mathcomp.analysis.charge]
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]
harmonic_ge0 [prf, in mathcomp.analysis.sequences]
harmonic_gt0 [prf, in mathcomp.analysis.sequences]
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_inf0 [prf, in mathcomp.classical.classical_sets]
has_inf1 [prf, in mathcomp.classical.classical_sets]
has_inf_half [prf, in mathcomp.reals.real_interval]
has_inf_supN [prf, in mathcomp.reals.reals]
has_infPn [prf, in mathcomp.reals.reals]
has_lb_ubN [prf, in mathcomp.classical.set_interval]
has_lbound0 [prf, in mathcomp.reals.reals]
has_lbound_itv [prf, in mathcomp.classical.set_interval]
has_lbound_sdrop [prf, in mathcomp.analysis.sequences]
has_lbPn [prf, in mathcomp.classical.set_interval]
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_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_sup0 [prf, in mathcomp.classical.classical_sets]
has_sup1 [prf, in mathcomp.classical.classical_sets]
has_sup_down [prf, in mathcomp.reals.reals]
has_sup_floor_set [prf, in mathcomp.reals.reals]
has_sup_half [prf, in mathcomp.reals.real_interval]
has_supPn [prf, in mathcomp.reals.reals]
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_ub_image_norm [prf, in mathcomp.reals.reals]
has_ub_lbN [prf, in mathcomp.reals.reals]
has_ub_set1 [prf, in mathcomp.classical.classical_sets]
has_ubound0 [prf, in mathcomp.reals.reals]
has_ubound_itv [prf, in mathcomp.classical.set_interval]
has_ubound_sdrop [prf, in mathcomp.analysis.sequences]
has_ubPn [prf, in mathcomp.classical.set_interval]
has_undup [prf, in mathcomp.boot.seq]
hasNfind [prf, in mathcomp.boot.seq]
hasNlbound_itv [prf, in mathcomp.classical.set_interval]
hasNub_ereal_sup [prf, in mathcomp.analysis.ereal]
hasNubound_itv [prf, in mathcomp.classical.set_interval]
hasP [prf, in mathcomp.boot.seq]
hasPn [prf, in mathcomp.boot.seq]
hasPP [prf, in mathcomp.boot.seq]
hausdorff_accessible [prf, in mathcomp.analysis.topology_theory.separation_axioms]
Hausdorff_maximal_principle [prf, in mathcomp.classical.wochoice]
hausdorff_product [prf, in mathcomp.analysis.topology_theory.function_spaces]
hausdorrf_close_eq_in [prf, in mathcomp.analysis.topology_theory.function_spaces]
have_near [prf, in mathcomp.classical.filter]
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]
HL_maximal_ge0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
HL_maximalT_ge0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
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]
hoelder [prf, in mathcomp.analysis.hoelder]
hoelder2 [prf, in mathcomp.analysis.hoelder]
hoelder_conj_ge1 [prf, in mathcomp.analysis.hoelder]
hoelder_conjugate0 [prf, in mathcomp.analysis.hoelder]
hoelder_conjugate1 [prf, in mathcomp.analysis.hoelder]
hoelder_conjugate2 [prf, in mathcomp.analysis.hoelder]
hoelder_conjugate_div [prf, in mathcomp.analysis.hoelder]
hoelder_conjugate_eq1 [prf, in mathcomp.analysis.hoelder]
hoelder_conjugate_eqNy [prf, in mathcomp.analysis.hoelder]
hoelder_conjugate_eqy [prf, in mathcomp.analysis.hoelder]
hoelder_conjugateK [prf, in mathcomp.analysis.hoelder]
hoelder_conjugateNy [prf, in mathcomp.analysis.hoelder]
hoelder_conjugateP [prf, in mathcomp.analysis.hoelder]
hoelder_conjugatey [prf, in mathcomp.analysis.hoelder]
hoelder_div_conjugate [prf, in mathcomp.analysis.hoelder]
hoelder_Mconjugate [prf, in mathcomp.analysis.hoelder]
homeomorphism_cantor_like [prf, in mathcomp.analysis.cantor]
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_setP [prf, in mathcomp.classical.classical_sets]
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]
horner0_ext [prf, in mathcomp.analysis.derive]
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_scale_ext [prf, in mathcomp.analysis.derive]
horner_sum [prf, in mathcomp.algebra.poly]
horner_swapXY [prf, in mathcomp.algebra.polyXY]
hornerC [prf, in mathcomp.algebra.poly]
hornerC_ext [prf, in mathcomp.analysis.derive]
hornerCM [prf, in mathcomp.algebra.poly]
hornerD [prf, in mathcomp.algebra.poly]
hornerD_ext [prf, in mathcomp.analysis.derive]
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]