| 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 | (100113 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 | (1864 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 | (49278 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 | (1631 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 | (6978 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 | (94 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 | (14781 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 | (75 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 | (222 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 | (131 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 | (2030 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 | (2189 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 | (1149 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 | (19126 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 | (565 entries) |
P (variable)
PairAlg.A1 [in mathcomp.algebra.ssralg]PairAlg.A2 [in mathcomp.algebra.ssralg]
PairAlg.R [in mathcomp.algebra.ssralg]
PairComSemiRing.R1 [in mathcomp.algebra.ssralg]
PairComSemiRing.R2 [in mathcomp.algebra.ssralg]
PairLalg.A1 [in mathcomp.algebra.ssralg]
PairLalg.A2 [in mathcomp.algebra.ssralg]
PairLalg.R [in mathcomp.algebra.ssralg]
PairLmod.R [in mathcomp.algebra.ssralg]
PairLmod.V1 [in mathcomp.algebra.ssralg]
PairLmod.V2 [in mathcomp.algebra.ssralg]
PairNmod.U [in mathcomp.algebra.ssralg]
PairNmod.V [in mathcomp.algebra.ssralg]
PairSemiRing.R1 [in mathcomp.algebra.ssralg]
PairSemiRing.R2 [in mathcomp.algebra.ssralg]
PairUnitRing.R1 [in mathcomp.algebra.ssralg]
PairUnitRing.R2 [in mathcomp.algebra.ssralg]
Pairwise.r [in mathcomp.ssreflect.seq]
Pairwise.T [in mathcomp.ssreflect.seq]
PairZmod.U [in mathcomp.algebra.ssralg]
PairZmod.V [in mathcomp.algebra.ssralg]
PartialAction.aT [in mathcomp.fingroup.action]
PartialAction.D [in mathcomp.fingroup.action]
PartialAction.OrbitStabilizer.G [in mathcomp.fingroup.action]
PartialAction.OrbitStabilizer.sGD [in mathcomp.fingroup.action]
PartialAction.OrbitStabilizer.ssGD [in mathcomp.fingroup.action]
PartialAction.OrbitStabilizer.x [in mathcomp.fingroup.action]
PartialAction.rT [in mathcomp.fingroup.action]
PartialAction.to [in mathcomp.fingroup.action]
PartialFunctorTheory.BasicTheory.F [in mathcomp.solvable.gfunctor]
PartialFunctorTheory.F1 [in mathcomp.solvable.gfunctor]
PartialFunctorTheory.F2 [in mathcomp.solvable.gfunctor]
PartialFunctorTheory.Modulo.F1 [in mathcomp.solvable.gfunctor]
PartialFunctorTheory.Modulo.F2 [in mathcomp.solvable.gfunctor]
PartitionImage.D [in mathcomp.ssreflect.finset]
PartitionImage.f [in mathcomp.ssreflect.finset]
PartitionImage.fP [in mathcomp.ssreflect.finset]
PartitionImage.inj_f [in mathcomp.ssreflect.finset]
PartitionImage.P [in mathcomp.ssreflect.finset]
PartitionImage.T [in mathcomp.ssreflect.finset]
PartitionImage.T' [in mathcomp.ssreflect.finset]
Partitions.BigOps.idx [in mathcomp.ssreflect.finset]
Partitions.BigOps.op [in mathcomp.ssreflect.finset]
Partitions.BigOps.R [in mathcomp.ssreflect.finset]
Partitions.BigOps.rhs [in mathcomp.ssreflect.finset]
Partitions.BigOps.rhs_cond [in mathcomp.ssreflect.finset]
Partitions.Equivalence.D [in mathcomp.ssreflect.finset]
Partitions.Equivalence.eqiR [in mathcomp.ssreflect.finset]
Partitions.Equivalence.PPx [in mathcomp.ssreflect.finset]
Partitions.Equivalence.Px [in mathcomp.ssreflect.finset]
Partitions.Equivalence.Pxx [in mathcomp.ssreflect.finset]
Partitions.Equivalence.R [in mathcomp.ssreflect.finset]
Partitions.I [in mathcomp.ssreflect.finset]
Partitions.Preim.f [in mathcomp.ssreflect.finset]
Partitions.Preim.rT [in mathcomp.ssreflect.finset]
Partitions.T [in mathcomp.ssreflect.finset]
Partitions.Transversals.D [in mathcomp.ssreflect.finset]
Partitions.Transversals.P [in mathcomp.ssreflect.finset]
Partitions.Transversals.sXP [in mathcomp.ssreflect.finset]
Partitions.Transversals.tiP [in mathcomp.ssreflect.finset]
Partitions.Transversals.trPX [in mathcomp.ssreflect.finset]
Partitions.Transversals.trX [in mathcomp.ssreflect.finset]
Partitions.Transversals.X [in mathcomp.ssreflect.finset]
Paths.EqPath_in.e'_e [in mathcomp.ssreflect.path]
Paths.EqPath_in.e_e' [in mathcomp.ssreflect.path]
Paths.EqPath_in.ee' [in mathcomp.ssreflect.path]
Paths.EqPath_in.e' [in mathcomp.ssreflect.path]
Paths.EqPath_in.e [in mathcomp.ssreflect.path]
Paths.EqPath_in.P [in mathcomp.ssreflect.path]
Paths.n0 [in mathcomp.ssreflect.path]
Paths.PathEq.e [in mathcomp.ssreflect.path]
Paths.PathEq.e' [in mathcomp.ssreflect.path]
Paths.Path.e [in mathcomp.ssreflect.path]
Paths.Path.x0_cycle [in mathcomp.ssreflect.path]
Paths.SubPath_in.ee' [in mathcomp.ssreflect.path]
Paths.SubPath_in.e' [in mathcomp.ssreflect.path]
Paths.SubPath_in.e [in mathcomp.ssreflect.path]
Paths.SubPath_in.P [in mathcomp.ssreflect.path]
Paths.SubPath.e [in mathcomp.ssreflect.path]
Paths.SubPath.e' [in mathcomp.ssreflect.path]
Paths.T [in mathcomp.ssreflect.path]
Paths.Transitive_in.leT_refl [in mathcomp.ssreflect.path]
Paths.Transitive_in.leT_tr [in mathcomp.ssreflect.path]
Paths.Transitive_in.leT [in mathcomp.ssreflect.path]
Paths.Transitive_in.P [in mathcomp.ssreflect.path]
Paths.Transitive.leT [in mathcomp.ssreflect.path]
Paths.Transitive.leT_refl [in mathcomp.ssreflect.path]
Paths.Transitive.leT_tr' [in mathcomp.ssreflect.path]
Paths.Transitive.leT_tr [in mathcomp.ssreflect.path]
PcoreDef.A [in mathcomp.solvable.pgroup]
PcoreDef.gT [in mathcomp.solvable.pgroup]
PcoreDef.pi [in mathcomp.solvable.pgroup]
PCoreProps.gT [in mathcomp.solvable.pgroup]
PCoreProps.pi [in mathcomp.solvable.pgroup]
Pdeg2.FieldMonic.Pdeg2FieldMonic.a [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.a1 [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.b [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.c [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.degp [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.delta [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.F [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.monicp [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.nz2 [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.p [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.r [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.r_sqrt_delta [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.r1 [in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.r2 [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.a [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.aa4 [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.aneq0 [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.a2neq0 [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.b [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.c [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.degp [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.delta [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.F [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.nz2 [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.p [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.pE [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.pneq0 [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.r [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.r_sqrt_delta [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.r1 [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.r2 [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.splitr [in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.sqa2neq0 [in mathcomp.algebra.poly]
Pdiv.ClosedField.closed.F [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.IDomainPseudoDivision.R [in mathcomp.algebra.polydiv]
Pdiv.CommonRing.RingPseudoDivision.R [in mathcomp.algebra.polydiv]
Pdiv.ComRing.CommutativeRingPseudoDivision.R [in mathcomp.algebra.polydiv]
Pdiv.Field.FieldDivision.F [in mathcomp.algebra.polydiv]
Pdiv.Field.FieldDivision.FieldMap.f [in mathcomp.algebra.polydiv]
Pdiv.Field.FieldDivision.FieldMap.rR [in mathcomp.algebra.polydiv]
Pdiv.Field.FieldDivision.FieldRingMap.f [in mathcomp.algebra.polydiv]
Pdiv.Field.FieldDivision.FieldRingMap.rR [in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.IDomainPseudoDivisionDefs.R [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.IdomainMonic.MonicDivisor.monq [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.IdomainMonic.MonicDivisor.q [in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.IdomainMonic.R [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.MoreUnitDivisor.d [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.MoreUnitDivisor.R [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.MoreUnitDivisor.ulcd [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.UnitDivisor.d [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.UnitDivisor.R [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.UnitDivisor.ulcd [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.ComRegDivisor.Cdl [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.ComRegDivisor.d [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.ComRegDivisor.R [in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.ComRegDivisor.Rreg [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.ComRingMonic.d [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.ComRingMonic.mond [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.ComRingMonic.R [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.RingMonic.MonicDivisor.d [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.RingMonic.MonicDivisor.mond [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.RingMonic.R [in mathcomp.algebra.polydiv]
Pdiv.Ring.ExtraMonicDivisor.R [in mathcomp.algebra.polydiv]
Pdiv.UnitRing.UnitRingPseudoDivision.R [in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.WeakTheoryForIDomainPseudoDivision.R [in mathcomp.algebra.polydiv]
PermAction.rT [in mathcomp.fingroup.action]
PermDefSection.T [in mathcomp.fingroup.perm]
PermIn.A [in mathcomp.fingroup.automorphism]
PermIn.f [in mathcomp.fingroup.automorphism]
PermIn.injf [in mathcomp.fingroup.automorphism]
PermIn.sBf [in mathcomp.fingroup.automorphism]
PermIn.T [in mathcomp.fingroup.automorphism]
PermSeq.T [in mathcomp.ssreflect.seq]
PermutationParity.T [in mathcomp.fingroup.perm]
Permutations.cons_permsE [in mathcomp.ssreflect.seq]
Permutations.permsP [in mathcomp.ssreflect.seq]
Permutations.T [in mathcomp.ssreflect.seq]
PervasiveMonoids.hb_instance_153.T [in mathcomp.ssreflect.bigop]
Pextraspecial.Construction.p [in mathcomp.solvable.extraspecial]
PgroupDefs.gT [in mathcomp.solvable.pgroup]
PgroupProps.gT [in mathcomp.solvable.pgroup]
PiAdditive.equivV [in mathcomp.algebra.ring_quotient]
PiAdditive.Q [in mathcomp.algebra.ring_quotient]
PiAdditive.V [in mathcomp.algebra.ring_quotient]
PiAdditive.zeroV [in mathcomp.algebra.ring_quotient]
PiRMorphism.equivR [in mathcomp.algebra.ring_quotient]
PiRMorphism.Q [in mathcomp.algebra.ring_quotient]
PiRMorphism.R [in mathcomp.algebra.ring_quotient]
PiRMorphism.zeroR [in mathcomp.algebra.ring_quotient]
Plain.op [in mathcomp.ssreflect.bigop]
Plain.R [in mathcomp.ssreflect.bigop]
Plain.x [in mathcomp.ssreflect.bigop]
Plogp.F [in mathcomp.field.qfpoly]
PmapSub.p [in mathcomp.ssreflect.seq]
PmapSub.sT [in mathcomp.ssreflect.seq]
PmapSub.T [in mathcomp.ssreflect.seq]
Pmap.aT [in mathcomp.ssreflect.seq]
Pmap.f [in mathcomp.ssreflect.seq]
Pmap.fK [in mathcomp.ssreflect.seq]
Pmap.g [in mathcomp.ssreflect.seq]
Pmap.rT [in mathcomp.ssreflect.seq]
PMax.gT [in mathcomp.solvable.maximal]
PMax.M [in mathcomp.solvable.maximal]
PMax.P [in mathcomp.solvable.maximal]
PMax.p [in mathcomp.solvable.maximal]
PMax.pP [in mathcomp.solvable.maximal]
PolyCompose.hb_instance_128.p [in mathcomp.algebra.poly]
PolyCompose.R [in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_202.q [in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_192.x [in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_184.x [in mathcomp.algebra.poly]
PolynomialComRing.HornerAlg.A [in mathcomp.algebra.poly]
PolynomialComRing.HornerAlg.Defs.a [in mathcomp.algebra.poly]
PolynomialComRing.HornerAlg.pf [in mathcomp.algebra.poly]
PolynomialComRing.R [in mathcomp.algebra.poly]
PolynomialIdomain.R [in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_103.n [in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_95.n [in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_82.zmodS [in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_67.i [in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_41.i [in mathcomp.algebra.poly]
PolynomialTheory.OnePrimitive.n [in mathcomp.algebra.poly]
PolynomialTheory.OnePrimitive.n_gt0 [in mathcomp.algebra.poly]
PolynomialTheory.OnePrimitive.prim_z [in mathcomp.algebra.poly]
PolynomialTheory.OnePrimitive.z [in mathcomp.algebra.poly]
PolynomialTheory.PolyOverAdd.S [in mathcomp.algebra.poly]
PolynomialTheory.PolyOverRing.S [in mathcomp.algebra.poly]
PolynomialTheory.PolyOverSemiring.S [in mathcomp.algebra.poly]
PolynomialTheory.PolyOverSemiRing2.S [in mathcomp.algebra.poly]
PolynomialTheory.R [in mathcomp.algebra.poly]
Polynomial.R [in mathcomp.algebra.poly]
PolyXY_Field.FtoE [in mathcomp.algebra.polyXY]
PolyXY_Field.E [in mathcomp.algebra.polyXY]
PolyXY_Field.F [in mathcomp.algebra.polyXY]
PolyXY_Idomain.R [in mathcomp.algebra.polyXY]
PolyXY_ComRing.R [in mathcomp.algebra.polyXY]
PolyXY_Ring.R [in mathcomp.algebra.polyXY]
PolyZintRing.R [in mathcomp.algebra.ssrint]
poly_of_size_zmod.npoly.n [in mathcomp.algebra.qpoly]
poly_of_size_zmod.poly_of_size.n [in mathcomp.algebra.qpoly]
Pquotient.G [in mathcomp.solvable.pgroup]
Pquotient.gT [in mathcomp.solvable.pgroup]
Pquotient.H [in mathcomp.solvable.pgroup]
Pquotient.K [in mathcomp.solvable.pgroup]
Pquotient.p [in mathcomp.solvable.pgroup]
Pquotient.pi [in mathcomp.solvable.pgroup]
Pquotient.piK [in mathcomp.solvable.pgroup]
PreClosedField.UseAxiom.closedF [in mathcomp.algebra.poly]
PreClosedField.UseAxiom.F [in mathcomp.algebra.poly]
Predicates.D [in mathcomp.character.classfun]
Predicates.gT [in mathcomp.character.classfun]
Predicates.R [in mathcomp.character.classfun]
Predicates.rT [in mathcomp.character.classfun]
PrefixSuffixInfix.T [in mathcomp.ssreflect.seq]
PreGroupIdentities.T [in mathcomp.fingroup.fingroup]
PreInSuffix.e [in mathcomp.ssreflect.path]
PreInSuffix.T [in mathcomp.ssreflect.path]
PrimeChar.FinField.charFp [in mathcomp.field.finfield]
PrimeChar.FinField.F0 [in mathcomp.field.finfield]
PrimeChar.FinRing.charRp [in mathcomp.field.finfield]
PrimeChar.FinRing.n [in mathcomp.field.finfield]
PrimeChar.FinRing.pr_p [in mathcomp.field.finfield]
PrimeChar.FinRing.R0 [in mathcomp.field.finfield]
PrimeChar.hb_instance_202.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_202.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_191.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_191.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_181.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_181.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_159.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_159.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_146.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_146.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_136.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_136.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_111.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_111.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_100.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_100.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_91.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_91.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_82.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_82.R [in mathcomp.field.finfield]
PrimeChar.hb_instance_73.charRp [in mathcomp.field.finfield]
PrimeChar.hb_instance_73.R [in mathcomp.field.finfield]
PrimeChar.p [in mathcomp.field.finfield]
PrimeChar.PrimeCharRing.charRp [in mathcomp.field.finfield]
PrimeChar.PrimeCharRing.natrFp [in mathcomp.field.finfield]
PrimeChar.PrimeCharRing.R0 [in mathcomp.field.finfield]
PrimeField.F_prime.p_pr [in mathcomp.algebra.zmodp]
PrimeField.p [in mathcomp.algebra.zmodp]
PrimeIdealr.EtaAndMixinExports.hb_instance_56.S [in mathcomp.algebra.ring_quotient]
PrimeIdealr.EtaAndMixinExports.hb_instance_56.R [in mathcomp.algebra.ring_quotient]
PrimeIdealTheory.pidealI [in mathcomp.algebra.ring_quotient]
PrimeIdealTheory.R [in mathcomp.algebra.ring_quotient]
PrimitiveDef.A [in mathcomp.solvable.primitive_action]
PrimitiveDef.aT [in mathcomp.solvable.primitive_action]
PrimitiveDef.S [in mathcomp.solvable.primitive_action]
PrimitiveDef.sT [in mathcomp.solvable.primitive_action]
PrimitiveDef.to [in mathcomp.solvable.primitive_action]
PrimitivePoly.F [in mathcomp.field.qfpoly]
PrimitivePoly.h [in mathcomp.field.qfpoly]
PrimitivePoly.Hh [in mathcomp.field.qfpoly]
PrimitivePoly.pred_card_qT_gt0 [in mathcomp.field.qfpoly]
PrimitivePoly.sh_gt1 [in mathcomp.field.qfpoly]
PrimitivePoly.sh_gt2 [in mathcomp.field.qfpoly]
Primitive.aT [in mathcomp.solvable.primitive_action]
Primitive.G [in mathcomp.solvable.primitive_action]
Primitive.S [in mathcomp.solvable.primitive_action]
Primitive.sT [in mathcomp.solvable.primitive_action]
Primitive.to [in mathcomp.solvable.primitive_action]
ProdEqType.T1 [in mathcomp.ssreflect.eqtype]
ProdEqType.T2 [in mathcomp.ssreflect.eqtype]
ProdFinType.T1 [in mathcomp.ssreflect.fintype]
ProdFinType.T2 [in mathcomp.ssreflect.fintype]
ProdMorph.Cprodm.cfHK [in mathcomp.fingroup.gproduct]
ProdMorph.Cprodm.eqfHK [in mathcomp.fingroup.gproduct]
ProdMorph.Cprodm.eqHK_G [in mathcomp.fingroup.gproduct]
ProdMorph.Cprodm.fH [in mathcomp.fingroup.gproduct]
ProdMorph.Cprodm.fK [in mathcomp.fingroup.gproduct]
ProdMorph.Cprodm.G [in mathcomp.fingroup.gproduct]
ProdMorph.Cprodm.H [in mathcomp.fingroup.gproduct]
ProdMorph.Cprodm.K [in mathcomp.fingroup.gproduct]
ProdMorph.defs.A [in mathcomp.fingroup.gproduct]
ProdMorph.defs.B [in mathcomp.fingroup.gproduct]
ProdMorph.defs.fA [in mathcomp.fingroup.gproduct]
ProdMorph.defs.fB [in mathcomp.fingroup.gproduct]
ProdMorph.Dprodm.cfHK [in mathcomp.fingroup.gproduct]
ProdMorph.Dprodm.eqHK_G [in mathcomp.fingroup.gproduct]
ProdMorph.Dprodm.fH [in mathcomp.fingroup.gproduct]
ProdMorph.Dprodm.fK [in mathcomp.fingroup.gproduct]
ProdMorph.Dprodm.G [in mathcomp.fingroup.gproduct]
ProdMorph.Dprodm.H [in mathcomp.fingroup.gproduct]
ProdMorph.Dprodm.K [in mathcomp.fingroup.gproduct]
ProdMorph.gT [in mathcomp.fingroup.gproduct]
ProdMorph.Props.actf [in mathcomp.fingroup.gproduct]
ProdMorph.Props.eqfHK [in mathcomp.fingroup.gproduct]
ProdMorph.Props.fH [in mathcomp.fingroup.gproduct]
ProdMorph.Props.fK [in mathcomp.fingroup.gproduct]
ProdMorph.Props.H [in mathcomp.fingroup.gproduct]
ProdMorph.Props.K [in mathcomp.fingroup.gproduct]
ProdMorph.Props.nHK [in mathcomp.fingroup.gproduct]
ProdMorph.rT [in mathcomp.fingroup.gproduct]
ProdMorph.Sdprodm.actf [in mathcomp.fingroup.gproduct]
ProdMorph.Sdprodm.eqHK_G [in mathcomp.fingroup.gproduct]
ProdMorph.Sdprodm.fH [in mathcomp.fingroup.gproduct]
ProdMorph.Sdprodm.fK [in mathcomp.fingroup.gproduct]
ProdMorph.Sdprodm.G [in mathcomp.fingroup.gproduct]
ProdMorph.Sdprodm.H [in mathcomp.fingroup.gproduct]
ProdMorph.Sdprodm.K [in mathcomp.fingroup.gproduct]
Product.G [in mathcomp.character.classfun]
Product.gT [in mathcomp.character.classfun]
Product.gT [in mathcomp.solvable.center]
ProdVector.R [in mathcomp.algebra.vector]
ProdVector.vT1 [in mathcomp.algebra.vector]
ProdVector.vT2 [in mathcomp.algebra.vector]
Projection.K [in mathcomp.algebra.vector]
Projection.Sumv_Pi.defV [in mathcomp.algebra.vector]
Projection.Sumv_Pi.V [in mathcomp.algebra.vector]
Projection.Sumv_Pi.sumv_pi_rec [in mathcomp.algebra.vector]
Projection.Sumv_Pi.Vs [in mathcomp.algebra.vector]
Projection.Sumv_Pi.P [in mathcomp.algebra.vector]
Projection.Sumv_Pi.r0 [in mathcomp.algebra.vector]
Projection.Sumv_Pi.I [in mathcomp.algebra.vector]
Projection.vT [in mathcomp.algebra.vector]
ProperIdeal.EtaAndMixinExports.hb_instance_45.S [in mathcomp.algebra.ring_quotient]
ProperIdeal.EtaAndMixinExports.hb_instance_45.R [in mathcomp.algebra.ring_quotient]
PropertiesDefs.A [in mathcomp.solvable.nilpotent]
PropertiesDefs.gT [in mathcomp.solvable.nilpotent]
Proper.aT [in mathcomp.field.falgebra]
Proper.R [in mathcomp.field.falgebra]
PseriesDefs.A [in mathcomp.solvable.pgroup]
PseriesDefs.gT [in mathcomp.solvable.pgroup]
PseriesDefs.pis [in mathcomp.solvable.pgroup]
| 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 | (100113 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 | (1864 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 | (49278 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 | (1631 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 | (6978 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 | (94 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 | (14781 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 | (75 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 | (222 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 | (131 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 | (2030 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 | (2189 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 | (1149 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 | (19126 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 | (565 entries) |