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

## I (variable)

IdentityMorphism.gT [in morphism]Image.Def.A [in fintype]

Image.Def.injf [in fintype]

Image.f [in fintype]

Image.T [in fintype]

Image.T' [in fintype]

ImsetCurry.aT1 [in finset]

ImsetCurry.aT2 [in finset]

ImsetCurry.Curry.A1 [in finset]

ImsetCurry.Curry.A2 [in finset]

ImsetCurry.Curry.D1 [in finset]

ImsetCurry.Curry.D2 [in finset]

ImsetCurry.f [in finset]

ImsetCurry.rT [in finset]

InjectionsTheory.A [in ssrfun]

InjectionsTheory.B [in ssrfun]

InjectionsTheory.C [in ssrfun]

InjectionsTheory.f [in ssrfun]

InjectionsTheory.g [in ssrfun]

InjectionsTheory.h [in ssrfun]

Injections.aT [in ssrfun]

Injections.f [in ssrfun]

Injections.rT [in ssrfun]

Injectiveb.aT [in fintype]

Injectiveb.f [in fintype]

Injectiveb.rT [in fintype]

InjFactm.aT [in morphism]

InjFactm.D [in morphism]

InjFactm.f [in morphism]

InjFactm.g [in morphism]

InjFactm.G [in morphism]

InjFactm.gT [in morphism]

InjFactm.injf [in morphism]

InjFactm.rT [in morphism]

InjmAbelem.aT [in abelian]

InjmAbelem.D [in abelian]

InjmAbelem.f [in abelian]

InjmAbelem.G [in abelian]

InjmAbelem.injf [in abelian]

InjmAbelem.rT [in abelian]

InjmAbelem.sGD [in abelian]

InjmAutIn.D [in action]

InjmAutIn.f [in action]

InjmAutIn.G [in action]

InjmAutIn.gT [in action]

InjmAutIn.H [in action]

InjmAutIn.injf [in action]

InjmAutIn.rT [in action]

InjmAutIn.sGD [in action]

InjmAutIn.sHG [in action]

InjmAut.D [in automorphism]

InjmAut.f [in automorphism]

InjmAut.G [in automorphism]

InjmAut.gT [in automorphism]

InjmAut.injf [in automorphism]

InjmAut.rT [in automorphism]

InjmAut.sGD [in automorphism]

InjmChar.aT [in automorphism]

InjmChar.D [in automorphism]

InjmChar.f [in automorphism]

InjmChar.injf [in automorphism]

InjmChar.rT [in automorphism]

InjmMax.D [in gseries]

InjmMax.f [in gseries]

InjmMax.G [in gseries]

InjmMax.gT [in gseries]

InjmMax.H [in gseries]

InjmMax.injf [in gseries]

InjmMax.K [in gseries]

InjmMax.rT [in gseries]

Injm.aT [in pgroup]

Injm.D [in pgroup]

Injm.f [in pgroup]

Injm.injf [in pgroup]

Injm.rT [in pgroup]

InnerAutCyclicPgroup.C [in pgroup]

InnerAutCyclicPgroup.G [in pgroup]

InnerAutCyclicPgroup.gT [in pgroup]

InnerAutCyclicPgroup.nCG [in pgroup]

InnerAutCyclicPgroup.p [in pgroup]

InternalActionDefs.gT [in action]

InternalAction.gT [in hall]

InternalAction.pi [in hall]

InternalGroupAction.CardClass.G [in action]

InternalGroupAction.gT [in action]

InternalProd.DisjointRem.H [in gproduct]

InternalProd.DisjointRem.K [in gproduct]

InternalProd.DisjointRem.tiKH [in gproduct]

InternalProd.gT [in gproduct]

InternalProd.NormalComplement.complH_K [in gproduct]

InternalProd.NormalComplement.G [in gproduct]

InternalProd.NormalComplement.H [in gproduct]

InternalProd.NormalComplement.K [in gproduct]

InternalProd.NormalComplement.nKG [in gproduct]

InverseMorphism.aT [in morphism]

InverseMorphism.f [in morphism]

InverseMorphism.G [in morphism]

InverseMorphism.injf [in morphism]

InverseMorphism.rT [in morphism]

InvLinearApp.K [in vector]

InvLinearApp.V [in vector]

InvLinearApp.W [in vector]

Involutions.A [in ssrfun]

Involutions.f [in ssrfun]

Involutions.Hf [in ssrfun]

IRing.a [in poly]

IRing.R [in poly]

IsoBoolEquiv.G [in morphism]

IsoBoolEquiv.gT [in morphism]

IsoBoolEquiv.H [in morphism]

IsoBoolEquiv.hT [in morphism]

IsoBoolEquiv.K [in morphism]

IsoBoolEquiv.kT [in morphism]

IsoCyclic.gT [in cyclic]

IsoCyclic.rT [in cyclic]

IsoFitting.D [in maximal]

IsoFitting.f [in maximal]

IsoFitting.G [in maximal]

IsoFitting.gT [in maximal]

IsoFitting.rT [in maximal]

IsoFunctorTheory.F [in gfunctor]

IsogAbelem.aT [in abelian]

IsogAbelem.G [in abelian]

IsogAbelem.H [in abelian]

IsogAbelem.isoGH [in abelian]

IsogAbelem.rT [in abelian]

IsogAbelian.aT [in abelian]

IsogAbelian.D [in abelian]

IsogAbelian.f [in abelian]

IsogAbelian.rT [in abelian]

Isog.aT [in pgroup]

Isog.G [in pgroup]

Isog.H [in pgroup]

Isog.rT [in pgroup]

Isomorphisms.G [in morphism]

Isomorphisms.gT [in morphism]

Isomorphisms.H [in morphism]

Isomorphisms.hT [in morphism]

Isomorphisms.K [in morphism]

Isomorphisms.kT [in morphism]

Iteration.T [in ssrnat]

IterCprod.G [in center]

IterCprod.gT [in center]

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