H (Global Index)
| 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
H [abbrev, in mathcomp.finite_group.quotient]Hahn_decomposition [prf, in mathcomp.analysis.charge]
hahn_decomposition [def, in mathcomp.analysis.charge]
hahn_decomposition_lemma [prf, in mathcomp.analysis.charge]
Hahn_decomposition_uniq [prf, in mathcomp.analysis.charge]
half [def, in mathcomp.boot.ssrnat]
half_bit_double [prf, in mathcomp.boot.ssrnat]
half_double [def, 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]
hall [file, in mathcomp.solvable.hall]
Hall [def, in mathcomp.solvable.pgroup]
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 [def, in mathcomp.analysis.sequences]
harmonic_ge0 [prf, in mathcomp.analysis.sequences]
harmonic_gt0 [prf, in mathcomp.analysis.sequences]
harmonic_mean [def, in mathcomp.analysis.sequences]
has [def, in mathcomp.boot.seq]
has_algid [def, in mathcomp.field.falgebra]
has_algid1 [prf, in mathcomp.field.falgebra]
has_algidP [prf, in mathcomp.field.falgebra]
has_cat [prf, in mathcomp.boot.seq]
has_char0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
has_count [prf, in mathcomp.boot.seq]
has_filter [prf, in mathcomp.boot.seq]
has_find [prf, in mathcomp.boot.seq]
has_Frobenius_action [ind, in mathcomp.solvable.frobenius]
has_inf [def, in mathcomp.classical.classical_sets]
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_lbound [def, in mathcomp.classical.classical_sets]
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_mxring_id [def, in mathcomp.algebra.mxalgebra]
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_pchar0 [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
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_sup [def, in mathcomp.classical.classical_sets]
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_ubound [def, 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]
hasChoice [abbrev, in mathcomp.boot.choice]
hasChoice [mod, in mathcomp.boot.choice]
hasChoice.axioms [abbrev, in mathcomp.boot.choice]
hasChoice.axioms_ [rec, in mathcomp.boot.choice]
hasChoice.Build [abbrev, in mathcomp.boot.choice]
hasChoice.choice_complete_subdef [proj, in mathcomp.boot.choice]
hasChoice.choice_correct_subdef [proj, in mathcomp.boot.choice]
hasChoice.choice_extensional_subdef [proj, in mathcomp.boot.choice]
hasChoice.Exports [mod, in mathcomp.boot.choice]
hasChoice.find_subdef [proj, in mathcomp.boot.choice]
hasChoice.identity_builder [def, in mathcomp.boot.choice]
hasChoice.phant_axioms [def, in mathcomp.boot.choice]
hasChoice.phant_Build [def, in mathcomp.boot.choice]
hasDecEq [abbrev, in mathcomp.boot.eqtype]
hasDecEq [mod, in mathcomp.boot.eqtype]
hasDecEq.axioms [abbrev, in mathcomp.boot.eqtype]
hasDecEq.axioms_ [rec, in mathcomp.boot.eqtype]
hasDecEq.Build [abbrev, in mathcomp.boot.eqtype]
hasDecEq.eq_op [proj, in mathcomp.boot.eqtype]
hasDecEq.eqP [proj, in mathcomp.boot.eqtype]
hasDecEq.Exports [mod, in mathcomp.boot.eqtype]
hasDecEq.identity_builder [def, in mathcomp.boot.eqtype]
hasDecEq.phant_axioms [def, in mathcomp.boot.eqtype]
hasDecEq.phant_Build [def, in mathcomp.boot.eqtype]
hasFrobeniusAction [constr, in mathcomp.solvable.frobenius]
hasInv [abbrev, in mathcomp.boot.monoid]
hasInv [mod, in mathcomp.boot.monoid]
hasInv.axioms [abbrev, in mathcomp.boot.monoid]
hasInv.axioms_ [rec, in mathcomp.boot.monoid]
hasInv.Build [abbrev, in mathcomp.boot.monoid]
hasInv.Exports [mod, in mathcomp.boot.monoid]
hasInv.identity_builder [def, in mathcomp.boot.monoid]
hasInv.inv [proj, in mathcomp.boot.monoid]
hasInv.phant_axioms [def, in mathcomp.boot.monoid]
hasInv.phant_Build [def, in mathcomp.boot.monoid]
hasMeasurableCountableUnion [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion [mod, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion.axioms [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion.axioms_ [rec, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion.bigcupT_measurable [proj, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion.Build [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion.Exports [mod, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion.identity_builder [def, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion.phant_axioms [def, in mathcomp.analysis.measure_theory.measurable_structure]
hasMeasurableCountableUnion.phant_Build [def, in mathcomp.analysis.measure_theory.measurable_structure]
hasMul [abbrev, in mathcomp.boot.monoid]
hasMul [mod, in mathcomp.boot.monoid]
hasMul.axioms [abbrev, in mathcomp.boot.monoid]
hasMul.axioms_ [rec, in mathcomp.boot.monoid]
hasMul.Build [abbrev, in mathcomp.boot.monoid]
hasMul.Exports [mod, in mathcomp.boot.monoid]
hasMul.identity_builder [def, in mathcomp.boot.monoid]
hasMul.mul [proj, in mathcomp.boot.monoid]
hasMul.phant_axioms [def, in mathcomp.boot.monoid]
hasMul.phant_Build [def, in mathcomp.boot.monoid]
hasNbhs [abbrev, in mathcomp.classical.filter]
hasNbhs [mod, in mathcomp.classical.filter]
hasNbhs.axioms [abbrev, in mathcomp.classical.filter]
hasNbhs.axioms_ [rec, in mathcomp.classical.filter]
hasNbhs.Build [abbrev, in mathcomp.classical.filter]
hasNbhs.Exports [mod, in mathcomp.classical.filter]
hasNbhs.nbhs [proj, in mathcomp.classical.filter]
hasNbhs.phant_axioms [def, in mathcomp.classical.filter]
hasNbhs.phant_Build [def, in mathcomp.classical.filter]
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]
hasOne [abbrev, in mathcomp.boot.monoid]
hasOne [mod, in mathcomp.boot.monoid]
hasOne.axioms [abbrev, in mathcomp.boot.monoid]
hasOne.axioms_ [rec, in mathcomp.boot.monoid]
hasOne.Build [abbrev, in mathcomp.boot.monoid]
hasOne.Exports [mod, in mathcomp.boot.monoid]
hasOne.identity_builder [def, in mathcomp.boot.monoid]
hasOne.one [proj, in mathcomp.boot.monoid]
hasOne.phant_axioms [def, in mathcomp.boot.monoid]
hasOne.phant_Build [def, in mathcomp.boot.monoid]
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]
hausdorff_space [def, in mathcomp.analysis.topology_theory.separation_axioms]
hausdorrf_close_eq_in [prf, in mathcomp.analysis.topology_theory.function_spaces]
have_near [prf, in mathcomp.classical.filter]
HBNNSimple [mod, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun [mod, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.axioms_ [rec, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.cardinality_FiniteImage_mixin [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.class [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.clone [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.copy [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.Exports [mod, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.Exports.join_HBNNSimple_NonNegSimpleFun_between_cardinality_FImFun_and_numfun_NonNegFun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.Exports.join_HBNNSimple_NonNegSimpleFun_between_measurable_function_MeasurableFun_and_numfun_NonNegFun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.Exports.join_HBNNSimple_NonNegSimpleFun_between_numfun_NonNegFun_and_HBSimple_SimpleFun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.measurable_function_isMeasurableFun_mixin [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.numfun_isNonNegFun_mixin [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.on [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.on_ [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.pack_ [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.phant_clone [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.phant_on_ [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.sort [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFun.type [rec, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBNNSimple.NonNegSimpleFunElpiOperations [mod, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple [mod, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun [mod, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.axioms_ [rec, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.cardinality_FiniteImage_mixin [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.class [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.clone [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.copy [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.Exports [mod, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.Exports.join_HBSimple_SimpleFun_between_cardinality_FImFun_and_measurable_function_MeasurableFun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.measurable_function_isMeasurableFun_mixin [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.on [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.on_ [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.pack_ [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.phant_clone [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.phant_on_ [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.sort [proj, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFun.type [rec, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
HBSimple.SimpleFunElpiOperations [mod, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
head [def, in mathcomp.boot.seq]
headI [prf, in mathcomp.boot.seq]
herm_eq0C [prf, in mathcomp.algebra.sesquilinear]
hermC [prf, in mathcomp.algebra.sesquilinear]
hermitian [abbrev, in mathcomp.algebra.sesquilinear]
Hermitian [abbrev, in mathcomp.algebra.sesquilinear]
Hermitian [mod, in mathcomp.algebra.sesquilinear]
Hermitian.axioms_ [rec, in mathcomp.algebra.sesquilinear]
Hermitian.class [proj, in mathcomp.algebra.sesquilinear]
Hermitian.clone [abbrev, in mathcomp.algebra.sesquilinear]
Hermitian.copy [abbrev, in mathcomp.algebra.sesquilinear]
Hermitian.Exports [mod, in mathcomp.algebra.sesquilinear]
Hermitian.on [abbrev, in mathcomp.algebra.sesquilinear]
Hermitian.on_ [abbrev, in mathcomp.algebra.sesquilinear]
Hermitian.pack_ [def, in mathcomp.algebra.sesquilinear]
Hermitian.phant_clone [def, in mathcomp.algebra.sesquilinear]
Hermitian.phant_on_ [def, in mathcomp.algebra.sesquilinear]
Hermitian.sesquilinear_isBilinear_mixin [proj, in mathcomp.algebra.sesquilinear]
Hermitian.sesquilinear_isHermitianSesquilinear_mixin [proj, in mathcomp.algebra.sesquilinear]
Hermitian.sort [proj, in mathcomp.algebra.sesquilinear]
Hermitian.type [rec, in mathcomp.algebra.sesquilinear]
hermitian1mx [def, in mathcomp.algebra.sesquilinear]
hermitian_matrix [rec, in mathcomp.algebra.sesquilinear]
hermitian_normalmx [prf, in mathcomp.algebra.spectral]
hermitian_spectral_diag_real [prf, in mathcomp.algebra.spectral]
HermitianElpiOperations [mod, in mathcomp.algebra.sesquilinear]
hermitianmx [def, in mathcomp.algebra.sesquilinear]
hermitianmx_key [prf, in mathcomp.algebra.sesquilinear]
hermitianmx_keyed [def, in mathcomp.algebra.sesquilinear]
hermitianmxE [prf, in mathcomp.algebra.sesquilinear]
hermmx_eq0P [prf, in mathcomp.algebra.sesquilinear]
hermsymmx [abbrev, in mathcomp.algebra.sesquilinear]
HG [abbrev, in mathcomp.solvable.finmodule]
hide [def, in mathcomp.boot.ssreflect]
hideT [abbrev, in mathcomp.boot.ssreflect]
Hilbert's_theorem_90 [prf, in mathcomp.field.galois]
HL [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
HL_maximal [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
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]
hlength [abbrev, in mathcomp.analysis.lebesgue_measure]
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 [file, in mathcomp.analysis.hoelder]
hoelder [prf, in mathcomp.analysis.hoelder]
hoelder2 [prf, in mathcomp.analysis.hoelder]
hoelder_conj_ge1 [prf, in mathcomp.analysis.hoelder]
hoelder_conjugate [def, 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]
Hom [constr, in mathcomp.algebra.vector]
hom [ind, in mathcomp.algebra.vector]
hom_ind [scheme, in mathcomp.algebra.vector]
hom_rec [scheme, in mathcomp.algebra.vector]
hom_rect [scheme, in mathcomp.algebra.vector]
hom_sind [scheme, in mathcomp.algebra.vector]
homeomorphism_cantor_like [prf, in mathcomp.analysis.cantor]
homg [def, in mathcomp.finite_group.morphism]
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]
homocyclic [def, in mathcomp.solvable.abelian]
homocyclic1 [prf, in mathcomp.solvable.abelian]
homocyclic_Ohm_Mho [prf, in mathcomp.solvable.abelian]
homotopy [file, in mathcomp.analysis.homotopy_theory.homotopy]
homoW [prf, in mathcomp.boot.eqtype]
homoW_in [prf, in mathcomp.boot.eqtype]
horner [def, in mathcomp.algebra.poly]
horner0 [prf, in mathcomp.algebra.poly]
horner0_ext [prf, in mathcomp.analysis.derive]
horner2_swapXY [prf, in mathcomp.algebra.polyXY]
horner_alg [def, in mathcomp.algebra.poly]
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 [def, in mathcomp.algebra.poly]
horner_eval_is_linear [prf, in mathcomp.algebra.poly]
horner_eval_is_monoid_morphism [prf, in mathcomp.algebra.poly]
horner_eval_is_multiplicative [def, 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_multiplicative [def, in mathcomp.algebra.poly]
horner_is_semilinear [prf, in mathcomp.algebra.poly]
horner_map [prf, in mathcomp.algebra.poly]
horner_morph [def, in mathcomp.algebra.poly]
horner_morphC [prf, in mathcomp.algebra.poly]
horner_morphX [prf, in mathcomp.algebra.poly]
horner_mx [def, in mathcomp.algebra.mxpoly]
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_rec [def, 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]
hornerE [def, in mathcomp.algebra.poly]
hornerE_comm [def, 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]
hQ [abbrev, in mathcomp.field.qfpoly]
hQ [abbrev, in mathcomp.field.qfpoly]
hQ [abbrev, in mathcomp.algebra.qpoly]
hsubmxK [prf, in mathcomp.algebra.matrix]