| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -
E (variable)
-ElementOps.T [in mathcomp.fingroup.fingroup]-Elim1.f [in mathcomp.ssreflect.bigop]
-Elim1.fM [in mathcomp.ssreflect.bigop]
-Elim1.f_id [in mathcomp.ssreflect.bigop]
-Elim1.idx [in mathcomp.ssreflect.bigop]
-Elim1.K [in mathcomp.ssreflect.bigop]
-Elim1.Kid [in mathcomp.ssreflect.bigop]
-Elim1.Kop [in mathcomp.ssreflect.bigop]
-Elim1.Kop' [in mathcomp.ssreflect.bigop]
-Elim1.op [in mathcomp.ssreflect.bigop]
-Elim1.op' [in mathcomp.ssreflect.bigop]
-Elim1.R [in mathcomp.ssreflect.bigop]
-Elim2.f [in mathcomp.ssreflect.bigop]
-Elim2.f_id [in mathcomp.ssreflect.bigop]
-Elim2.f_op [in mathcomp.ssreflect.bigop]
-Elim2.id1 [in mathcomp.ssreflect.bigop]
-Elim2.id2 [in mathcomp.ssreflect.bigop]
-Elim2.K [in mathcomp.ssreflect.bigop]
-Elim2.Kid [in mathcomp.ssreflect.bigop]
-Elim2.Kop [in mathcomp.ssreflect.bigop]
-Elim2.op1 [in mathcomp.ssreflect.bigop]
-Elim2.op2 [in mathcomp.ssreflect.bigop]
-Elim2.R1 [in mathcomp.ssreflect.bigop]
-Elim2.R2 [in mathcomp.ssreflect.bigop]
-Elim3.id1 [in mathcomp.ssreflect.bigop]
-Elim3.id2 [in mathcomp.ssreflect.bigop]
-Elim3.id3 [in mathcomp.ssreflect.bigop]
-Elim3.K [in mathcomp.ssreflect.bigop]
-Elim3.Kid [in mathcomp.ssreflect.bigop]
-Elim3.Kop [in mathcomp.ssreflect.bigop]
-Elim3.op1 [in mathcomp.ssreflect.bigop]
-Elim3.op2 [in mathcomp.ssreflect.bigop]
-Elim3.op3 [in mathcomp.ssreflect.bigop]
-Elim3.R1 [in mathcomp.ssreflect.bigop]
-Elim3.R2 [in mathcomp.ssreflect.bigop]
-Elim3.R3 [in mathcomp.ssreflect.bigop]
-Eltm.aT [in mathcomp.solvable.cyclic]
-Eltm.dvd_y_x [in mathcomp.solvable.cyclic]
-Eltm.rT [in mathcomp.solvable.cyclic]
-Eltm.x [in mathcomp.solvable.cyclic]
-Eltm.y [in mathcomp.solvable.cyclic]
-EncodingModuloEquiv.D [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloEquiv.DE [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloEquiv.e [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloEquiv.E [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloEquiv.ED [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloEquiv.r [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloRel.D [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloRel.DE [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloRel.e [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloRel.E [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloRel.ED [in mathcomp.ssreflect.generic_quotient]
-EncodingModuloRel.r [in mathcomp.ssreflect.generic_quotient]
-EnumRank.T [in mathcomp.ssreflect.fintype]
-EqAllPairsDep.R [in mathcomp.ssreflect.seq]
-EqAllPairsDep.S [in mathcomp.ssreflect.seq]
-EqAllPairsDep.T [in mathcomp.ssreflect.seq]
-EqAllPairs.R [in mathcomp.ssreflect.seq]
-EqAllPairs.S [in mathcomp.ssreflect.seq]
-EqAllPairs.T [in mathcomp.ssreflect.seq]
-EqConnect.T [in mathcomp.ssreflect.fingraph]
-EqFlatten.S [in mathcomp.ssreflect.seq]
-EqFlatten.T [in mathcomp.ssreflect.seq]
-EqFun.aT [in mathcomp.ssreflect.eqtype]
-EqFun.Endo.T [in mathcomp.ssreflect.eqtype]
-EqFun.Exo.aT [in mathcomp.ssreflect.eqtype]
-EqFun.Exo.D [in mathcomp.ssreflect.eqtype]
-EqFun.Exo.f [in mathcomp.ssreflect.eqtype]
-EqFun.Exo.g [in mathcomp.ssreflect.eqtype]
-EqFun.Exo.rT [in mathcomp.ssreflect.eqtype]
-EqFun.f [in mathcomp.ssreflect.eqtype]
-EqFun.h [in mathcomp.ssreflect.eqtype]
-EqFun.k [in mathcomp.ssreflect.eqtype]
-EqFun.rT1 [in mathcomp.ssreflect.eqtype]
-EqFun.rT2 [in mathcomp.ssreflect.eqtype]
-EqImage.T [in mathcomp.ssreflect.fintype]
-EqImage.T' [in mathcomp.ssreflect.fintype]
-EqIso.eqGH [in mathcomp.fingroup.quotient]
-EqIso.G [in mathcomp.fingroup.quotient]
-EqIso.gT [in mathcomp.fingroup.quotient]
-EqIso.H [in mathcomp.fingroup.quotient]
-EqMap.f [in mathcomp.ssreflect.seq]
-EqMap.Hf [in mathcomp.ssreflect.seq]
-EqMap.n0 [in mathcomp.ssreflect.seq]
-EqMap.T1 [in mathcomp.ssreflect.seq]
-EqMap.T2 [in mathcomp.ssreflect.seq]
-EqMap.x1 [in mathcomp.ssreflect.seq]
-EqMap.x2 [in mathcomp.ssreflect.seq]
-EqMask.n0 [in mathcomp.ssreflect.seq]
-EqMask.T [in mathcomp.ssreflect.seq]
-EqPath.e [in mathcomp.ssreflect.path]
-EqPath.n0 [in mathcomp.ssreflect.path]
-EqPath.T [in mathcomp.ssreflect.path]
-EqPath.x0_cycle [in mathcomp.ssreflect.path]
-EqPcore.gT [in mathcomp.solvable.pgroup]
-EqPmapSub.insT [in mathcomp.ssreflect.seq]
-EqPmapSub.p [in mathcomp.ssreflect.seq]
-EqPmapSub.sT [in mathcomp.ssreflect.seq]
-EqPmapSub.T [in mathcomp.ssreflect.seq]
-EqPmap.aT [in mathcomp.ssreflect.seq]
-EqPmap.f [in mathcomp.ssreflect.seq]
-EqPmap.fK [in mathcomp.ssreflect.seq]
-EqPmap.g [in mathcomp.ssreflect.seq]
-EqPmap.rT [in mathcomp.ssreflect.seq]
-EqPred.b [in mathcomp.ssreflect.eqtype]
-EqPred.T [in mathcomp.ssreflect.eqtype]
-EqPred.T2 [in mathcomp.ssreflect.eqtype]
-EqPred.u [in mathcomp.ssreflect.eqtype]
-EqPred.x [in mathcomp.ssreflect.eqtype]
-EqPred.y [in mathcomp.ssreflect.eqtype]
-EqPred.z [in mathcomp.ssreflect.eqtype]
-EqQuotTheory.e [in mathcomp.ssreflect.generic_quotient]
-EqQuotTheory.Q [in mathcomp.ssreflect.generic_quotient]
-EqQuotTheory.T [in mathcomp.ssreflect.generic_quotient]
-EqQuotTypeStructure.eq_quot_op [in mathcomp.ssreflect.generic_quotient]
-EqQuotTypeStructure.T [in mathcomp.ssreflect.generic_quotient]
-EqSeq.EqIn.a1 [in mathcomp.ssreflect.seq]
-EqSeq.EqIn.a2 [in mathcomp.ssreflect.seq]
-EqSeq.Filters.A [in mathcomp.ssreflect.seq]
-EqSeq.Filters.a [in mathcomp.ssreflect.seq]
-EqSeq.Filters.aP [in mathcomp.ssreflect.seq]
-EqSeq.Filters.s [in mathcomp.ssreflect.seq]
-EqSeq.inE [in mathcomp.ssreflect.seq]
-EqSeq.n0 [in mathcomp.ssreflect.seq]
-EqSeq.T [in mathcomp.ssreflect.seq]
-EqSeq.x0 [in mathcomp.ssreflect.seq]
-EqTheory.aT [in mathcomp.ssreflect.finfun]
-EqTheory.rT [in mathcomp.ssreflect.finfun]
-EqTrajectory.f [in mathcomp.ssreflect.path]
-EqTrajectory.T [in mathcomp.ssreflect.path]
-EqTuple.n [in mathcomp.ssreflect.tuple]
-EqTuple.T [in mathcomp.ssreflect.tuple]
-Equality.ClassDef.cT [in mathcomp.ssreflect.eqtype]
-Equality.ClassDef.T [in mathcomp.ssreflect.eqtype]
-EquivQuotTheory.e [in mathcomp.ssreflect.generic_quotient]
-EquivQuotTheory.Q [in mathcomp.ssreflect.generic_quotient]
-EquivQuotTheory.T [in mathcomp.ssreflect.generic_quotient]
-EquivQuot.EquivQuot.C [in mathcomp.ssreflect.generic_quotient]
-EquivQuot.EquivQuot.CD [in mathcomp.ssreflect.generic_quotient]
-EquivQuot.EquivQuot.D [in mathcomp.ssreflect.generic_quotient]
-EquivQuot.EquivQuot.DC [in mathcomp.ssreflect.generic_quotient]
-EquivQuot.EquivQuot.eD [in mathcomp.ssreflect.generic_quotient]
-EquivQuot.EquivQuot.encD [in mathcomp.ssreflect.generic_quotient]
-EquivRel.e [in mathcomp.ssreflect.generic_quotient]
-EquivRel.T [in mathcomp.ssreflect.generic_quotient]
-ExMaxn.exP [in mathcomp.ssreflect.ssrnat]
-ExMaxn.m [in mathcomp.ssreflect.ssrnat]
-ExMaxn.P [in mathcomp.ssreflect.ssrnat]
-ExMaxn.ubP [in mathcomp.ssreflect.ssrnat]
-ExMinn.exP [in mathcomp.ssreflect.ssrnat]
-ExMinn.P [in mathcomp.ssreflect.ssrnat]
-ExponentAbelem.gT [in mathcomp.solvable.abelian]
-ExponentPextraspecialTheory.p [in mathcomp.solvable.extraspecial]
-ExponentPextraspecialTheory.p_gt0 [in mathcomp.solvable.extraspecial]
-ExponentPextraspecialTheory.p_gt1 [in mathcomp.solvable.extraspecial]
-ExponentPextraspecialTheory.p_pr [in mathcomp.solvable.extraspecial]
-ExprzField.F [in mathcomp.algebra.ssrint]
-ExprzIdomain.R [in mathcomp.algebra.ssrint]
-ExprzOrder.R [in mathcomp.algebra.ssrint]
-ExprzUnitRing.R [in mathcomp.algebra.ssrint]
-Exprz_Zint_UnitRing.R [in mathcomp.algebra.ssrint]
-ExtCprod.gTH [in mathcomp.solvable.center]
-ExtCprod.gTK [in mathcomp.solvable.center]
-ExtCprod.gt_ [in mathcomp.solvable.center]
-ExtCprod.G_ [in mathcomp.solvable.center]
-ExtCprod.H [in mathcomp.solvable.center]
-ExtCprod.K [in mathcomp.solvable.center]
-ExtendInvariantIrr.ConsttIndExtendible.c [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.chi [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.cNt [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.G [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.IGtheta [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.N [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.nNG [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.nsNG [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.sNG [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.t [in mathcomp.character.inertia]
-ExtendInvariantIrr.ConsttIndExtendible.theta [in mathcomp.character.inertia]
-ExtendInvariantIrr.gT [in mathcomp.character.inertia]
-Extensionality.idx [in mathcomp.ssreflect.bigop]
-Extensionality.op [in mathcomp.ssreflect.bigop]
-Extensionality.R [in mathcomp.ssreflect.bigop]
-Extensionality.SeqExtension.I [in mathcomp.ssreflect.bigop]
-ExternalAction.A [in mathcomp.solvable.hall]
-ExternalAction.aT [in mathcomp.solvable.hall]
-ExternalAction.FullExtension.coGA [in mathcomp.solvable.hall]
-ExternalAction.FullExtension.coGA' [in mathcomp.solvable.hall]
-ExternalAction.FullExtension.injA [in mathcomp.solvable.hall]
-ExternalAction.FullExtension.injG [in mathcomp.solvable.hall]
-ExternalAction.FullExtension.nGA' [in mathcomp.solvable.hall]
-ExternalAction.FullExtension.solG [in mathcomp.solvable.hall]
-ExternalAction.FullExtension.solG' [in mathcomp.solvable.hall]
-ExternalAction.G [in mathcomp.solvable.hall]
-ExternalAction.gT [in mathcomp.solvable.hall]
-ExternalAction.pi [in mathcomp.solvable.hall]
-ExternalAction.to [in mathcomp.solvable.hall]
-ExternalDirProd.gT1 [in mathcomp.fingroup.gproduct]
-ExternalDirProd.gT2 [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.A [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.aT [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.D [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.G [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.R [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.rT [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.sAD [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.sGR [in mathcomp.fingroup.gproduct]
-ExternalSDirProd.to [in mathcomp.fingroup.gproduct]
-Extraspecial.Basic.esS [in mathcomp.solvable.maximal]
-Extraspecial.Basic.pS [in mathcomp.solvable.maximal]
-Extraspecial.Basic.pZ [in mathcomp.solvable.maximal]
-Extraspecial.Basic.S [in mathcomp.solvable.maximal]
-Extraspecial.esS [in mathcomp.character.mxabelem]
-Extraspecial.ExtraspecialFormspace.esG [in mathcomp.solvable.maximal]
-Extraspecial.ExtraspecialFormspace.G [in mathcomp.solvable.maximal]
-Extraspecial.ExtraspecialFormspace.oZ [in mathcomp.solvable.maximal]
-Extraspecial.ExtraspecialFormspace.pG [in mathcomp.solvable.maximal]
-Extraspecial.ExtraspecialFormspace.p_gt0 [in mathcomp.solvable.maximal]
-Extraspecial.ExtraspecialFormspace.p_gt1 [in mathcomp.solvable.maximal]
-Extraspecial.ExtraspecialFormspace.p_pr [in mathcomp.solvable.maximal]
-Extraspecial.F [in mathcomp.character.mxabelem]
-Extraspecial.ffulU [in mathcomp.character.mxabelem]
-Extraspecial.F'S [in mathcomp.character.mxabelem]
-Extraspecial.gT [in mathcomp.solvable.maximal]
-Extraspecial.gT [in mathcomp.character.mxabelem]
-Extraspecial.m [in mathcomp.character.mxabelem]
-Extraspecial.modIp' [in mathcomp.character.mxabelem]
-Extraspecial.n [in mathcomp.character.mxabelem]
-Extraspecial.oSpn [in mathcomp.character.mxabelem]
-Extraspecial.oZp [in mathcomp.character.mxabelem]
-Extraspecial.p [in mathcomp.solvable.maximal]
-Extraspecial.p [in mathcomp.character.mxabelem]
-Extraspecial.pS [in mathcomp.character.mxabelem]
-Extraspecial.p_gt1 [in mathcomp.character.mxabelem]
-Extraspecial.p_gt0 [in mathcomp.character.mxabelem]
-Extraspecial.p_pr [in mathcomp.character.mxabelem]
-Extraspecial.rS [in mathcomp.character.mxabelem]
-Extraspecial.rT [in mathcomp.solvable.maximal]
-Extraspecial.rZ [in mathcomp.character.mxabelem]
-Extraspecial.S [in mathcomp.character.mxabelem]
-Extraspecial.simU [in mathcomp.character.mxabelem]
-Extraspecial.splitF [in mathcomp.character.mxabelem]
-Extraspecial.StructureCorollaries.esS [in mathcomp.solvable.maximal]
-Extraspecial.StructureCorollaries.oZ [in mathcomp.solvable.maximal]
-Extraspecial.StructureCorollaries.pS [in mathcomp.solvable.maximal]
-Extraspecial.StructureCorollaries.p_pr [in mathcomp.solvable.maximal]
-Extraspecial.StructureCorollaries.S [in mathcomp.solvable.maximal]
-Extraspecial.sZS [in mathcomp.character.mxabelem]
-Extraspecial.U [in mathcomp.character.mxabelem]
-ExtremalTheory.DihedralGroup.def_q [in mathcomp.solvable.extremal]
-ExtremalTheory.DihedralGroup.def2 [in mathcomp.solvable.extremal]
-ExtremalTheory.DihedralGroup.Dihedral_extension.even_p [in mathcomp.solvable.extremal]
-ExtremalTheory.DihedralGroup.Dihedral_extension.p_gt1 [in mathcomp.solvable.extremal]
-ExtremalTheory.DihedralGroup.Dihedral_extension.p [in mathcomp.solvable.extremal]
-ExtremalTheory.DihedralGroup.m [in mathcomp.solvable.extremal]
-ExtremalTheory.DihedralGroup.q [in mathcomp.solvable.extremal]
-ExtremalTheory.DihedralGroup.q_gt1 [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalClass.G [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalClass.gT [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.def2qr [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.G [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.gT [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.m [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.Mxy [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.My [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.n [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.q [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.q_gt0 [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.r [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.r_gt0 [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.X [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.x [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.xyG [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.Y [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.y [in mathcomp.solvable.extremal]
-ExtremalTheory.ExtremalStructure.yG [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.def_r [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.def_q [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.def_p [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.def_n [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.ltqm [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.ltrq [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.m [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.n [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.n_gt2 [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.p [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.p_gt0 [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.p_gt1 [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.p_pr [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.q [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.q_gt1 [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.r [in mathcomp.solvable.extremal]
-ExtremalTheory.ModularGroup.r_gt0 [in mathcomp.solvable.extremal]
-ExtremalTheory.Quaternion.defQ [in mathcomp.solvable.extremal]
-ExtremalTheory.Quaternion.GrpQ [in mathcomp.solvable.extremal]
-ExtremalTheory.Quaternion.m [in mathcomp.solvable.extremal]
-ExtremalTheory.Quaternion.n [in mathcomp.solvable.extremal]
-ExtremalTheory.Quaternion.n_gt2 [in mathcomp.solvable.extremal]
-ExtremalTheory.Quaternion.q [in mathcomp.solvable.extremal]
-ExtremalTheory.Quaternion.r [in mathcomp.solvable.extremal]
-Extremal.Construction.a [in mathcomp.solvable.extremal]
-Extremal.Construction.b [in mathcomp.solvable.extremal]
-Extremal.Construction.e [in mathcomp.solvable.extremal]
-Extremal.Construction.p [in mathcomp.solvable.extremal]
-Extremal.Construction.p_gt1 [in mathcomp.solvable.extremal]
-Extremal.Construction.q [in mathcomp.solvable.extremal]
-Extremal.Construction.q_gt1 [in mathcomp.solvable.extremal]
-Extrema.ArgMinMax.F [in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.I [in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.i0 [in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.P [in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.Pi0 [in mathcomp.ssreflect.fintype]
-Extrema.arg_pred [in mathcomp.ssreflect.fintype]
-Extrema.Extremum.ord_total [in mathcomp.ssreflect.fintype]
-Extrema.Extremum.ord_trans [in mathcomp.ssreflect.fintype]
-Extrema.Extremum.ord_refl [in mathcomp.ssreflect.fintype]
-Extrema.Extremum.Pi0 [in mathcomp.ssreflect.fintype]
-ExtSdprodm.actf [in mathcomp.fingroup.gproduct]
-ExtSdprodm.aT [in mathcomp.fingroup.gproduct]
-ExtSdprodm.DgH [in mathcomp.fingroup.gproduct]
-ExtSdprodm.DgK [in mathcomp.fingroup.gproduct]
-ExtSdprodm.fH [in mathcomp.fingroup.gproduct]
-ExtSdprodm.fK [in mathcomp.fingroup.gproduct]
-ExtSdprodm.gT [in mathcomp.fingroup.gproduct]
-ExtSdprodm.H [in mathcomp.fingroup.gproduct]
-ExtSdprodm.K [in mathcomp.fingroup.gproduct]
-ExtSdprodm.rT [in mathcomp.fingroup.gproduct]
-ExtSdprodm.to [in mathcomp.fingroup.gproduct]
-
| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -