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

## K

ker [definition, in morphism]kercoset_rcoset [lemma, in quotient]

kerE [lemma, in morphism]

kerHK [definition, in center]

kermx [definition, in mxalgebra]

kermx_hom_module [lemma, in mxrepresentation]

kermx_eq0 [lemma, in mxalgebra]

kermx_centg_module [lemma, in mxrepresentation]

kerP [lemma, in morphism]

ker_cprodm [lemma, in gproduct]

ker_cprod_by_central [lemma, in center]

ker_reprGLm [lemma, in mxabelem]

ker_in_cprod [lemma, in center]

ker_autm [lemma, in automorphism]

ker_sub_pre [lemma, in morphism]

ker_ifactm [lemma, in morphism]

ker_group [definition, in morphism]

ker_invm [lemma, in morphism]

ker_restrm [lemma, in morphism]

ker_dprodm [lemma, in gproduct]

ker_norm [lemma, in morphism]

ker_quotm [lemma, in quotient]

ker_comp [lemma, in morphism]

ker_trivm [lemma, in morphism]

ker_factm_loc [lemma, in morphism]

ker_factm [lemma, in morphism]

ker_coset [lemma, in quotient]

ker_irr_comp_op [lemma, in mxrepresentation]

ker_sgval [lemma, in morphism]

ker_eltm [lemma, in cyclic]

ker_normal_pre [lemma, in morphism]

ker_actperm [lemma, in action]

ker_subg [lemma, in morphism]

ker_conj_aut [lemma, in automorphism]

ker_trivg_morphim [lemma, in morphism]

ker_cprod_by [definition, in center]

ker_cprod_by_group [definition, in center]

ker_coset_prim [lemma, in quotient]

ker_restr_perm [lemma, in action]

ker_pprodm [lemma, in gproduct]

ker_idm [lemma, in morphism]

ker_cprod_by_is_group [lemma, in center]

ker_sdprodm [lemma, in gproduct]

ker_injm [lemma, in morphism]

ker_normal [lemma, in morphism]

ker_rcoset [lemma, in morphism]

kquo_repr_coset [lemma, in mxrepresentation]

kquo_repr [definition, in mxrepresentation]

kquo_mxE [lemma, in mxrepresentation]

kquo_mx [definition, in mxrepresentation]

kquo_mx_faithful [lemma, in mxrepresentation]

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