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 _ (6599 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 _ (86 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 _ (57 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 _ (3455 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 _ (290 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 _ (147 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 _ (148 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 _ (53 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 _ (1466 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 _ (28 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 _ (53 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 _ (788 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 _ (28 entries)

P (lemma)

pairmapK [in seq]
pairmap_tupleP [in tuple]
pair_big [in bigops]
pair_bigA [in bigops]
pair_big_dep [in bigops]
pair_eqE [in eqtype]
pair_eqP [in eqtype]
pair_eq1 [in eqtype]
pair_eq2 [in eqtype]
pair_of_tagK [in choice]
partition_big [in bigops]
partition_big_imset [in finset]
partnC [in prime]
partnI [in prime]
partnNK [in prime]
partnT [in prime]
partn0 [in prime]
partn1 [in prime]
partn_dvd [in prime]
partn_exp [in prime]
partn_mul [in prime]
partn_part [in prime]
partn_pi [in prime]
part_gt0 [in prime]
part_pnat [in prime]
part_p'nat [in prime]
pascal [in binomial]
pastemxEl [in matrix]
pastemxEr [in matrix]
pastemxKl [in matrix]
pastemxKr [in matrix]
pastemx0 [in matrix]
paste_mx_col' [in matrix]
pathP [in paths]
path_cat [in paths]
path_connect [in connect]
path_map [in paths]
path_merge [in paths]
path_sorted [in paths]
pcan_enumP [in fintype]
pcan_inj [in ssrfun]
pcan_pcomp [in ssrfun]
pcan_pickleK [in choice]
pcycle_id [in perm]
pcycle_perm [in perm]
pcycle_sym [in perm]
pcycle_traject [in perm]
pdivP [in prime]
pdiv_gt0 [in prime]
pdiv_min_dvd [in prime]
PermDef.fun_of_permE [in perm]
PermDef.permE [in perm]
permE [in perm]
permJ [in perm]
permK [in perm]
permKV [in perm]
permM [in perm]
permP [in perm]
permX [in perm]
perm1 [in perm]
perm_catAC [in seq]
perm_catC [in seq]
perm_catCA [in seq]
perm_cat2l [in seq]
perm_cat2r [in seq]
perm_closed [in perm]
perm_cons [in seq]
perm_eqlP [in seq]
perm_eqP [in seq]
perm_eqrP [in seq]
perm_eq_mem [in seq]
perm_eq_refl [in seq]
perm_eq_size [in seq]
perm_eq_sym [in seq]
perm_eq_trans [in seq]
perm_eq_uniq [in seq]
perm_inE [in automorphism]
perm_inj [in perm]
perm_invK [in perm]
perm_invP [in perm]
perm_in_inj [in automorphism]
perm_in_on [in automorphism]
perm_merge [in paths]
perm_mulP [in perm]
perm_mxV [in matrix]
perm_mx1 [in matrix]
perm_mx_is_perm [in matrix]
perm_oneP [in perm]
perm_onM [in perm]
perm_onto [in perm]
perm_on1 [in perm]
perm_proof [in perm]
perm_rcons [in seq]
perm_rot [in seq]
perm_rotr [in seq]
perm_sort [in paths]
perm_sortP [in paths]
perm_uniq [in seq]
pfactorK [in prime]
pfactor_coprime [in prime]
pfactor_dvdn [in prime]
pfactor_dvdnn [in prime]
pfactor_gt0 [in prime]
pfamilyP [in finfun]
pffun_onP [in finfun]
phiE [in prime]
phi_add [in charpoly]
phi_coprime [in prime]
phi_count_coprime [in prime]
phi_gen [in cyclic]
phi_gt0 [in prime]
phi_mul [in charpoly]
phi_one [in charpoly]
phi_opp [in charpoly]
phi_pfactor [in prime]
phi_polyC [in charpoly]
phi_zero [in charpoly]
phi_Zpoly [in charpoly]
pickleK [in choice]
pickleK_inv [in choice]
pickle_invK [in choice]
pickP [in fintype]
pi_of_exp [in prime]
pi_of_prime [in prime]
plusE [in ssrnat]
pmapS_filter [in seq]
pmap_filter [in seq]
pmap_sub_uniq [in seq]
pmap_uniq [in seq]
pnatE [in prime]
pnatI [in prime]
pnatNK [in prime]
pnatP [in prime]
pnat_coprime [in prime]
pnat_div [in prime]
pnat_dvd [in prime]
pnat_exp [in prime]
pnat_id [in prime]
pnat_mul [in prime]
pnat_part [in prime]
pnat_pi [in prime]
pnat_1 [in prime]
polyC0 [in poly]
polyC1 [in poly]
polyC_add [in poly]
polyC_eq0 [in poly]
polyC_exp [in poly]
polyC_inj [in poly]
polyC_mul [in poly]
polyC_natmul [in poly]
polyC_opp [in poly]
polyC_sub [in poly]
PolyK [in poly]
polyP [in poly]
polyseqC [in poly]
polyseqK [in poly]
polyseqX [in poly]
polyseq1 [in poly]
polyseq_cons [in poly]
polyseq_poly [in poly]
polySpred [in poly]
poly0Vpos [in poly]
poly_cons_def [in poly]
poly_def [in poly]
poly_idomainMixin [in poly]
poly_ind [in poly]
poly_inj [in poly]
poly_intro_unit [in poly]
poly_inv_out [in poly]
poly_mulC [in poly]
poly_mulVp [in poly]
posnP [in ssrnat]
pos_natP [in ssrnat]
predC_closed [in connect]
predD1P [in eqtype]
predE [in ssrnat]
prednK [in ssrnat]
predT_subset [in fintype]
predU1l [in eqtype]
predU1P [in eqtype]
predU1r [in eqtype]
predX_prod_enum [in fintype]
pred0P [in fintype]
pred0Pn [in fintype]
pred1E [in eqtype]
pred2P [in eqtype]
preimsetC [in finset]
preimsetD [in finset]
preimsetI [in finset]
preimsetS [in finset]
preimsetT [in finset]
preimsetU [in finset]
preimset0 [in finset]
preimset_proper [in finset]
preim_autE [in automorphism]
preim_iinv [in fintype]
preim_partitionP [in finset]
prev_cycle [in paths]
prev_map [in paths]
prev_next [in paths]
prev_nth [in paths]
prev_rev [in paths]
prev_rot [in paths]
prev_rotr [in paths]
pre_image [in fintype]
primeP [in prime]
primePn [in prime]
primePns [in prime]
primes_exp [in prime]
primes_mul [in prime]
primes_part [in prime]
primes_pdiv [in prime]
primes_prime [in prime]
primes_uniq [in prime]
prime_coprime [in prime]
prime_cyclic [in cyclic]
prime_decompE [in prime]
prime_decomp_correct [in prime]
prime_gt0 [in prime]
prime_gt1 [in prime]
prime_pdiv [in prime]
prodn_cond_gt0 [in bigops]
prodn_gt0 [in bigops]
prod_enumP [in fintype]
prod_nat_const [in bigops]
prod_nat_const_nat [in bigops]
prod_prime_decomp [in prime]
prod_tpermP [in perm]
properD [in finset]
properD1 [in finset]
properE [in fintype]
properEcard [in finset]
properEneq [in finset]
properI [in finset]
properIl [in finset]
properIr [in finset]
properIset [in finset]
properP [in fintype]
properU [in finset]
properUl [in finset]
properUr [in finset]
proper0 [in finset]
proper1G [in groups]
proper1set [in finset]
proper_card [in fintype]
proper_irrefl [in fintype]
proper_neq [in finset]
proper_sub [in fintype]
proper_subn [in fintype]
proper_sub_trans [in fintype]
proper_trans [in fintype]
prop_congr [in ssrbool]
pvalE [in perm]
p'natE [in prime]
p_natP [in prime]
p_part [in prime]



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 _ (6599 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 _ (86 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 _ (57 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 _ (3455 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 _ (290 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 _ (147 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 _ (148 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 _ (53 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 _ (1466 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 _ (28 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 _ (53 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 _ (788 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 _ (28 entries)