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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)

P (definition)

p [in extremal]
pack_subFinType [in fintype]
pack_subCountType [in choice]
pairg1 [in gproduct]
pairg1_morphism [in gproduct]
pairmap [in seq]
pairmap_tuple [in tuple]
pair_of_sd [in gproduct]
pair_of_section [in jordanholder]
pair_eq [in eqtype]
pair_of_mxvec_index [in matrix]
pair_of_tag [in choice]
pair1g [in gproduct]
pair1g_morphism [in gproduct]
partial_product [in gproduct]
partition [in finset]
partn [in prime]
path [in path]
path_setIgr [in gseries]
pcancel [in ssrfun]
PcanChoiceMixin [in choice]
PcanCountMixin [in choice]
PcanEqMixin [in eqtype]
PcanFinMixin [in fintype]
pcomp [in ssrfun]
pcore [in pgroup]
pcore_pgFun [in pgroup]
pcore_gFun [in pgroup]
pcore_igFun [in pgroup]
pcore_mod_group [in pgroup]
pcore_group [in pgroup]
pcore_mod [in pgroup]
pcycle [in perm]
pcycles [in perm]
pdiv [in prime]
pE [in mxabelem]
pElem [in abelian]
PermDef.fun_of_perm [in perm]
PermDef.perm [in perm]
perm_mx [in matrix]
perm_on [in perm]
perm_of_finGroupType [in perm]
perm_of_baseFinGroupType [in perm]
perm_finGroupType [in perm]
perm_baseFinGroupType [in perm]
perm_unlock [in perm]
perm_for_subFinType [in perm]
perm_for_finType [in perm]
perm_for_subCountType [in perm]
perm_for_countType [in perm]
perm_for_choiceType [in perm]
perm_for_eqType [in perm]
perm_for_subType [in perm]
perm_subFinType [in perm]
perm_finType [in perm]
perm_subCountType [in perm]
perm_countType [in perm]
perm_choiceType [in perm]
perm_eqType [in perm]
perm_subType [in perm]
perm_finMixin [in perm]
perm_countMixin [in perm]
perm_inv [in perm]
perm_one [in perm]
perm_in [in automorphism]
perm_choiceMixin [in perm]
perm_eq [in seq]
perm_eqMixin [in perm]
perm_of [in perm]
perm_mul [in perm]
perm_action [in action]
perm_of_baseFinGroupMixin [in perm]
Pextraspecial.act [in extraspecial]
Pextraspecial.action [in extraspecial]
Pextraspecial.groupAction [in extraspecial]
Pextraspecial.gtype [in extraspecial]
Pextraspecial.ngtype [in extraspecial]
Pextraspecial.ngtypeQ [in extraspecial]
pfactor [in prime]
pfamily [in finfun]
pffun_on [in finfun]
pgroup [in pgroup]
pHall [in pgroup]
phant_id [in ssrfun]
phi [in prime]
pick [in fintype]
pickle [in choice]
pickle_inv [in choice]
pid_mx [in matrix]
pinvmx [in mxalgebra]
pi_arg_of_fin_pred [in prime]
pi_arg_of_nat [in prime]
pi_of [in prime]
pi_wrapped_arg [in prime]
pi_unwrapped_arg [in prime]
pmap [in seq]
pmaxElem [in abelian]
pnat [in prime]
pnElem [in abelian]
Poly [in poly]
polyC [in poly]
polyC_rmorphism [in poly]
polyC_additive [in poly]
polynomial_idomainType [in poly]
polynomial_comUnitRingType [in poly]
polynomial_unitAlgType [in poly]
polynomial_unitRingType [in poly]
polynomial_algType [in poly]
polynomial_comRingType [in poly]
polynomial_lalgType [in poly]
polynomial_lmodType [in poly]
polynomial_ringType [in poly]
polynomial_zmodType [in poly]
polynomial_choiceType [in poly]
polynomial_eqType [in poly]
polynomial_subType [in poly]
polynomial_choiceMixin [in poly]
polynomial_eqMixin [in poly]
polyX [in poly]
poly_unit [in poly]
poly_unitRingMixin [in poly]
poly_of [in poly]
poly_comp_rmorphism [in poly]
poly_comp_linear [in poly]
poly_comp_additive [in poly]
poly_idomainType [in poly]
poly_comUnitRingType [in poly]
poly_unitAlgType [in poly]
poly_unitRingType [in poly]
poly_algType [in poly]
poly_comRingType [in poly]
poly_lalgType [in poly]
poly_lmodType [in poly]
poly_lmodMixin [in poly]
poly_ringType [in poly]
poly_zmodType [in poly]
poly_choiceType [in poly]
poly_eqType [in poly]
poly_subType [in poly]
poly_cons [in poly]
poly_rV [in mxpoly]
poly_inv [in poly]
poly_comp [in poly]
poly_zmodMixin [in poly]
poly_rV_linear [in mxpoly]
poly_rV_additive [in mxpoly]
poly_ringMixin [in poly]
pop_succn [in ssrnat]
pos_of_nat [in ssrnat]
powerset [in finfun]
powers_mx [in mxpoly]
pprodm [in gproduct]
pprodm_morphism [in gproduct]
pred [in ssrbool]
predArgType [in ssrbool]
predC [in ssrbool]
predC1 [in eqtype]
predD [in ssrbool]
predD1 [in eqtype]
predI [in ssrbool]
predn [in ssrnat]
predPredType [in ssrbool]
predT [in ssrbool]
predU [in ssrbool]
predU1 [in eqtype]
predX [in eqtype]
pred_of_set_unlock [in finset]
pred_of_eq_seq [in seq]
pred_of_mem_pred [in ssrbool]
pred_of_argType [in ssrbool]
pred_of_mem [in ssrbool]
pred_of_simpl [in ssrbool]
pred0 [in ssrbool]
pred0b [in fintype]
pred1 [in eqtype]
pred2 [in eqtype]
pred3 [in eqtype]
pred4 [in eqtype]
preim [in ssrbool]
preimset [in finset]
preim_at [in finset]
preim_partition [in finset]
preim_seq [in fintype]
Presentation.and_rel [in presentation]
Presentation.bool_of_rel [in presentation]
Presentation.Cast [in presentation]
Presentation.env1 [in presentation]
Presentation.Eq1 [in presentation]
Presentation.Eq3 [in presentation]
Presentation.eval [in presentation]
Presentation.hom [in presentation]
Presentation.iso [in presentation]
Presentation.rel [in presentation]
Presentation.sat [in presentation]
prev [in path]
prev_at [in path]
pre_symmetric [in ssrbool]
prime [in prime]
primes [in prime]
prime_decomp [in prime]
prime_decomp_rec [in prime]
primitive [in primitive_action]
primitive_root_of_unity [in poly]
principal_comp [in mxrepresentation]
prodVector [in vector]
prod_group [in gproduct]
prod_finType [in fintype]
prod_countMixin [in choice]
prod_choiceMixin [in choice]
prod_eqMixin [in eqtype]
prod_finMixin [in fintype]
prod_eqType [in eqtype]
prod_countType [in choice]
prod_choiceType [in choice]
prod_enum [in fintype]
projv [in vector]
proj_mx [in mxalgebra]
proper [in fintype]
proper_mxsumP [in mxalgebra]
proper_addvP [in vector]
prop_in3 [in ssrbool]
prop_in111 [in ssrbool]
prop_in21 [in ssrbool]
prop_on1 [in ssrbool]
prop_in12 [in ssrbool]
prop_for [in ssrbool]
prop_on2 [in ssrbool]
prop_in11 [in ssrbool]
prop_in1 [in ssrbool]
prop_in2 [in ssrbool]
protect_term [in ssreflect]
pseries [in pgroup]
pseries_pgFun [in pgroup]
pseries_gFun [in pgroup]
pseries_igFun [in pgroup]
pseries_group [in pgroup]
psubgroup [in pgroup]
pval [in perm]
pvf [in vector]
pv2p [in vector]
pZ [in maximal]
p_group [in pgroup]
p_elt [in pgroup]
p_rank [in abelian]
p_gt1 [in maximal]
p_gt0 [in mxabelem]
p_gt1 [in mxabelem]
p_gt0 [in maximal]
p_pr [in mxabelem]
p_gt1 [in extremal]
p_pr [in maximal]
p_gt1 [in extraspecial]
p_pr [in maximal]
p_gt0 [in extremal]
p_pr [in mxabelem]
p_gt0 [in extraspecial]
p2pv [in vector]



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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)