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 (24947 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 (1496 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 (216 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 (3586 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 (84 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 (11878 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 (389 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 (49 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 (119 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 (272 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 (1128 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 (701 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 (4837 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 (192 entries)

P (abbreviation)

p [in mathcomp.algebra.zmodp]
p [in mathcomp.algebra.zmodp]
P [in mathcomp.ssreflect.finset]
perm [in mathcomp.fingroup.perm]
perm_def [in mathcomp.fingroup.perm]
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]
ph [in mathcomp.ssreflect.ssrbool]
ph [in mathcomp.ssreflect.ssrbool]
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]
pprod [in mathcomp.fingroup.gproduct]
pprod [in mathcomp.fingroup.gproduct]
pQtoC [in mathcomp.field.algC]
pQtoC [in mathcomp.field.cyclotomic]
pQtoC [in mathcomp.field.algnum]
predn [in mathcomp.ssreflect.ssrnat]
predOfType [in mathcomp.ssreflect.finset]
pred_class [in mathcomp.ssreflect.ssrbool]
pred_of_set [in mathcomp.ssreflect.finset]
pred_of_set_def [in mathcomp.ssreflect.finset]
pT [in mathcomp.fingroup.perm]
Px [in mathcomp.field.galois]
pZtoC [in mathcomp.field.algC]
pZtoC [in mathcomp.field.cyclotomic]
pZtoC [in mathcomp.field.algnum]
pZtoQ [in mathcomp.field.algC]
pZtoQ [in mathcomp.algebra.intdiv]
pZtoQ [in mathcomp.field.cyclotomic]
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 (24947 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 (1496 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 (216 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 (3586 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 (84 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 (11878 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 (389 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 (49 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 (119 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 (272 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 (1128 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 (701 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 (4837 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 (192 entries)