| 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) | -
P (definition)
-pack_subCountType [in mathcomp.ssreflect.choice]-pack_subFinType [in mathcomp.ssreflect.fintype]
-pairg1 [in mathcomp.fingroup.gproduct]
-pairmap [in mathcomp.ssreflect.seq]
-pairwise_orthogonal [in mathcomp.character.classfun]
-pair_unitRingMixin [in mathcomp.algebra.ssralg]
-pair_invr [in mathcomp.algebra.ssralg]
-pair_unitr [in mathcomp.algebra.ssralg]
-pair_lmodMixin [in mathcomp.algebra.ssralg]
-pair_ringMixin [in mathcomp.algebra.ssralg]
-pair_zmodMixin [in mathcomp.algebra.ssralg]
-pair_vectMixin [in mathcomp.algebra.vector]
-pair_of_tag [in mathcomp.ssreflect.choice]
-pair_ortho_rec [in mathcomp.character.classfun]
-pair_eq [in mathcomp.ssreflect.eqtype]
-pair1g [in mathcomp.fingroup.gproduct]
-partial_product [in mathcomp.fingroup.gproduct]
-partition [in mathcomp.ssreflect.finset]
-partn [in mathcomp.ssreflect.prime]
-path [in mathcomp.ssreflect.path]
-pblock [in mathcomp.ssreflect.finset]
-PcanCountMixin [in mathcomp.ssreflect.choice]
-PcanEqMixin [in mathcomp.ssreflect.eqtype]
-PcanFinMixin [in mathcomp.ssreflect.fintype]
-pcore [in mathcomp.solvable.pgroup]
-pcore_mod [in mathcomp.solvable.pgroup]
-pcycle [in mathcomp.fingroup.perm]
-pcycles [in mathcomp.fingroup.perm]
-pdiv [in mathcomp.ssreflect.prime]
-Pdiv.CommonIdomain.apply_irredp [in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep [in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.egcdp [in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.egcdp_rec [in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp [in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_rec [in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gdcop [in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gdcop_rec [in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.irreducible_poly [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rcoprimep [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdivp [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvdp [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.redivp [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.redivp_expanded_def [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.redivp_rec [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgcdp [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgdcop [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgdcop_rec [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodp [in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rscalp [in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.divp [in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.dvdp [in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.edivp [in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.edivp_expanded_def [in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.eqp [in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.modp [in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.scalp [in mathcomp.algebra.polydiv]
-pElem [in mathcomp.solvable.abelian]
-PermDef.fun_of_perm [in mathcomp.fingroup.perm]
-PermDef.perm [in mathcomp.fingroup.perm]
-perms_rec [in mathcomp.ssreflect.seq]
-permutations [in mathcomp.ssreflect.seq]
-perm_on [in mathcomp.fingroup.perm]
-perm_of_baseFinGroupMixin [in mathcomp.fingroup.perm]
-perm_mul [in mathcomp.fingroup.perm]
-perm_inv [in mathcomp.fingroup.perm]
-perm_one [in mathcomp.fingroup.perm]
-perm_finMixin [in mathcomp.fingroup.perm]
-perm_countMixin [in mathcomp.fingroup.perm]
-perm_choiceMixin [in mathcomp.fingroup.perm]
-perm_eqMixin [in mathcomp.fingroup.perm]
-perm_of [in mathcomp.fingroup.perm]
-perm_mx [in mathcomp.algebra.matrix]
-perm_in [in mathcomp.fingroup.automorphism]
-perm_eq [in mathcomp.ssreflect.seq]
-Pextraspecial.act [in mathcomp.solvable.extraspecial]
-Pextraspecial.groupAction [in mathcomp.solvable.extraspecial]
-Pextraspecial.gtype [in mathcomp.solvable.extraspecial]
-Pextraspecial.ngtype [in mathcomp.solvable.extraspecial]
-Pextraspecial.ngtypeQ [in mathcomp.solvable.extraspecial]
-pfactor [in mathcomp.ssreflect.prime]
-pfamily_mem [in mathcomp.ssreflect.finfun]
-pffun_on_mem [in mathcomp.ssreflect.finfun]
-pgroup [in mathcomp.solvable.pgroup]
-pHall [in mathcomp.solvable.pgroup]
-pick [in mathcomp.ssreflect.fintype]
-pickle [in mathcomp.ssreflect.choice]
-pickle_tagged [in mathcomp.ssreflect.choice]
-pickle_seq [in mathcomp.ssreflect.choice]
-pickle_inv [in mathcomp.ssreflect.choice]
-pick_true [in mathcomp.ssreflect.fintype]
-pid_mx [in mathcomp.algebra.matrix]
-pinvmx [in mathcomp.algebra.mxalgebra]
-pi_of [in mathcomp.ssreflect.prime]
-pi_arg [in mathcomp.ssreflect.prime]
-pi_phant [in mathcomp.ssreflect.generic_quotient]
-Pi.E [in mathcomp.ssreflect.generic_quotient]
-Pi.f [in mathcomp.ssreflect.generic_quotient]
-pmap [in mathcomp.ssreflect.seq]
-pmaxElem [in mathcomp.solvable.abelian]
-pnat [in mathcomp.ssreflect.prime]
-pnElem [in mathcomp.solvable.abelian]
-poly [in mathcomp.algebra.poly]
-Poly [in mathcomp.algebra.poly]
-polyC [in mathcomp.algebra.poly]
-polynomial_choiceMixin [in mathcomp.algebra.poly]
-polynomial_eqMixin [in mathcomp.algebra.poly]
-polyOver [in mathcomp.algebra.poly]
-polyX [in mathcomp.algebra.poly]
-polyX_def [in mathcomp.algebra.poly]
-poly_rV [in mathcomp.algebra.mxpoly]
-poly_XmY [in mathcomp.algebra.polyXY]
-poly_XaY [in mathcomp.algebra.polyXY]
-poly_comUnitMixin [in mathcomp.algebra.poly]
-poly_inv [in mathcomp.algebra.poly]
-poly_unit [in mathcomp.algebra.poly]
-poly_lmodMixin [in mathcomp.algebra.poly]
-poly_ringMixin [in mathcomp.algebra.poly]
-poly_zmodMixin [in mathcomp.algebra.poly]
-poly_expanded_def [in mathcomp.algebra.poly]
-poly_nil [in mathcomp.algebra.poly]
-poly_countMixin [in mathcomp.algebra.poly]
-poly_of [in mathcomp.algebra.poly]
-pop_succn [in mathcomp.ssreflect.ssrnat]
-pos_of_nat [in mathcomp.ssreflect.ssrnat]
-powerset [in mathcomp.ssreflect.finset]
-powers_mx [in mathcomp.algebra.mxpoly]
-pprodm [in mathcomp.fingroup.gproduct]
-predC1 [in mathcomp.ssreflect.eqtype]
-predD1 [in mathcomp.ssreflect.eqtype]
-PredType [in mathcomp.ssreflect.ssrbool]
-predU1 [in mathcomp.ssreflect.eqtype]
-predX [in mathcomp.ssreflect.eqtype]
-pred_of_vspace [in mathcomp.algebra.vector]
-pred_of_itv [in mathcomp.algebra.interval]
-pred_Nirr [in mathcomp.character.character]
-pred0b [in mathcomp.ssreflect.fintype]
-pred1 [in mathcomp.ssreflect.eqtype]
-pred2 [in mathcomp.ssreflect.eqtype]
-pred3 [in mathcomp.ssreflect.eqtype]
-pred4 [in mathcomp.ssreflect.eqtype]
-preimset [in mathcomp.ssreflect.finset]
-preim_seq [in mathcomp.ssreflect.fintype]
-preim_partition [in mathcomp.ssreflect.finset]
-Presentation.and_rel [in mathcomp.fingroup.presentation]
-Presentation.bool_of_rel [in mathcomp.fingroup.presentation]
-Presentation.Cast [in mathcomp.fingroup.presentation]
-Presentation.env1 [in mathcomp.fingroup.presentation]
-Presentation.Eq1 [in mathcomp.fingroup.presentation]
-Presentation.Eq3 [in mathcomp.fingroup.presentation]
-Presentation.eval [in mathcomp.fingroup.presentation]
-Presentation.hom [in mathcomp.fingroup.presentation]
-Presentation.iso [in mathcomp.fingroup.presentation]
-Presentation.rel [in mathcomp.fingroup.presentation]
-Presentation.sat [in mathcomp.fingroup.presentation]
-prev [in mathcomp.ssreflect.path]
-prev_at [in mathcomp.ssreflect.path]
-prime [in mathcomp.ssreflect.prime]
-PrimeCharType [in mathcomp.field.finfield]
-primeChar_vectMixin [in mathcomp.field.finfield]
-primeChar_lmodMixin [in mathcomp.field.finfield]
-primeChar_scale [in mathcomp.field.finfield]
-PrimeDecompAux.add_totient_factor [in mathcomp.ssreflect.prime]
-PrimeDecompAux.add_divisors [in mathcomp.ssreflect.prime]
-PrimeDecompAux.cons_pfactor [in mathcomp.ssreflect.prime]
-PrimeDecompAux.edivn2 [in mathcomp.ssreflect.prime]
-PrimeDecompAux.elogn2 [in mathcomp.ssreflect.prime]
-PrimeDecompAux.ifnz [in mathcomp.ssreflect.prime]
-primes [in mathcomp.ssreflect.prime]
-prime_decomp [in mathcomp.ssreflect.prime]
-prime_decomp_rec [in mathcomp.ssreflect.prime]
-prime_idealr_closed [in mathcomp.algebra.ring_quotient]
-primitive [in mathcomp.solvable.primitive_action]
-primitive_root_of_unity [in mathcomp.algebra.poly]
-principal_comp [in mathcomp.character.mxrepresentation]
-principal_comp_def [in mathcomp.character.mxrepresentation]
-prodv [in mathcomp.field.falgebra]
-prod_repr [in mathcomp.character.character]
-prod_countMixin [in mathcomp.ssreflect.choice]
-prod_choiceMixin [in mathcomp.ssreflect.choice]
-prod_finMixin [in mathcomp.ssreflect.fintype]
-prod_enum [in mathcomp.ssreflect.fintype]
-prod_tuple [in mathcomp.solvable.burnside_app]
-projv [in mathcomp.algebra.vector]
-proj_mx [in mathcomp.algebra.mxalgebra]
-proper [in mathcomp.ssreflect.fintype]
-proper_addvP [in mathcomp.algebra.vector]
-proper_ideal [in mathcomp.algebra.ring_quotient]
-proper_mxsumP [in mathcomp.algebra.mxalgebra]
-pseries [in mathcomp.solvable.pgroup]
-psubgroup [in mathcomp.solvable.pgroup]
-purely_inseparable [in mathcomp.field.separable]
-purely_inseparable_element [in mathcomp.field.separable]
-pval [in mathcomp.fingroup.perm]
-p_elt [in mathcomp.solvable.pgroup]
-p_group [in mathcomp.solvable.pgroup]
-p_rank [in mathcomp.solvable.abelian]
-
| 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) | -