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 (75489 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 (1813 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 (45320 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 (382 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 (3967 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 (14046 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 (469 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 (128 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 (457 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 (1372 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 (1025 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 (6124 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 (250 entries)

P (abbreviation)

p [in mathcomp.algebra.zmodp]
p [in mathcomp.algebra.zmodp]
P [in mathcomp.ssreflect.finset]
path [in mathcomp.ssreflect.path]
pcycle [in mathcomp.fingroup.perm]
pcycleE [in mathcomp.fingroup.action]
pcycles [in mathcomp.fingroup.perm]
pcycle_perm [in mathcomp.fingroup.perm]
pcycle_sym [in mathcomp.fingroup.perm]
pcycle_traject [in mathcomp.fingroup.perm]
pcycle_id [in mathcomp.fingroup.perm]
pcycle_actperm [in mathcomp.fingroup.action]
Pdiv.CommonIdomain.coprimep_mulr [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_mull [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_scaler [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_scalel [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_opp [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_scaler [in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_scalel [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_add [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_opp [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_scaler [in mathcomp.algebra.polydiv]
Pdiv.Field.divp_scalel [in mathcomp.algebra.polydiv]
Pdiv.Field.modp_add [in mathcomp.algebra.polydiv]
Pdiv.Field.modp_opp [in mathcomp.algebra.polydiv]
Pdiv.Field.modp_scaler [in mathcomp.algebra.polydiv]
Pdiv.Field.modp_scalel [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_add [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_opp [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_scaler [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_scalel [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modp_add [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modp_opp [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modp_scaler [in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modp_scalel [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_addr [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_addl [in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_add [in mathcomp.algebra.polydiv]
perm [in mathcomp.fingroup.perm]
perms [in mathcomp.ssreflect.seq]
perm_def [in mathcomp.fingroup.perm]
perm_allpairs_rconsr [in mathcomp.ssreflect.seq]
perm_tseq [in mathcomp.ssreflect.seq]
perm_eqr [in mathcomp.ssreflect.seq]
perm_eql [in mathcomp.ssreflect.seq]
perm_eqr [in mathcomp.ssreflect.seq]
perm_eql [in mathcomp.ssreflect.seq]
pfamily [in mathcomp.ssreflect.finfun]
pffun_on [in mathcomp.ssreflect.finfun]
pFtoE [in mathcomp.algebra.polyXY]
PiConst [in mathcomp.ssreflect.generic_quotient]
piE [in mathcomp.ssreflect.generic_quotient]
PiEmbed [in mathcomp.ssreflect.generic_quotient]
PiMono1 [in mathcomp.ssreflect.generic_quotient]
PiMono2 [in mathcomp.ssreflect.generic_quotient]
PiMorph [in mathcomp.ssreflect.generic_quotient]
PiMorph1 [in mathcomp.ssreflect.generic_quotient]
PiMorph11 [in mathcomp.ssreflect.generic_quotient]
PiMorph2 [in mathcomp.ssreflect.generic_quotient]
pnat_exp [in mathcomp.ssreflect.prime]
pnat_mul [in mathcomp.ssreflect.prime]
polyC_mulrz [in mathcomp.algebra.ssrint]
polyC_inv [in mathcomp.algebra.poly]
polyC_mul [in mathcomp.algebra.poly]
polyC_muln [in mathcomp.algebra.poly]
polyC_sub [in mathcomp.algebra.poly]
polyC_opp [in mathcomp.algebra.poly]
polyC_add [in mathcomp.algebra.poly]
pprod [in mathcomp.fingroup.gproduct]
pprod [in mathcomp.fingroup.gproduct]
pQtoC [in mathcomp.field.cyclotomic]
pQtoC [in mathcomp.field.algC]
pQtoC [in mathcomp.field.algnum]
predn [in mathcomp.ssreflect.ssrnat]
predOfType [in mathcomp.ssreflect.finset]
pred_of_set [in mathcomp.ssreflect.finset]
pred_of_set_def [in mathcomp.ssreflect.finset]
primes_exp [in mathcomp.ssreflect.prime]
primes_mul [in mathcomp.ssreflect.prime]
pT [in mathcomp.fingroup.perm]
Px [in mathcomp.field.galois]
pZtoC [in mathcomp.field.cyclotomic]
pZtoC [in mathcomp.field.algC]
pZtoC [in mathcomp.field.algnum]
pZtoQ [in mathcomp.algebra.intdiv]
pZtoQ [in mathcomp.field.cyclotomic]
pZtoQ [in mathcomp.field.algC]
pZtoQ [in mathcomp.field.algnum]
p_A [in mathcomp.algebra.mxpoly]



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 (75489 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 (1813 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 (45320 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 (382 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 (3967 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 (14046 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 (469 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 (128 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 (457 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 (1372 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 (1025 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 (6124 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 (250 entries)