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 (lemma)

half_add [in ssrnat]half_leq [in ssrnat]

half_gt0 [in ssrnat]

half_bit_double [in ssrnat]

HallJ [in pgroup]

HallP [in pgroup]

Hall_subJ [in hall]

Hall_exists [in hall]

Hall_max [in pgroup]

Hall_pJsub [in sylow]

Hall_Frattini_arg [in hall]

Hall_psubJ [in sylow]

Hall_trans [in hall]

Hall_setI_normal [in sylow]

Hall_pi [in pgroup]

Hall_Witt_identity [in commutator]

Hall_exists_subJ [in hall]

Hall_superset [in hall]

Hall_Jsub [in hall]

Hall1 [in pgroup]

hasP [in seq]

hasPn [in seq]

has_rot [in seq]

has_rotr [in seq]

has_nil [in seq]

has_filter [in seq]

has_pred1 [in seq]

has_non_scalar_mxP [in mxalgebra]

has_sym [in seq]

has_predU [in seq]

has_predC [in seq]

has_prim_root [in cyclic]

has_nthP [in seq]

has_pred0 [in seq]

has_cat [in seq]

has_map [in seq]

has_mask_cons [in seq]

has_count [in seq]

has_seq1 [in seq]

has_seqb [in seq]

has_rcons [in seq]

has_predT [in seq]

has_find [in seq]

headI [in seq]

head_coef_mul [in poly]

homgP [in morphism]

homGrp_trans [in presentation]

homg_refl [in morphism]

homg_trans [in morphism]

homg_quotientS [in quotient]

homocyclic_Ohm_Mho [in abelian]

hom_mxsemisimple [in mxrepresentation]

hom_mxmodule [in mxrepresentation]

hom_is_linear [in vector]

hom_component_mx [in mxrepresentation]

hom_envelop_mxC [in mxrepresentation]

hom_cyclic_mx [in mxrepresentation]

hom_mxP [in mxrepresentation]

hom_component_mx_iso [in mxrepresentation]

hom_mxsemisimple_iso [in mxrepresentation]

hornerC [in poly]

hornerX [in poly]

hornerXn [in poly]

horner_sum [in poly]

horner_amulX [in poly]

horner_mx_X [in mxpoly]

horner_exp_com [in poly]

horner_exp [in poly]

horner_rVpolyK [in mxpoly]

horner_mul_com [in poly]

horner_morphX [in poly]

horner_coef_wide [in poly]

horner_is_rmorphism [in poly]

horner_cons [in poly]

horner_mxZ [in mxpoly]

horner_coef [in poly]

horner_mx_mem [in mxpoly]

horner_add [in poly]

horner_mulX [in poly]

horner_opp [in poly]

horner_mul [in poly]

horner_Poly [in poly]

horner_prod [in poly]

horner_scaler [in poly]

horner_poly [in poly]

horner_mxK [in mxpoly]

horner_mulrn [in poly]

horner_morphC [in poly]

horner_map [in poly]

horner_Cmul [in poly]

horner_poly_comp [in poly]

horner_rVpoly_inj [in mxpoly]

horner_mx_C [in mxpoly]

horner_rVpoly [in mxpoly]

horner0 [in poly]

hsubmxK [in 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 | (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) |