| 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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 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]
+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]
+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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +