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 | (78577 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 | (1807 entries) |

Binder 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 | (48032 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 | (375 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 | (3995 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 | (91 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 | (14468 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 | (223 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 | (45 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 | (133 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 | (451 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 | (1387 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 | (1144 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 | (6179 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 | (247 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]

IncreasingSemiGroup [in mathcomp.ssreflect.bigop]

IncreasingSemiGroup.Id [in mathcomp.ssreflect.bigop]

Induced [in mathcomp.character.classfun]

Induced [in mathcomp.character.character]

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]

InheritedStructures [in mathcomp.ssreflect.finfun]

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]

IntervalChoice.IntervalChoice [in mathcomp.algebra.interval]

IntervalEq [in mathcomp.algebra.interval]

IntervalField [in mathcomp.algebra.interval]

IntervalLattice [in mathcomp.algebra.interval]

IntervalNumDomain [in mathcomp.algebra.interval]

IntervalPOrder [in mathcomp.algebra.interval]

IntervalTotal [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 | (78577 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 | (1807 entries) |

Binder 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 | (48032 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 | (375 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 | (3995 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 | (91 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 | (14468 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 | (223 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 | (45 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 | (133 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 | (451 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 | (1387 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 | (1144 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 | (6179 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 | (247 entries) |