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 | (23233 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 | (1373 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 | (213 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 | (3475 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 | (89 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 | (11853 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 | (359 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 | (47 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 | (103 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 | (266 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 | (1118 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 | (691 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 | (3461 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 | (185 entries) |

## H

H [abbreviation, in mathcomp.fingroup.quotient]H [abbreviation, in mathcomp.character.classfun]

H [abbreviation, in mathcomp.character.classfun]

H [abbreviation, in mathcomp.character.classfun]

half [definition, in mathcomp.ssreflect.ssrnat]

halfD [lemma, in mathcomp.ssreflect.ssrnat]

half_gt0 [lemma, in mathcomp.ssreflect.ssrnat]

half_leq [lemma, in mathcomp.ssreflect.ssrnat]

half_bit_double [lemma, in mathcomp.ssreflect.ssrnat]

half_double [definition, in mathcomp.ssreflect.ssrnat]

Hall [section, in mathcomp.solvable.hall]

Hall [definition, in mathcomp.solvable.pgroup]

hall [library]

HallCorollaries [section, in mathcomp.solvable.hall]

HallCorollaries.gT [variable, in mathcomp.solvable.hall]

HallJ [lemma, in mathcomp.solvable.pgroup]

HallP [lemma, in mathcomp.solvable.pgroup]

Hall_Frattini_arg [lemma, in mathcomp.solvable.hall]

Hall_Jsub [lemma, in mathcomp.solvable.hall]

Hall_subJ [lemma, in mathcomp.solvable.hall]

Hall_superset [lemma, in mathcomp.solvable.hall]

Hall_trans [lemma, in mathcomp.solvable.hall]

Hall_exists [lemma, in mathcomp.solvable.hall]

Hall_exists_subJ [lemma, in mathcomp.solvable.hall]

Hall_max [lemma, in mathcomp.solvable.pgroup]

Hall_pi [lemma, in mathcomp.solvable.pgroup]

Hall_Witt_identity [lemma, in mathcomp.solvable.commutator]

Hall_setI_normal [lemma, in mathcomp.solvable.sylow]

Hall_psubJ [lemma, in mathcomp.solvable.sylow]

Hall_pJsub [lemma, in mathcomp.solvable.sylow]

Hall1 [lemma, in mathcomp.solvable.pgroup]

has [definition, in mathcomp.ssreflect.seq]

HasFrobeniusAction [constructor, in mathcomp.solvable.frobenius]

hasP [lemma, in mathcomp.ssreflect.seq]

hasPn [lemma, in mathcomp.ssreflect.seq]

has_Frobenius_action [inductive, in mathcomp.solvable.frobenius]

has_tnthP [lemma, in mathcomp.ssreflect.tuple]

has_nonprincipal_irr [lemma, in mathcomp.character.character]

has_map [lemma, in mathcomp.ssreflect.seq]

has_mask [lemma, in mathcomp.ssreflect.seq]

has_mask_cons [lemma, in mathcomp.ssreflect.seq]

has_rotr [lemma, in mathcomp.ssreflect.seq]

has_nthP [lemma, in mathcomp.ssreflect.seq]

has_pred1 [lemma, in mathcomp.ssreflect.seq]

has_sym [lemma, in mathcomp.ssreflect.seq]

has_filter [lemma, in mathcomp.ssreflect.seq]

has_rev [lemma, in mathcomp.ssreflect.seq]

has_rot [lemma, in mathcomp.ssreflect.seq]

has_predU [lemma, in mathcomp.ssreflect.seq]

has_predC [lemma, in mathcomp.ssreflect.seq]

has_predT [lemma, in mathcomp.ssreflect.seq]

has_pred0 [lemma, in mathcomp.ssreflect.seq]

has_rcons [lemma, in mathcomp.ssreflect.seq]

has_cat [lemma, in mathcomp.ssreflect.seq]

has_seqb [lemma, in mathcomp.ssreflect.seq]

has_nseq [lemma, in mathcomp.ssreflect.seq]

has_seq1 [lemma, in mathcomp.ssreflect.seq]

has_nil [lemma, in mathcomp.ssreflect.seq]

has_find [lemma, in mathcomp.ssreflect.seq]

has_count [lemma, in mathcomp.ssreflect.seq]

has_algid1 [lemma, in mathcomp.field.falgebra]

has_algidP [lemma, in mathcomp.field.falgebra]

has_algid [definition, in mathcomp.field.falgebra]

has_prim_root [lemma, in mathcomp.solvable.cyclic]

has_mxring_id [definition, in mathcomp.algebra.mxalgebra]

has_non_scalar_mxP [lemma, in mathcomp.algebra.mxalgebra]

head [definition, in mathcomp.ssreflect.seq]

headI [lemma, in mathcomp.ssreflect.seq]

HG [abbreviation, in mathcomp.solvable.finmodule]

Hilbert's_theorem_90 [lemma, in mathcomp.field.galois]

holds [abbreviation, in mathcomp.character.mxrepresentation]

holds_ex_elim [lemma, in mathcomp.field.closed_field]

holds_conjn [lemma, in mathcomp.field.closed_field]

holds_conj [lemma, in mathcomp.field.closed_field]

homg [definition, in mathcomp.fingroup.morphism]

Homg [section, in mathcomp.fingroup.morphism]

homgP [lemma, in mathcomp.fingroup.morphism]

homGrp_trans [lemma, in mathcomp.fingroup.presentation]

homg_quotientS [lemma, in mathcomp.fingroup.quotient]

homg_trans [lemma, in mathcomp.fingroup.morphism]

homg_refl [lemma, in mathcomp.fingroup.morphism]

homocyclic [definition, in mathcomp.solvable.abelian]

homocyclic_Ohm_Mho [lemma, in mathcomp.solvable.abelian]

homocyclic1 [lemma, in mathcomp.solvable.abelian]

Hom_G [abbreviation, in mathcomp.character.mxrepresentation]

hom_component_mx [lemma, in mathcomp.character.mxrepresentation]

hom_component_mx_iso [lemma, in mathcomp.character.mxrepresentation]

hom_mxsemisimple_iso [lemma, in mathcomp.character.mxrepresentation]

hom_mxsemisimple [lemma, in mathcomp.character.mxrepresentation]

hom_cyclic_mx [lemma, in mathcomp.character.mxrepresentation]

hom_mxmodule [lemma, in mathcomp.character.mxrepresentation]

hom_envelop_mxC [lemma, in mathcomp.character.mxrepresentation]

hom_mxP [lemma, in mathcomp.character.mxrepresentation]

horner [definition, in mathcomp.algebra.poly]

hornerC [lemma, in mathcomp.algebra.poly]

hornerCM [lemma, in mathcomp.algebra.poly]

hornerD [lemma, in mathcomp.algebra.poly]

hornerE [definition, in mathcomp.algebra.poly]

hornerE_comm [definition, in mathcomp.algebra.poly]

hornerM [lemma, in mathcomp.algebra.poly]

hornerMn [lemma, in mathcomp.algebra.poly]

HornerMx [section, in mathcomp.algebra.mxpoly]

hornerMX [lemma, in mathcomp.algebra.poly]

hornerMXaddC [lemma, in mathcomp.algebra.poly]

HornerMx.A [variable, in mathcomp.algebra.mxpoly]

HornerMx.n' [variable, in mathcomp.algebra.mxpoly]

HornerMx.R [variable, in mathcomp.algebra.mxpoly]

hornerMz [lemma, in mathcomp.algebra.ssrint]

hornerM_comm [lemma, in mathcomp.algebra.poly]

hornerN [lemma, in mathcomp.algebra.poly]

hornerX [lemma, in mathcomp.algebra.poly]

hornerXn [lemma, in mathcomp.algebra.poly]

hornerXsubC [lemma, in mathcomp.algebra.poly]

hornerZ [lemma, in mathcomp.algebra.poly]

horner_rVpoly_inj [lemma, in mathcomp.algebra.mxpoly]

horner_mxK [lemma, in mathcomp.algebra.mxpoly]

horner_rVpolyK [lemma, in mathcomp.algebra.mxpoly]

horner_mx_mem [lemma, in mathcomp.algebra.mxpoly]

horner_rVpoly [lemma, in mathcomp.algebra.mxpoly]

horner_mxZ [lemma, in mathcomp.algebra.mxpoly]

horner_mx_X [lemma, in mathcomp.algebra.mxpoly]

horner_mx_C [lemma, in mathcomp.algebra.mxpoly]

horner_mx [definition, in mathcomp.algebra.mxpoly]

horner_poly_XmY [lemma, in mathcomp.algebra.polyXY]

horner_poly_XaY [lemma, in mathcomp.algebra.polyXY]

horner_polyC [lemma, in mathcomp.algebra.polyXY]

horner_swapXY [lemma, in mathcomp.algebra.polyXY]

horner_comp [lemma, in mathcomp.algebra.poly]

horner_eval_is_lrmorphism [lemma, in mathcomp.algebra.poly]

horner_evalE [lemma, in mathcomp.algebra.poly]

horner_eval [definition, in mathcomp.algebra.poly]

horner_prod [lemma, in mathcomp.algebra.poly]

horner_exp [lemma, in mathcomp.algebra.poly]

horner_is_lrmorphism [lemma, in mathcomp.algebra.poly]

horner_morphX [lemma, in mathcomp.algebra.poly]

horner_morphC [lemma, in mathcomp.algebra.poly]

horner_map [lemma, in mathcomp.algebra.poly]

horner_morph [definition, in mathcomp.algebra.poly]

horner_exp_comm [lemma, in mathcomp.algebra.poly]

horner_sum [lemma, in mathcomp.algebra.poly]

horner_poly [lemma, in mathcomp.algebra.poly]

horner_coef_wide [lemma, in mathcomp.algebra.poly]

horner_coef [lemma, in mathcomp.algebra.poly]

horner_Poly [lemma, in mathcomp.algebra.poly]

horner_coef0 [lemma, in mathcomp.algebra.poly]

horner_cons [lemma, in mathcomp.algebra.poly]

horner_rec [definition, in mathcomp.algebra.poly]

horner_int [lemma, in mathcomp.algebra.ssrint]

horner0 [lemma, in mathcomp.algebra.poly]

horner2_swapXY [lemma, in mathcomp.algebra.polyXY]

hsubmxK [lemma, 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 | (23233 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 | (1373 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 | (213 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 | (3475 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 | (89 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 | (11853 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 | (359 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 | (47 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 | (103 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 | (266 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 | (1118 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 | (691 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 | (3461 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 | (185 entries) |