H (Definitions)
| 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 (Definitions)
half [def, in mathcomp.boot.ssrnat]half_double [def, in mathcomp.boot.ssrnat]
Hall [def, in mathcomp.solvable.pgroup]
has [def, in mathcomp.boot.seq]
has_algid [def, in mathcomp.field.falgebra]
has_mxring_id [def, in mathcomp.algebra.mxalgebra]
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.identity_builder [def, in mathcomp.boot.eqtype]
hasDecEq.phant_axioms [def, in mathcomp.boot.eqtype]
hasDecEq.phant_Build [def, in mathcomp.boot.eqtype]
hasInv.identity_builder [def, in mathcomp.boot.monoid]
hasInv.phant_axioms [def, in mathcomp.boot.monoid]
hasInv.phant_Build [def, in mathcomp.boot.monoid]
hasMul.identity_builder [def, in mathcomp.boot.monoid]
hasMul.phant_axioms [def, in mathcomp.boot.monoid]
hasMul.phant_Build [def, in mathcomp.boot.monoid]
hasOne.identity_builder [def, in mathcomp.boot.monoid]
hasOne.phant_axioms [def, in mathcomp.boot.monoid]
hasOne.phant_Build [def, in mathcomp.boot.monoid]
head [def, in mathcomp.boot.seq]
Hermitian.pack_ [def, in mathcomp.algebra.sesquilinear]
Hermitian.phant_clone [def, in mathcomp.algebra.sesquilinear]
Hermitian.phant_on_ [def, in mathcomp.algebra.sesquilinear]
hermitian1mx [def, in mathcomp.algebra.sesquilinear]
hermitianmx [def, in mathcomp.algebra.sesquilinear]
hermitianmx_keyed [def, in mathcomp.algebra.sesquilinear]
hide [def, in mathcomp.boot.ssreflect]
homg [def, in mathcomp.finite_group.morphism]
homocyclic [def, in mathcomp.solvable.abelian]
horner [def, in mathcomp.algebra.poly]
horner_alg [def, in mathcomp.algebra.poly]
horner_eval [def, in mathcomp.algebra.poly]
horner_eval_is_multiplicative [def, in mathcomp.algebra.poly]
horner_is_multiplicative [def, in mathcomp.algebra.poly]
horner_morph [def, in mathcomp.algebra.poly]
horner_mx [def, in mathcomp.algebra.mxpoly]
horner_rec [def, in mathcomp.algebra.poly]
hornerE [def, in mathcomp.algebra.poly]
hornerE_comm [def, in mathcomp.algebra.poly]