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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |

## H

H [abbreviation, in quotient]half [definition, in ssrnat]

half_add [lemma, in ssrnat]

half_double [definition, in ssrnat]

half_leq [lemma, in ssrnat]

half_gt0 [lemma, in ssrnat]

half_bit_double [lemma, in ssrnat]

Hall [definition, in pgroup]

Hall [section, in hall]

hall [library]

HallCorollaries [section, in hall]

HallCorollaries.gT [variable, in hall]

HallJ [lemma, in pgroup]

HallP [lemma, in pgroup]

Hall_subJ [lemma, in hall]

Hall_exists [lemma, in hall]

Hall_max [lemma, in pgroup]

Hall_pJsub [lemma, in sylow]

Hall_Frattini_arg [lemma, in hall]

Hall_psubJ [lemma, in sylow]

Hall_trans [lemma, in hall]

Hall_setI_normal [lemma, in sylow]

Hall_pi [lemma, in pgroup]

Hall_Witt_identity [lemma, in commutator]

Hall_exists_subJ [lemma, in hall]

Hall_superset [lemma, in hall]

Hall_Jsub [lemma, in hall]

Hall1 [lemma, in pgroup]

has [definition, in seq]

HasFrobeniusAction [constructor, in frobenius]

hasP [lemma, in seq]

hasPn [lemma, in seq]

has_rot [lemma, in seq]

has_rotr [lemma, in seq]

has_nil [lemma, in seq]

has_filter [lemma, in seq]

has_pred1 [lemma, in seq]

has_non_scalar_mxP [lemma, in mxalgebra]

has_sym [lemma, in seq]

has_predU [lemma, in seq]

has_predC [lemma, in seq]

has_prim_root [lemma, in cyclic]

has_Frobenius_action [inductive, in frobenius]

has_nthP [lemma, in seq]

has_pred0 [lemma, in seq]

has_cat [lemma, in seq]

has_map [lemma, in seq]

has_mask_cons [lemma, in seq]

has_count [lemma, in seq]

has_seq1 [lemma, in seq]

has_seqb [lemma, in seq]

has_rcons [lemma, in seq]

has_mxring_id [definition, in mxalgebra]

has_predT [lemma, in seq]

has_find [lemma, in seq]

head [definition, in seq]

headI [lemma, in seq]

head_coef_mul [lemma, in poly]

Hf [definition, in fingraph]

holds [abbreviation, in mxrepresentation]

homg [definition, in morphism]

Homg [section, in morphism]

homgP [lemma, in morphism]

homGrp_trans [lemma, in presentation]

homg_refl [lemma, in morphism]

homg_trans [lemma, in morphism]

homg_quotientS [lemma, in quotient]

homocyclic [definition, in abelian]

homocyclic_Ohm_Mho [lemma, in abelian]

hom_mxsemisimple [lemma, in mxrepresentation]

hom_mxmodule [lemma, in mxrepresentation]

hom_is_linear [lemma, in vector]

hom_component_mx [lemma, in mxrepresentation]

hom_envelop_mxC [lemma, in mxrepresentation]

hom_cyclic_mx [lemma, in mxrepresentation]

hom_mxP [lemma, in mxrepresentation]

hom_component_mx_iso [lemma, in mxrepresentation]

hom_mxsemisimple_iso [lemma, in mxrepresentation]

hom_linear [definition, in vector]

Hom_G [abbreviation, in mxrepresentation]

horner [definition, in poly]

hornerC [lemma, in poly]

HornerMx [section, in mxpoly]

HornerMx.A [variable, in mxpoly]

HornerMx.n' [variable, in mxpoly]

HornerMx.R [variable, in mxpoly]

hornerX [lemma, in poly]

hornerXn [lemma, in poly]

horner_lin [definition, in poly]

horner_sum [lemma, in poly]

horner_amulX [lemma, in poly]

horner_mx_X [lemma, in mxpoly]

horner_rmorphism [definition, in poly]

horner_additive [definition, in poly]

horner_mx [definition, in mxpoly]

horner_exp_com [lemma, in poly]

horner_exp [lemma, in poly]

horner_rVpolyK [lemma, in mxpoly]

horner_mul_com [lemma, in poly]

horner_morphX [lemma, in poly]

horner_coef_wide [lemma, in poly]

horner_is_rmorphism [lemma, in poly]

horner_cons [lemma, in poly]

horner_mxZ [lemma, in mxpoly]

horner_coef [lemma, in poly]

horner_mx_mem [lemma, in mxpoly]

horner_add [lemma, in poly]

horner_mulX [lemma, in poly]

horner_opp [lemma, in poly]

horner_mul [lemma, in poly]

horner_Poly [lemma, in poly]

horner_prod [lemma, in poly]

horner_lin_com [definition, in poly]

horner_scaler [lemma, in poly]

horner_poly [lemma, in poly]

horner_morph [definition, in poly]

horner_mxK [lemma, in mxpoly]

horner_mulrn [lemma, in poly]

horner_morphC [lemma, in poly]

horner_map [lemma, in poly]

horner_Cmul [lemma, in poly]

horner_poly_comp [lemma, in poly]

horner_mx_lrmorphism [definition, in mxpoly]

horner_mx_linear [definition, in mxpoly]

horner_mx_rmorphism [definition, in mxpoly]

horner_mx_additive [definition, in mxpoly]

horner_rVpoly_inj [lemma, in mxpoly]

horner_mx_C [lemma, in mxpoly]

horner_rVpoly [lemma, in mxpoly]

horner0 [lemma, in poly]

hsubmxK [lemma, in matrix]

H_g_rcosets [definition, in finmodule]

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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |