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 | (24947 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 | (1496 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 | (216 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 | (3586 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 | (84 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 | (11878 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 | (389 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 | (49 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 | (119 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 | (272 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 | (1128 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 | (701 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 | (4837 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 | (192 entries) |

## I (section)

IdealDef [in mathcomp.algebra.ring_quotient]IdealDef.IdealTheory [in mathcomp.algebra.ring_quotient]

IdealDef.PrimeIdealTheory [in mathcomp.algebra.ring_quotient]

IdentityMorphism [in mathcomp.fingroup.morphism]

Image [in mathcomp.ssreflect.fintype]

Image.Injective [in mathcomp.ssreflect.fintype]

Image.SizeImage [in mathcomp.ssreflect.fintype]

ImsetCurry [in mathcomp.ssreflect.finset]

ImsetCurry.Curry [in mathcomp.ssreflect.finset]

Induced [in mathcomp.character.character]

Induced [in mathcomp.character.classfun]

Induced.Def [in mathcomp.character.classfun]

Inertia [in mathcomp.character.inertia]

InertiaBigdprod [in mathcomp.character.inertia]

InertiaBigdprod.ConjBig [in mathcomp.character.inertia]

InertiaBigdprod.InertiaBig [in mathcomp.character.inertia]

InertiaDprod [in mathcomp.character.inertia]

InertiaSdprod [in mathcomp.character.inertia]

InfinitePrimitiveElementTheorem [in mathcomp.field.separable]

Injections [in mathcomp.ssreflect.ssrfun]

InjectionsTheory [in mathcomp.ssreflect.ssrfun]

Injectiveb [in mathcomp.ssreflect.fintype]

InjFactm [in mathcomp.fingroup.morphism]

Injm [in mathcomp.solvable.pgroup]

InjmAbelem [in mathcomp.solvable.abelian]

InjmAut [in mathcomp.fingroup.automorphism]

InjmAutIn [in mathcomp.fingroup.action]

InjmChar [in mathcomp.fingroup.automorphism]

InjmFrobenius [in mathcomp.solvable.frobenius]

InjmMax [in mathcomp.solvable.gseries]

InnerAutCyclicPgroup [in mathcomp.solvable.pgroup]

InnerProduct [in mathcomp.character.character]

InPrealField [in mathcomp.algebra.rat]

InRing [in mathcomp.algebra.rat]

IntDist.Distn [in mathcomp.algebra.ssrint]

IntegralChar [in mathcomp.character.integral_char]

IntegralChar.GringIrrMode [in mathcomp.character.integral_char]

IntegralOverComRing [in mathcomp.algebra.mxpoly]

IntegralOverField [in mathcomp.algebra.mxpoly]

IntegralOverRing [in mathcomp.algebra.mxpoly]

InternalAction [in mathcomp.solvable.hall]

InternalActionDefs [in mathcomp.fingroup.action]

InternalGroupAction [in mathcomp.fingroup.action]

InternalGroupAction.CardClass [in mathcomp.fingroup.action]

InternalProd [in mathcomp.fingroup.gproduct]

InternalProd.DisjointRem [in mathcomp.fingroup.gproduct]

InternalProd.NormalComplement [in mathcomp.fingroup.gproduct]

IntervalField [in mathcomp.algebra.interval]

IntervalOrdered [in mathcomp.algebra.interval]

IntervalPo [in mathcomp.algebra.interval]

intOrderedTheory [in mathcomp.algebra.ssrint]

intOrdered.intOrdered [in mathcomp.algebra.ssrint]

intRingTheory [in mathcomp.algebra.ssrint]

intRing.intRing [in mathcomp.algebra.ssrint]

intUnitRing.intUnitRing [in mathcomp.algebra.ssrint]

intZmoduleTheory [in mathcomp.algebra.ssrint]

intZmod.intZmod [in mathcomp.algebra.ssrint]

InverseMorphism [in mathcomp.fingroup.morphism]

InvMorphism [in mathcomp.character.classfun]

Involutions [in mathcomp.ssreflect.ssrfun]

IrrClass [in mathcomp.character.character]

IrrClassDef [in mathcomp.character.character]

IrrConstt [in mathcomp.character.character]

IsChar [in mathcomp.character.character]

IsoBoolEquiv [in mathcomp.fingroup.morphism]

IsoCyclic [in mathcomp.solvable.cyclic]

IsoFitting [in mathcomp.solvable.maximal]

IsoFunctorTheory [in mathcomp.solvable.gfunctor]

Isog [in mathcomp.solvable.pgroup]

IsogAbelem [in mathcomp.solvable.abelian]

IsogAbelian [in mathcomp.solvable.abelian]

Isom [in mathcomp.character.character]

Isometries [in mathcomp.character.vcharacter]

IsomInv [in mathcomp.character.character]

Isomorphism [in mathcomp.character.classfun]

Isomorphisms [in mathcomp.fingroup.morphism]

Iteration [in mathcomp.ssreflect.ssrnat]

IterCprod [in mathcomp.solvable.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 | (24947 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 | (1496 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 | (216 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 | (3586 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 | (84 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 | (11878 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 | (389 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 | (49 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 | (119 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 | (272 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 | (1128 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 | (701 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 | (4837 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 | (192 entries) |