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

pairmap [definition, in seq]
pairmapK [lemma, in seq]
pairmap_tuple [definition, in tuple]
pairmap_tupleP [lemma, in tuple]
pair_big [lemma, in bigops]
pair_bigA [lemma, in bigops]
pair_big_dep [lemma, in bigops]
pair_eq [definition, in eqtype]
pair_eqE [lemma, in eqtype]
pair_eqP [lemma, in eqtype]
pair_eq1 [lemma, in eqtype]
pair_eq2 [lemma, in eqtype]
pair_of_tag [definition, in choice]
pair_of_tagK [lemma, in choice]
partition [definition, in finset]
Partitions [section, in finset]
Partitions.BigOps [section, in finset]
Partitions.BigOps.law [variable, in finset]
Partitions.BigOps.nil [variable, in finset]
Partitions.BigOps.R [variable, in finset]
Partitions.Preim [section, in finset]
Partitions.Preim.f [variable, in finset]
Partitions.Preim.rT [variable, in finset]
Partitions.T [variable, in finset]
partition_big [lemma, in bigops]
partition_big_imset [lemma, in finset]
partn [definition, in prime]
partnC [lemma, in prime]
partnI [lemma, in prime]
partnNK [lemma, in prime]
partnT [lemma, in prime]
partn0 [lemma, in prime]
partn1 [lemma, in prime]
partn_dvd [lemma, in prime]
partn_exp [lemma, in prime]
partn_mul [lemma, in prime]
partn_part [lemma, in prime]
partn_pi [lemma, in prime]
part_gt0 [lemma, in prime]
part_pnat [lemma, in prime]
part_p'nat [lemma, in prime]
pascal [lemma, in binomial]
pastemx [definition, in matrix]
pastemxEl [lemma, in matrix]
pastemxEr [lemma, in matrix]
pastemxKl [lemma, in matrix]
pastemxKr [lemma, in matrix]
pastemx0 [lemma, in matrix]
paste_mx_col' [lemma, in matrix]
path [definition, in paths]
pathP [lemma, in paths]
Paths [section, in paths]
paths [library]
Paths.n0 [variable, in paths]
Paths.Path [section, in paths]
Paths.Path.e [variable, in paths]
Paths.Path.x0_cycle [variable, in paths]
Paths.T [variable, in paths]
path_cat [lemma, in paths]
path_connect [lemma, in connect]
path_map [lemma, in paths]
path_merge [lemma, in paths]
path_sorted [lemma, in paths]
pcancel [definition, in ssrfun]
PcanChoiceMixin [definition, in choice]
PcanCountMixin [definition, in choice]
PcanEqMixin [definition, in eqtype]
PcanFinMixin [definition, in fintype]
pcan_enumP [lemma, in fintype]
pcan_inj [lemma, in ssrfun]
pcan_pcomp [lemma, in ssrfun]
pcan_pickleK [lemma, in choice]
pcomp [definition, in ssrfun]
pcycle [definition, in perm]
pcycles [definition, in perm]
pcycle_id [lemma, in perm]
pcycle_perm [lemma, in perm]
pcycle_sym [lemma, in perm]
pcycle_traject [lemma, in perm]
pdiv [definition, in prime]
pdivP [lemma, in prime]
pdiv_gt0 [lemma, in prime]
pdiv_min_dvd [lemma, in prime]
perm [abbreviation, in perm]
Perm [constructor, in perm]
perm [library]
PermDef [module, in perm]
PermDefSection [section, in perm]
PermDefSection.T [variable, in perm]
PermDefSig [module, in perm]
PermDefSig.fun_of_perm [axiom, in perm]
PermDefSig.fun_of_permE [axiom, in perm]
PermDefSig.perm [axiom, in perm]
PermDefSig.permE [axiom, in perm]
PermDef.fun_of_perm [definition, in perm]
PermDef.fun_of_permE [lemma, in perm]
PermDef.perm [definition, in perm]
PermDef.permE [lemma, in perm]
permE [lemma, in perm]
PermIn [section, in automorphism]
PermIn.B [variable, in automorphism]
PermIn.f [variable, in automorphism]
PermIn.injf [variable, in automorphism]
PermIn.sBf [variable, in automorphism]
PermIn.T [variable, in automorphism]
permJ [lemma, in perm]
permK [lemma, in perm]
permKV [lemma, in perm]
permM [lemma, in perm]
PermMatrix [section, in matrix]
PermMatrix.n [variable, in matrix]
PermMatrix.R [variable, in matrix]
permP [lemma, in perm]
PermSeq [section, in seq]
PermSeq.T [variable, in seq]
PermutationParity [section, in perm]
PermutationParity.T [variable, in perm]
permX [lemma, in perm]
perm1 [lemma, in perm]
perm_baseFinGroupType [definition, in perm]
perm_catAC [lemma, in seq]
perm_catC [lemma, in seq]
perm_catCA [lemma, in seq]
perm_cat2l [lemma, in seq]
perm_cat2r [lemma, in seq]
perm_choiceMixin [definition, in perm]
perm_choiceType [definition, in perm]
perm_closed [lemma, in perm]
perm_cons [lemma, in seq]
perm_countMixin [definition, in perm]
perm_countType [definition, in perm]
perm_def [abbreviation, in perm]
perm_eq [definition, in seq]
perm_eql [abbreviation, in seq]
perm_eql [abbreviation, in seq]
perm_eqlP [lemma, in seq]
perm_eqMixin [definition, in perm]
perm_eqP [lemma, in seq]
perm_eqr [abbreviation, in seq]
perm_eqr [abbreviation, in seq]
perm_eqrP [lemma, in seq]
perm_eqType [definition, in perm]
perm_eq_mem [lemma, in seq]
perm_eq_refl [lemma, in seq]
perm_eq_size [lemma, in seq]
perm_eq_sym [lemma, in seq]
perm_eq_trans [lemma, in seq]
perm_eq_uniq [lemma, in seq]
perm_finGroupType [definition, in perm]
perm_finMixin [definition, in perm]
perm_finType [definition, in perm]
perm_for_choiceType [definition, in perm]
perm_for_countType [definition, in perm]
perm_for_eqType [definition, in perm]
perm_for_finType [definition, in perm]
perm_for_subCountType [definition, in perm]
perm_for_subFinType [definition, in perm]
perm_for_subType [definition, in perm]
perm_in [definition, in automorphism]
perm_inE [lemma, in automorphism]
perm_inj [lemma, in perm]
perm_inv [definition, in perm]
perm_invK [lemma, in perm]
perm_invP [lemma, in perm]
perm_in_inj [lemma, in automorphism]
perm_in_on [lemma, in automorphism]
perm_merge [lemma, in paths]
perm_mul [definition, in perm]
perm_mulP [lemma, in perm]
perm_mx [definition, in matrix]
perm_mxV [lemma, in matrix]
perm_mx1 [lemma, in matrix]
perm_mx_is_perm [lemma, in matrix]
perm_of [definition, in perm]
perm_of_baseFinGroupMixin [definition, in perm]
perm_of_baseFinGroupType [definition, in perm]
perm_of_finGroupType [definition, in perm]
perm_on [definition, in perm]
perm_one [definition, in perm]
perm_oneP [lemma, in perm]
perm_onM [lemma, in perm]
perm_onto [lemma, in perm]
perm_on1 [lemma, in perm]
perm_proof [lemma, in perm]
perm_rcons [lemma, in seq]
perm_rot [lemma, in seq]
perm_rotr [lemma, in seq]
perm_sort [lemma, in paths]
perm_sortP [lemma, in paths]
perm_subCountType [definition, in perm]
perm_subFinType [definition, in perm]
perm_subType [definition, in perm]
perm_type [inductive, in perm]
perm_uniq [lemma, in seq]
perm_unlock [definition, in perm]
PervasiveMonoids [section, in bigops]
pfactor [definition, in prime]
pfactorK [lemma, in prime]
pfactor_coprime [lemma, in prime]
pfactor_dvdn [lemma, in prime]
pfactor_dvdnn [lemma, in prime]
pfactor_gt0 [lemma, in prime]
pfamily [definition, in finfun]
pfamilyP [lemma, in finfun]
pffun_on [definition, in finfun]
pffun_onP [lemma, in finfun]
ph [abbreviation, in ssrbool]
ph [abbreviation, in ssrbool]
Phant [constructor, in ssreflect]
phant [inductive, in ssreflect]
phantom [inductive, in ssreflect]
Phantom [constructor, in ssreflect]
phi [definition, in charpoly]
phi [definition, in prime]
phiE [lemma, in prime]
phi_add [lemma, in charpoly]
phi_coprime [lemma, in prime]
phi_count_coprime [lemma, in prime]
phi_gen [lemma, in cyclic]
phi_gt0 [lemma, in prime]
phi_mul [lemma, in charpoly]
phi_one [lemma, in charpoly]
phi_opp [lemma, in charpoly]
phi_pfactor [lemma, in prime]
phi_polyC [lemma, in charpoly]
phi_zero [lemma, in charpoly]
phi_Zpoly [lemma, in charpoly]
Pick [constructor, in fintype]
pick [definition, in fintype]
pickle [definition, in choice]
pickleK [lemma, in choice]
pickleK_inv [lemma, in choice]
pickle_inv [definition, in choice]
pickle_invK [lemma, in choice]
pickP [lemma, in fintype]
pick_spec [inductive, in fintype]
PiNat [section, in prime]
pi_of [definition, in prime]
pi_of_exp [lemma, in prime]
pi_of_prime [lemma, in prime]
PlainTheory [section, in finfun]
PlainTheory.aT [variable, in finfun]
PlainTheory.Family [section, in finfun]
PlainTheory.Family.F [variable, in finfun]
PlainTheory.rT [variable, in finfun]
plusE [lemma, in ssrnat]
pmap [definition, in seq]
Pmap [section, in seq]
pmapS_filter [lemma, in seq]
Pmapub [section, in seq]
Pmapub.p [variable, in seq]
Pmapub.sT [variable, in seq]
Pmapub.T [variable, in seq]
Pmap.aT [variable, in seq]
Pmap.f [variable, in seq]
Pmap.fK [variable, in seq]
Pmap.g [variable, in seq]
Pmap.rT [variable, in seq]
pmap_filter [lemma, in seq]
pmap_sub_uniq [lemma, in seq]
pmap_uniq [lemma, in seq]
pnat [definition, in prime]
pnatE [lemma, in prime]
pnatI [lemma, in prime]
pnatNK [lemma, in prime]
pnatP [lemma, in prime]
pnat_coprime [lemma, in prime]
pnat_div [lemma, in prime]
pnat_dvd [lemma, in prime]
pnat_exp [lemma, in prime]
pnat_id [lemma, in prime]
pnat_mul [lemma, in prime]
pnat_part [lemma, in prime]
pnat_pi [lemma, in prime]
pnat_1 [lemma, in prime]
Poly [definition, in poly]
poly [library]
polyC [definition, in poly]
polyC0 [lemma, in poly]
polyC1 [lemma, in poly]
polyC_add [lemma, in poly]
polyC_eq0 [lemma, in poly]
polyC_exp [lemma, in poly]
polyC_inj [lemma, in poly]
polyC_mul [lemma, in poly]
polyC_natmul [lemma, in poly]
polyC_opp [lemma, in poly]
polyC_sub [lemma, in poly]
PolyK [lemma, in poly]
Polynomial [constructor, in poly]
Polynomial [section, in poly]
polynomial [record, in poly]
PolynomialComRing [section, in poly]
PolynomialComRing.R [variable, in poly]
PolynomialIdomain [section, in poly]
PolynomialIdomain.R [variable, in poly]
Polynomial.R [variable, in poly]
polynomial_choiceMixin [definition, in poly]
polynomial_choiceType [definition, in poly]
polynomial_comRingType [definition, in poly]
polynomial_comUnitRingType [definition, in poly]
polynomial_eqMixin [definition, in poly]
polynomial_eqType [definition, in poly]
polynomial_idomainType [definition, in poly]
polynomial_ringType [definition, in poly]
polynomial_subType [definition, in poly]
polynomial_unitRingType [definition, in poly]
polynomial_zmodType [definition, in poly]
polyP [lemma, in poly]
polyseq [projection, in poly]
polyseqC [lemma, in poly]
polyseqK [lemma, in poly]
polyseqX [lemma, in poly]
polyseq1 [lemma, in poly]
polyseq_cons [lemma, in poly]
polyseq_poly [lemma, in poly]
polySpred [lemma, in poly]
polyX [definition, in poly]
poly0Vpos [lemma, in poly]
poly_choiceType [definition, in poly]
poly_comRingType [definition, in poly]
poly_comUnitRingType [definition, in poly]
poly_cons [definition, in poly]
poly_cons_def [lemma, in poly]
poly_def [lemma, in poly]
poly_eqType [definition, in poly]
poly_idomainMixin [lemma, in poly]
poly_idomainType [definition, in poly]
poly_ind [lemma, in poly]
poly_inj [lemma, in poly]
poly_intro_unit [lemma, in poly]
poly_inv [definition, in poly]
poly_inv_out [lemma, in poly]
poly_mulC [lemma, in poly]
poly_mulVp [lemma, in poly]
poly_of [definition, in poly]
poly_ringMixin [definition, in poly]
poly_ringType [definition, in poly]
poly_subType [definition, in poly]
poly_unit [definition, in poly]
poly_unitRingMixin [definition, in poly]
poly_unitRingType [definition, in poly]
poly_zmodMixin [definition, in poly]
poly_zmodType [definition, in poly]
pop_succn [definition, in ssrnat]
PosNat [constructor, in ssrnat]
PosNotEq0 [constructor, in ssrnat]
posnP [lemma, in ssrnat]
pos_nat [record, in ssrnat]
pos_natP [lemma, in ssrnat]
pos_nat_choiceMixin [definition, in choice]
pos_nat_choiceType [definition, in choice]
pos_nat_countMixin [definition, in choice]
pos_nat_countType [definition, in choice]
pos_nat_eqMixin [definition, in ssrnat]
pos_nat_eqType [definition, in ssrnat]
pos_nat_subCountType [definition, in choice]
pos_nat_subType [definition, in ssrnat]
pos_nat_val [projection, in ssrnat]
pos_of_nat [definition, in ssrnat]
powerset [definition, in finfun]
pred [definition, in ssrbool]
predArgType [definition, in ssrbool]
predC [definition, in ssrbool]
predC1 [definition, in eqtype]
predC_closed [lemma, in connect]
predD [definition, in ssrbool]
predD1 [definition, in eqtype]
predD1P [lemma, in eqtype]
predE [lemma, in ssrnat]
predI [definition, in ssrbool]
Predicates [section, in ssrbool]
Predicates.T [variable, in ssrbool]
predn [definition, in ssrnat]
prednK [lemma, in ssrnat]
predPredType [definition, in ssrbool]
predT [definition, in ssrbool]
PredType [constructor, in ssrbool]
predType [record, in ssrbool]
predT_subset [lemma, in fintype]
predU [definition, in ssrbool]
predU1 [definition, in eqtype]
predU1l [lemma, in eqtype]
predU1P [lemma, in eqtype]
predU1r [lemma, in eqtype]
predX [definition, in eqtype]
predX_prod_enum [lemma, in fintype]
pred0 [definition, in ssrbool]
pred0b [definition, in fintype]
pred0P [lemma, in fintype]
pred0Pn [lemma, in fintype]
pred1 [definition, in eqtype]
pred1E [lemma, in eqtype]
pred2 [definition, in eqtype]
pred2P [lemma, in eqtype]
pred3 [definition, in eqtype]
pred4 [definition, in eqtype]
pred_class [abbreviation, in ssrbool]
pred_of_argType [definition, in ssrbool]
pred_of_eq_seq [definition, in seq]
pred_of_mem [definition, in ssrbool]
pred_of_mem_pred [definition, in ssrbool]
pred_of_set [abbreviation, in finset]
pred_of_set_def [abbreviation, in finset]
pred_of_set_unlock [definition, in finset]
pred_of_simpl [definition, in ssrbool]
pred_sort [projection, in ssrbool]
PreGroupIdentities [section, in groups]
PreGroupIdentities.T [variable, in groups]
preim [definition, in ssrbool]
preimset [definition, in finset]
preimsetC [lemma, in finset]
preimsetD [lemma, in finset]
preimsetI [lemma, in finset]
preimsetS [lemma, in finset]
preimsetT [lemma, in finset]
preimsetU [lemma, in finset]
preimset0 [lemma, in finset]
preimset_proper [lemma, in finset]
preim_at [definition, in finset]
preim_autE [lemma, in automorphism]
preim_iinv [lemma, in fintype]
preim_partition [definition, in finset]
preim_partitionP [lemma, in finset]
preim_seq [definition, in fintype]
prev [definition, in paths]
prev_at [definition, in paths]
prev_cycle [lemma, in paths]
prev_map [lemma, in paths]
prev_next [lemma, in paths]
prev_nth [lemma, in paths]
prev_rev [lemma, in paths]
prev_rot [lemma, in paths]
prev_rotr [lemma, in paths]
pre_image [lemma, in fintype]
pre_symmetric [definition, in ssrbool]
prime [definition, in prime]
prime [library]
PrimeField [section, in zmodp]
PrimeField.p [variable, in zmodp]
PrimeField.pr_p [variable, in zmodp]
primeP [lemma, in prime]
primePn [lemma, in prime]
primePns [lemma, in prime]
primes [definition, in prime]
primes_exp [lemma, in prime]
primes_mul [lemma, in prime]
primes_part [lemma, in prime]
primes_pdiv [lemma, in prime]
primes_prime [lemma, in prime]
primes_uniq [lemma, in prime]
prime_coprime [lemma, in prime]
prime_cyclic [lemma, in cyclic]
prime_decomp [definition, in prime]
prime_decomp [section, in prime]
prime_decompE [lemma, in prime]
prime_decomp_correct [lemma, in prime]
prime_decomp_rec [definition, in prime]
prime_gt0 [lemma, in prime]
prime_gt1 [lemma, in prime]
prime_pdiv [lemma, in prime]
prime_pos_nat [definition, in prime]
ProdEqType [section, in eqtype]
ProdEqType.T1 [variable, in eqtype]
ProdEqType.T2 [variable, in eqtype]
ProdFinType [section, in fintype]
ProdFinType.T1 [variable, in fintype]
ProdFinType.T2 [variable, in fintype]
prodn_cond_gt0 [lemma, in bigops]
prodn_gt0 [lemma, in bigops]
ProdTag [section, in choice]
ProdTag.T1 [variable, in choice]
ProdTag.T2 [variable, in choice]
prod_choiceMixin [definition, in choice]
prod_choiceType [definition, in choice]
prod_countMixin [definition, in choice]
prod_countType [definition, in choice]
prod_enum [definition, in fintype]
prod_enumP [lemma, in fintype]
prod_eqMixin [definition, in eqtype]
prod_eqType [definition, in eqtype]
prod_finMixin [definition, in fintype]
prod_finType [definition, in fintype]
prod_nat_const [lemma, in bigops]
prod_nat_const_nat [lemma, in bigops]
prod_prime_decomp [lemma, in prime]
prod_tpermP [lemma, in perm]
proper [definition, in fintype]
properD [lemma, in finset]
properD1 [lemma, in finset]
properE [lemma, in fintype]
properEcard [lemma, in finset]
properEneq [lemma, in finset]
properI [lemma, in finset]
properIl [lemma, in finset]
properIr [lemma, in finset]
properIset [lemma, in finset]
properP [lemma, in fintype]
properU [lemma, in finset]
properUl [lemma, in finset]
properUr [lemma, in finset]
proper0 [lemma, in finset]
proper1G [lemma, in groups]
proper1set [lemma, in finset]
proper_card [lemma, in fintype]
proper_irrefl [lemma, in fintype]
proper_neq [lemma, in finset]
proper_sub [lemma, in fintype]
proper_subn [lemma, in fintype]
proper_sub_trans [lemma, in fintype]
proper_trans [lemma, in fintype]
prop_congr [lemma, in ssrbool]
prop_in1 [definition, in ssrbool]
prop_in11 [definition, in ssrbool]
prop_in111 [definition, in ssrbool]
prop_in12 [definition, in ssrbool]
prop_in2 [definition, in ssrbool]
prop_in21 [definition, in ssrbool]
prop_in3 [definition, in ssrbool]
prop_on1 [definition, in ssrbool]
prop_on2 [definition, in ssrbool]
protect_term [definition, in ssreflect]
pT [abbreviation, in perm]
pT [abbreviation, in perm]
pval [definition, in perm]
pvalE [lemma, in perm]
p'natE [lemma, in prime]
p_natP [lemma, in prime]
p_part [lemma, 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)