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

p [abbreviation, in zmodp]
p [definition, in extremal]
p [abbreviation, in zmodp]
PackSocle [constructor, in mxrepresentation]
PackSocleK [lemma, in mxrepresentation]
pack_subFinType [definition, in fintype]
pack_subCountType [definition, in choice]
pairg1 [definition, in gproduct]
pairg1_morphism [definition, in gproduct]
pairg1_morphM [lemma, in gproduct]
pairmap [definition, in seq]
pairmapK [lemma, in seq]
pairmap_tuple [definition, in tuple]
pairmap_cat [lemma, in seq]
pairmap_tupleP [lemma, in tuple]
pair_of_sd [definition, in gproduct]
pair_of_section [definition, in jordanholder]
pair_big_dep [lemma, in bigop]
pair_eqP [lemma, in eqtype]
pair_of_tagK [lemma, in choice]
pair_big [lemma, in bigop]
pair_bigA [lemma, in bigop]
pair_eq1 [lemma, in eqtype]
pair_eqE [lemma, in eqtype]
pair_eq [definition, in eqtype]
pair_of_mxvec_index [definition, in matrix]
pair_eq2 [lemma, in eqtype]
pair_of_tag [definition, in choice]
pair1g [definition, in gproduct]
pair1g_morphism [definition, in gproduct]
pair1g_morphM [lemma, in gproduct]
partG_eq1 [lemma, in pgroup]
PartialAction [section, in action]
PartialAction.aT [variable, in action]
PartialAction.D [variable, in action]
PartialAction.OrbitStabilizer [section, in action]
PartialAction.OrbitStabilizer.G [variable, in action]
PartialAction.OrbitStabilizer.sGD [variable, in action]
PartialAction.OrbitStabilizer.x [variable, in action]
PartialAction.rT [variable, in action]
PartialAction.to [variable, in action]
PartialFunctorTheory [section, in gfunctor]
PartialFunctorTheory.BasicTheory [section, in gfunctor]
PartialFunctorTheory.BasicTheory.F [variable, in gfunctor]
PartialFunctorTheory.F1 [variable, in gfunctor]
PartialFunctorTheory.F2 [variable, in gfunctor]
PartialFunctorTheory.Modulo [section, in gfunctor]
PartialFunctorTheory.Modulo.F1 [variable, in gfunctor]
PartialFunctorTheory.Modulo.F2 [variable, in gfunctor]
partial_product [definition, in gproduct]
partition [definition, in finset]
Partitions [section, in finset]
Partitions.BigOps [section, in finset]
Partitions.BigOps.idx [variable, in finset]
Partitions.BigOps.op [variable, in finset]
Partitions.BigOps.R [variable, in finset]
Partitions.I [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_imset [lemma, in finset]
partition_big [lemma, in bigop]
partn [definition, in prime]
partnC [lemma, in prime]
partnI [lemma, in prime]
partnNK [lemma, in prime]
partnT [lemma, in prime]
partn_gcd [lemma, in prime]
partn_exp [lemma, in prime]
partn_part [lemma, in prime]
partn_biglcm [lemma, in prime]
partn_exponentS [lemma, in abelian]
partn_lcm [lemma, in prime]
partn_dvd [lemma, in prime]
partn_eq1 [lemma, in prime]
partn_mul [lemma, in prime]
partn_biggcd [lemma, in prime]
partn_pi [lemma, in prime]
partn0 [lemma, in prime]
partn1 [lemma, in prime]
part_pnat_id [lemma, in prime]
part_pnat [lemma, in prime]
part_p'nat [lemma, in prime]
part_gt0 [lemma, in prime]
Pascal [lemma, in binomial]
path [definition, in path]
path [library]
pathP [lemma, in path]
Paths [section, in path]
Paths.n0 [variable, in path]
Paths.Path [section, in path]
Paths.Path.e [variable, in path]
Paths.Path.x0_cycle [variable, in path]
Paths.T [variable, in path]
path_cat [lemma, in path]
path_rev [lemma, in path]
path_connect [lemma, in fingraph]
path_setIgr [definition, in gseries]
path_sorted [lemma, in path]
path_merge [lemma, in path]
path_rcons [lemma, in path]
path_map [lemma, in path]
path_min_sorted [lemma, in path]
pcancel [definition, in ssrfun]
PcanChoiceMixin [definition, in choice]
PcanCountMixin [definition, in choice]
PcanEqMixin [definition, in eqtype]
PcanFinMixin [definition, in fintype]
pcan_inj [lemma, in ssrfun]
pcan_pcomp [lemma, in ssrfun]
pcan_enumP [lemma, in fintype]
pcan_pickleK [lemma, in choice]
pcomp [definition, in ssrfun]
pcore [definition, in pgroup]
PcoreDef [section, in pgroup]
PcoreDef.A [variable, in pgroup]
PcoreDef.gT [variable, in pgroup]
PcoreDef.pi [variable, in pgroup]
pcoreI [lemma, in pgroup]
pcoreJ [lemma, in pgroup]
pcoreNK [lemma, in pgroup]
PCoreProps [section, in pgroup]
PCoreProps.gT [variable, in pgroup]
PCoreProps.pi [variable, in pgroup]
pcoreS [lemma, in pgroup]
pcore_modp [lemma, in pgroup]
pcore_pgFun [definition, in pgroup]
pcore_gFun [definition, in pgroup]
pcore_igFun [definition, in pgroup]
pcore_mod_group [definition, in pgroup]
pcore_group [definition, in pgroup]
pcore_mod_res [lemma, in pgroup]
pcore_sub_Hall [lemma, in pgroup]
pcore_mod1 [lemma, in pgroup]
pcore_Fitting [lemma, in maximal]
pcore_mod [definition, in pgroup]
pcore_max [lemma, in pgroup]
pcore_psubgroup [lemma, in pgroup]
pcore_faithful_mx_irr [lemma, in mxabelem]
pcore_sub [lemma, in pgroup]
pcore_pgroup_id [lemma, in pgroup]
pcore_char [lemma, in pgroup]
pcore_mod_sub [lemma, in pgroup]
pcore_sub_rstab_mxsimple [lemma, in mxabelem]
pcore_sub_rker_mx_irr [lemma, in mxabelem]
pcore_normal [lemma, in pgroup]
pcore_pgroup [lemma, in pgroup]
pcore_faithful_irr_act [lemma, in sylow]
pcore_sub_astab_irr [lemma, in sylow]
pcore_setI_normal [lemma, in pgroup]
pcycle [definition, in perm]
pcycleE [lemma, in action]
pcycles [definition, in perm]
pcycle_id [lemma, in perm]
pcycle_traject [lemma, in perm]
pcycle_actperm [lemma, in action]
pcycle_sym [lemma, in perm]
pcycle_perm [lemma, in perm]
pdiv [definition, in prime]
pdivP [lemma, in prime]
pdiv_gt0 [lemma, in prime]
pdiv_min_dvd [lemma, in prime]
pdiv_leq [lemma, in prime]
pdiv_prime [lemma, in prime]
pdiv_pfactor [lemma, in prime]
pdiv_p_elt [lemma, in abelian]
pdiv_dvd [lemma, in prime]
pdiv_id [lemma, in prime]
pE [definition, in mxabelem]
pElem [definition, in abelian]
pElemI [lemma, in abelian]
pElemJ [lemma, in abelian]
pElemP [lemma, in abelian]
pElemS [lemma, in abelian]
Perm [constructor, in perm]
perm [abbreviation, in perm]
perm [library]
PermAction [section, in action]
PermAction.rT [variable, in action]
PermDef [module, in perm]
PermDefSection [section, in perm]
PermDefSection.T [variable, in perm]
PermDefSig [module, in perm]
PermDefSig.fun_of_permE [axiom, in perm]
PermDefSig.fun_of_perm [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.A [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]
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]
perm_mx [definition, in matrix]
perm_eqP [lemma, in seq]
perm_inj [lemma, in perm]
perm_cat2r [lemma, in seq]
perm_cat2l [lemma, in seq]
perm_oneP [lemma, in perm]
perm_eqrP [lemma, in seq]
perm_on [definition, in perm]
perm_of_finGroupType [definition, in perm]
perm_of_baseFinGroupType [definition, in perm]
perm_finGroupType [definition, in perm]
perm_baseFinGroupType [definition, in perm]
perm_unlock [definition, in perm]
perm_for_subFinType [definition, in perm]
perm_for_finType [definition, in perm]
perm_for_subCountType [definition, in perm]
perm_for_countType [definition, in perm]
perm_for_choiceType [definition, in perm]
perm_for_eqType [definition, in perm]
perm_for_subType [definition, in perm]
perm_subFinType [definition, in perm]
perm_finType [definition, in perm]
perm_subCountType [definition, in perm]
perm_countType [definition, in perm]
perm_choiceType [definition, in perm]
perm_eqType [definition, in perm]
perm_subType [definition, in perm]
perm_faithful [lemma, in action]
perm_eqlP [lemma, in seq]
perm_finMixin [definition, in perm]
perm_type [inductive, in perm]
perm_mx_is_perm [lemma, in matrix]
perm_countMixin [definition, in perm]
perm_inv [definition, in perm]
perm_mulP [lemma, in perm]
perm_one [definition, in perm]
perm_onM [lemma, in perm]
perm_mx1 [lemma, in matrix]
perm_mxM [lemma, in matrix]
perm_catAC [lemma, in seq]
perm_sort [lemma, in path]
perm_invK [lemma, in perm]
perm_mact [lemma, in action]
perm_uniq [lemma, in seq]
perm_filterC [lemma, in seq]
perm_onto [lemma, in perm]
perm_eqr [abbreviation, in seq]
perm_in [definition, in automorphism]
perm_choiceMixin [definition, in perm]
perm_cons [lemma, in seq]
perm_eq_uniq [lemma, in seq]
perm_proof [lemma, in perm]
perm_eq [definition, in seq]
perm_eql [abbreviation, in seq]
perm_eq_size [lemma, in seq]
perm_sortP [lemma, in path]
perm_eq_refl [lemma, in seq]
perm_closed [lemma, in perm]
perm_inE [lemma, in automorphism]
perm_act1P [lemma, in action]
perm_invP [lemma, in perm]
perm_eq_trans [lemma, in seq]
perm_eqMixin [definition, in perm]
perm_of [definition, in perm]
perm_catC [lemma, in seq]
perm_mul [definition, in perm]
perm_on1 [lemma, in perm]
perm_action [definition, in action]
perm_def [abbreviation, in perm]
perm_merge [lemma, in path]
perm_eq_mem [lemma, in seq]
perm_mxV [lemma, in matrix]
perm_rot [lemma, in seq]
perm_eq_abelian_type [lemma, in abelian]
perm_in_on [lemma, in automorphism]
perm_in_inj [lemma, in automorphism]
perm_rcons [lemma, in seq]
perm_of_baseFinGroupMixin [definition, in perm]
perm_eql [abbreviation, in seq]
perm_eq_sym [lemma, in seq]
perm_eqr [abbreviation, in seq]
perm_catCA [lemma, in seq]
perm_rotr [lemma, in seq]
perm1 [lemma, in perm]
PervasiveMonoids [section, in bigop]
Pextraspecial [module, in extraspecial]
Pextraspecial.act [definition, in extraspecial]
Pextraspecial.action [definition, in extraspecial]
Pextraspecial.actP [lemma, in extraspecial]
Pextraspecial.Construction [section, in extraspecial]
Pextraspecial.Construction.p [variable, in extraspecial]
Pextraspecial.gactP [lemma, in extraspecial]
Pextraspecial.groupAction [definition, in extraspecial]
Pextraspecial.gtype [definition, in extraspecial]
Pextraspecial.ngtype [definition, in extraspecial]
Pextraspecial.ngtypeQ [definition, in extraspecial]
pfactor [definition, in prime]
pfactorK [lemma, in prime]
pfactorKpdiv [lemma, in prime]
pfactor_dvdn [lemma, in prime]
pfactor_coprime [lemma, in prime]
pfactor_gt0 [lemma, in prime]
pfactor_dvdnn [lemma, in prime]
pfamily [definition, in finfun]
pfamilyP [lemma, in finfun]
pffun_on [definition, in finfun]
pffun_onP [lemma, in finfun]
pgroup [definition, in pgroup]
pgroup [library]
PgroupDefs [section, in pgroup]
PgroupDefs.gT [variable, in pgroup]
pgroupE [lemma, in pgroup]
pgroupJ [lemma, in pgroup]
pgroupM [lemma, in pgroup]
pgroupNK [lemma, in pgroup]
pgroupP [lemma, in pgroup]
PgroupProps [section, in pgroup]
PgroupProps.gT [variable, in pgroup]
pgroupS [lemma, in pgroup]
pgroup_pi [lemma, in pgroup]
pgroup_nil [lemma, in sylow]
pgroup_p [lemma, in pgroup]
pgroup_sol [lemma, in sylow]
pgroup_fix_mod [lemma, in sylow]
pgroup_pdiv [lemma, in pgroup]
pgroup1 [lemma, in pgroup]
ph [abbreviation, in ssrbool]
ph [abbreviation, in ssrbool]
pHall [definition, in pgroup]
pHallE [lemma, in pgroup]
pHallJ [lemma, in pgroup]
pHallJnorm [lemma, in pgroup]
pHallJ2 [lemma, in pgroup]
pHallNK [lemma, in pgroup]
pHallP [lemma, in pgroup]
pHall_id [lemma, in pgroup]
pHall_subl [lemma, in pgroup]
pHall_Hall [lemma, in pgroup]
pHall_sub [lemma, in pgroup]
pHall_pgroup [lemma, in pgroup]
Phant [constructor, in ssreflect]
phant [inductive, in ssreflect]
phantom [inductive, in ssreflect]
Phantom [constructor, in ssreflect]
phant_id [definition, in ssrfun]
phi [definition, in prime]
phiE [lemma, in prime]
PhiJ [lemma, in maximal]
PhiS [lemma, in maximal]
Phi_quotient_id [lemma, in maximal]
Phi_proper [lemma, in maximal]
phi_gen [lemma, in cyclic]
Phi_normal [lemma, in maximal]
Phi_quotient_cyclic [lemma, in maximal]
phi_coprime [lemma, in prime]
Phi_min [lemma, in maximal]
phi_pfactor [lemma, in prime]
Phi_mulg [lemma, in maximal]
Phi_char [lemma, in maximal]
Phi_nongen [lemma, in maximal]
Phi_cprod [lemma, in maximal]
phi_gt0 [lemma, in prime]
Phi_joing [lemma, in maximal]
Phi_quotient_abelem [lemma, in maximal]
Phi_sub_max [lemma, in maximal]
Phi_sub [lemma, in maximal]
phi_count_coprime [lemma, in prime]
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]
pid_mx_block [lemma, in matrix]
pid_mx [definition, in matrix]
pid_mx_id [lemma, in matrix]
pid_mx_minv [lemma, in matrix]
pid_mx_1 [lemma, in matrix]
pid_mx_col [lemma, in matrix]
pid_mx_minh [lemma, in matrix]
pid_mx_row [lemma, in matrix]
pid_mx_0 [lemma, in matrix]
PiNat [section, in prime]
pinvmx [definition, in mxalgebra]
piOhm1 [lemma, in abelian]
piSg [lemma, in fingroup]
pi_of_prime [lemma, in prime]
pi_max_pdiv [lemma, in prime]
pi_of_partn [lemma, in prime]
pi_arg_of_fin_pred [definition, in prime]
pi_arg_of_nat [definition, in prime]
pi_of [definition, in prime]
pi_pnat [lemma, in prime]
pi_pdiv [lemma, in prime]
pi_wrapped_arg [definition, in prime]
pi_of_muln [lemma, in prime]
pi_of_exponent [lemma, in abelian]
pi_center_nilpotent [lemma, in sylow]
pi_p'nat [lemma, in prime]
pi_of_exp [lemma, in prime]
pi_unwrapped_arg [definition, in prime]
pi_p'group [lemma, in pgroup]
pi_pgroup [lemma, in pgroup]
pi_of_dvd [lemma, in prime]
pi'_p'group [lemma, in pgroup]
pi'_p'nat [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_uniq [lemma, in seq]
pmap_filter [lemma, in seq]
pmap_sub_uniq [lemma, 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]
PMax [section, in maximal]
pmaxElem [definition, in abelian]
pmaxElemJ [lemma, in abelian]
pmaxElemP [lemma, in abelian]
pmaxElemS [lemma, in abelian]
pmaxElem_LdivP [lemma, in abelian]
pmaxElem_exists [lemma, in abelian]
pmaxElem_extraspecial [lemma, in maximal]
PMax.gT [variable, in maximal]
PMax.M [variable, in maximal]
PMax.p [variable, in maximal]
PMax.P [variable, in maximal]
PMax.pP [variable, in maximal]
pmorphimF [lemma, in gfunctor]
pmorphim_pgroup [lemma, in pgroup]
pmorphim_pHall [lemma, in pgroup]
pnat [definition, in prime]
pnatE [lemma, in prime]
pnatI [lemma, in prime]
pnatNK [lemma, in prime]
pnatP [lemma, in prime]
pnatPpi [lemma, in prime]
pnat_div [lemma, in prime]
pnat_coprime [lemma, in prime]
pnat_1 [lemma, in prime]
pnat_mul [lemma, in prime]
pnat_dvd [lemma, in prime]
pnat_exponent [lemma, in abelian]
pnat_exp [lemma, in prime]
pnat_id [lemma, in prime]
pnat_pi [lemma, in prime]
pnElem [definition, in abelian]
pnElemE [lemma, in abelian]
pnElemI [lemma, in abelian]
pnElemJ [lemma, in abelian]
pnElemP [lemma, in abelian]
pnElemPcard [lemma, in abelian]
pnElemS [lemma, in abelian]
pnElem_prime [lemma, in abelian]
pnElem0 [lemma, in abelian]
Poly [definition, in poly]
poly [library]
polyC [definition, in poly]
PolyCompose [section, in poly]
PolyCompose.R [variable, in poly]
polyC_rmorphism [definition, in poly]
polyC_additive [definition, in poly]
polyC_opp [lemma, in poly]
polyC_exp [lemma, in poly]
polyC_eq0 [lemma, in poly]
polyC_natmul [lemma, in poly]
polyC_inj [lemma, in poly]
polyC_add [lemma, in poly]
polyC_is_rmorphism [lemma, in poly]
polyC_mul [lemma, in poly]
polyC_sub [lemma, in poly]
polyC0 [lemma, in poly]
polyC1 [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]
PolynomialTheory [section, in poly]
PolynomialTheory.R [variable, in poly]
polynomial_idomainType [definition, in poly]
polynomial_comUnitRingType [definition, in poly]
polynomial_unitAlgType [definition, in poly]
polynomial_unitRingType [definition, in poly]
polynomial_algType [definition, in poly]
polynomial_comRingType [definition, in poly]
polynomial_lalgType [definition, in poly]
polynomial_lmodType [definition, in poly]
polynomial_ringType [definition, in poly]
polynomial_zmodType [definition, in poly]
polynomial_choiceType [definition, in poly]
polynomial_eqType [definition, in poly]
polynomial_subType [definition, in poly]
polynomial_choiceMixin [definition, in poly]
polynomial_eqMixin [definition, in poly]
Polynomial.R [variable, in poly]
polyP [lemma, in poly]
polyseq [projection, in poly]
polyseqC [lemma, in poly]
polyseqK [lemma, in poly]
polyseqX [lemma, in poly]
polyseq_cons [lemma, in poly]
polyseq_poly [lemma, in poly]
polyseq1 [lemma, in poly]
polySpred [lemma, in poly]
polyX [definition, in poly]
poly_unit [definition, in poly]
poly_rV_is_linear [lemma, in mxpoly]
poly_mulC [lemma, in poly]
poly_idomainMixin [lemma, in poly]
poly_comp_scall [lemma, in poly]
poly_unitRingMixin [definition, in poly]
poly_ind [lemma, in poly]
poly_cons_def [lemma, in poly]
poly_comp_addl [lemma, in poly]
poly_of [definition, in poly]
poly_comp_rmorphism [definition, in poly]
poly_comp_linear [definition, in poly]
poly_comp_additive [definition, in poly]
poly_idomainType [definition, in poly]
poly_comUnitRingType [definition, in poly]
poly_unitAlgType [definition, in poly]
poly_unitRingType [definition, in poly]
poly_algType [definition, in poly]
poly_comRingType [definition, in poly]
poly_lalgType [definition, in poly]
poly_lmodType [definition, in poly]
poly_lmodMixin [definition, in poly]
poly_ringType [definition, in poly]
poly_zmodType [definition, in poly]
poly_choiceType [definition, in poly]
poly_eqType [definition, in poly]
poly_subType [definition, in poly]
poly_compA [lemma, in poly]
poly_comp_is_additive [lemma, in poly]
poly_comp_subl [lemma, in poly]
poly_cons [definition, in poly]
poly_compE [lemma, in poly]
poly_initial [lemma, in poly]
poly_com0p [lemma, in poly]
poly_rV [definition, in mxpoly]
poly_comp_amulX [lemma, in poly]
poly_comp_rmorphr [lemma, in poly]
poly_comXp [lemma, in poly]
poly_compC [lemma, in poly]
poly_comp_mull [lemma, in poly]
poly_comp0 [lemma, in poly]
poly_inv [definition, in poly]
poly_mulVp [lemma, in poly]
poly_comp_translateK [lemma, in poly]
poly_comp [definition, in poly]
poly_zmodMixin [definition, in poly]
poly_inj [lemma, in poly]
poly_compX [lemma, in poly]
poly_intro_unit [lemma, in poly]
poly_inv_out [lemma, in poly]
poly_def [lemma, in poly]
poly_rV_linear [definition, in mxpoly]
poly_rV_additive [definition, in mxpoly]
poly_morphX_comm [lemma, in poly]
poly_rV_K [lemma, in mxpoly]
poly_ringMixin [definition, in poly]
poly_comp_is_linear [lemma, in poly]
poly0Vpos [lemma, in poly]
pop_succn [definition, in ssrnat]
PosNotEq0 [constructor, in ssrnat]
posnP [lemma, in ssrnat]
pos_of_nat [definition, in ssrnat]
powerset [definition, in finfun]
powers_mx [definition, in mxpoly]
pprod [abbreviation, in gproduct]
pprod [abbreviation, in gproduct]
pprodE [lemma, in gproduct]
pprodEY [lemma, in gproduct]
pprodg1 [lemma, in gproduct]
pprodm [definition, in gproduct]
pprodmE [lemma, in gproduct]
pprodmEl [lemma, in gproduct]
pprodmEr [lemma, in gproduct]
pprodmM [lemma, in gproduct]
pprodm_morphism [definition, in gproduct]
pprodP [lemma, in gproduct]
pprod1g [lemma, in gproduct]
Pquotient [section, in pgroup]
pquotient_pHall [lemma, in pgroup]
pquotient_pcore [lemma, in pgroup]
pquotient_pgroup [lemma, in pgroup]
Pquotient.G [variable, in pgroup]
Pquotient.gT [variable, in pgroup]
Pquotient.H [variable, in pgroup]
Pquotient.K [variable, in pgroup]
Pquotient.p [variable, in pgroup]
Pquotient.pi [variable, in pgroup]
Pquotient.piK [variable, in pgroup]
pred [definition, in ssrbool]
predArgType [definition, in ssrbool]
predC [definition, in ssrbool]
predC_closed [lemma, in fingraph]
predC1 [definition, in eqtype]
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]
predn_subS [lemma, in ssrnat]
predn_exp [lemma, in binomial]
predn_sub [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]
pred_class [abbreviation, in ssrbool]
pred_of_set_unlock [definition, in finset]
pred_sort [projection, in ssrbool]
pred_of_set_def [abbreviation, in finset]
pred_of_set [abbreviation, in finset]
pred_of_eq_seq [definition, in seq]
pred_of_mem_pred [definition, in ssrbool]
pred_of_argType [definition, in ssrbool]
pred_of_mem [definition, in ssrbool]
pred_of_simpl [definition, in ssrbool]
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]
PreGroupIdentities [section, in fingroup]
PreGroupIdentities.T [variable, in fingroup]
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]
preimset_proper [lemma, in finset]
preimset0 [lemma, in finset]
preim_at [definition, in finset]
preim_permV [lemma, in perm]
preim_partitionP [lemma, in finset]
preim_partition [definition, in finset]
preim_iinv [lemma, in fintype]
preim_seq [definition, in fintype]
preim_autE [lemma, in automorphism]
Presentation [module, in presentation]
presentation [library]
PresentationTheory [section, in presentation]
Presentation.And [constructor, in presentation]
Presentation.and_rel [definition, in presentation]
Presentation.bool_of_rel [definition, in presentation]
Presentation.Cast [definition, in presentation]
Presentation.Comm [constructor, in presentation]
Presentation.Conj [constructor, in presentation]
Presentation.Cst [constructor, in presentation]
Presentation.Env [constructor, in presentation]
Presentation.env [inductive, in presentation]
Presentation.env1 [definition, in presentation]
Presentation.Eq1 [definition, in presentation]
Presentation.Eq2 [constructor, in presentation]
Presentation.Eq3 [definition, in presentation]
Presentation.eval [definition, in presentation]
Presentation.Exp [constructor, in presentation]
Presentation.Formula [constructor, in presentation]
Presentation.formula [inductive, in presentation]
Presentation.Generator [constructor, in presentation]
Presentation.hom [definition, in presentation]
Presentation.Idx [constructor, in presentation]
Presentation.Inv [constructor, in presentation]
Presentation.iso [definition, in presentation]
Presentation.Mul [constructor, in presentation]
Presentation.NoRel [constructor, in presentation]
Presentation.Presentation [section, in presentation]
Presentation.rel [definition, in presentation]
Presentation.Rel [constructor, in presentation]
Presentation.rel_type [inductive, in presentation]
Presentation.sat [definition, in presentation]
Presentation.term [inductive, in presentation]
Presentation.type [inductive, in presentation]
prev [definition, in path]
prev_at [definition, in path]
prev_cycle [lemma, in path]
prev_rev [lemma, in path]
prev_rotr [lemma, in path]
prev_nth [lemma, in path]
prev_rot [lemma, in path]
prev_map [lemma, in path]
prev_next [lemma, in path]
pre_symmetric [definition, in ssrbool]
pre_image [lemma, in fintype]
prime [definition, in prime]
prime [library]
PrimeField [section, in zmodp]
PrimeField.F_prime [section, in zmodp]
PrimeField.F_prime.p_pr [variable, in zmodp]
PrimeField.p [variable, in zmodp]
primeP [lemma, in prime]
primePn [lemma, in prime]
primePns [lemma, in prime]
primes [definition, in prime]
primes_mul [lemma, in prime]
primes_prime [lemma, in prime]
primes_exp [lemma, in prime]
primes_exponent [lemma, in abelian]
primes_uniq [lemma, in prime]
primes_part [lemma, in prime]
prime_TIg [lemma, in fingroup]
prime_nt_dvdP [lemma, in prime]
prime_subgroupVti [lemma, in pgroup]
prime_decomp [definition, in prime]
prime_decomp [section, in prime]
prime_gt0 [lemma, in prime]
prime_meetG [lemma, in fingroup]
prime_coprime [lemma, in prime]
prime_dvd_bin [lemma, in binomial]
prime_decomp_rec [definition, in prime]
prime_gt1 [lemma, in prime]
prime_decomp_correct [lemma, in prime]
prime_Ohm1P [lemma, in extremal]
prime_abelem [lemma, in abelian]
prime_oddPn [lemma, in prime]
prime_cyclic [lemma, in cyclic]
prime_decompE [lemma, in prime]
Primitive [section, in primitive_action]
primitive [definition, in primitive_action]
PrimitiveDef [section, in primitive_action]
PrimitiveDef.A [variable, in primitive_action]
PrimitiveDef.aT [variable, in primitive_action]
PrimitiveDef.S [variable, in primitive_action]
PrimitiveDef.sT [variable, in primitive_action]
PrimitiveDef.to [variable, in primitive_action]
PrimitiveRoots [section, in cyclic]
primitive_root_of_unity [definition, in poly]
primitive_root_splitting_abelian [lemma, in mxrepresentation]
primitive_action [library]
Primitive.aT [variable, in primitive_action]
Primitive.G [variable, in primitive_action]
Primitive.S [variable, in primitive_action]
Primitive.sT [variable, in primitive_action]
Primitive.to [variable, in primitive_action]
prim_trans_norm [lemma, in primitive_action]
prim_order_dvd [lemma, in poly]
prim_expr_mod [lemma, in poly]
prim_expr_order [lemma, in poly]
prim_order_exists [lemma, in poly]
prim_order_gt0 [lemma, in poly]
prim_rootP [lemma, in poly]
principal_comp [definition, in mxrepresentation]
principal_comp_subproof [lemma, in mxrepresentation]
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]
ProdMorph [section, in gproduct]
ProdMorph.Cprodm [section, in gproduct]
ProdMorph.Cprodm.cfHK [variable, in gproduct]
ProdMorph.Cprodm.eqfHK [variable, in gproduct]
ProdMorph.Cprodm.eqHK_G [variable, in gproduct]
ProdMorph.Cprodm.fH [variable, in gproduct]
ProdMorph.Cprodm.fK [variable, in gproduct]
ProdMorph.Cprodm.G [variable, in gproduct]
ProdMorph.Cprodm.H [variable, in gproduct]
ProdMorph.Cprodm.K [variable, in gproduct]
ProdMorph.defs [section, in gproduct]
ProdMorph.defs.A [variable, in gproduct]
ProdMorph.defs.B [variable, in gproduct]
ProdMorph.defs.fA [variable, in gproduct]
ProdMorph.defs.fB [variable, in gproduct]
ProdMorph.Dprodm [section, in gproduct]
ProdMorph.Dprodm.cfHK [variable, in gproduct]
ProdMorph.Dprodm.eqHK_G [variable, in gproduct]
ProdMorph.Dprodm.fH [variable, in gproduct]
ProdMorph.Dprodm.fK [variable, in gproduct]
ProdMorph.Dprodm.G [variable, in gproduct]
ProdMorph.Dprodm.H [variable, in gproduct]
ProdMorph.Dprodm.K [variable, in gproduct]
ProdMorph.gT [variable, in gproduct]
ProdMorph.Props [section, in gproduct]
ProdMorph.Props.actf [variable, in gproduct]
ProdMorph.Props.eqfHK [variable, in gproduct]
ProdMorph.Props.fH [variable, in gproduct]
ProdMorph.Props.fK [variable, in gproduct]
ProdMorph.Props.H [variable, in gproduct]
ProdMorph.Props.K [variable, in gproduct]
ProdMorph.Props.nHK [variable, in gproduct]
ProdMorph.rT [variable, in gproduct]
ProdMorph.Sdprodm [section, in gproduct]
ProdMorph.Sdprodm.actf [variable, in gproduct]
ProdMorph.Sdprodm.eqHK_G [variable, in gproduct]
ProdMorph.Sdprodm.fH [variable, in gproduct]
ProdMorph.Sdprodm.fK [variable, in gproduct]
ProdMorph.Sdprodm.G [variable, in gproduct]
ProdMorph.Sdprodm.H [variable, in gproduct]
ProdMorph.Sdprodm.K [variable, in gproduct]
prodn_cond_gt0 [lemma, in bigop]
prodn_gt0 [lemma, in bigop]
prodsgP [lemma, in fingroup]
Product [section, in center]
Product.gT [variable, in center]
prodVector [definition, in vector]
ProdVector [section, in vector]
ProdVector.K [variable, in vector]
ProdVector.V [variable, in vector]
ProdVector.W [variable, in vector]
prod_group [definition, in gproduct]
prod_tpermP [lemma, in perm]
prod_finType [definition, in fintype]
prod_constt [lemma, in pgroup]
prod_countMixin [definition, in choice]
prod_prime_decomp [lemma, in prime]
prod_factors_of_unity [lemma, in poly]
prod_choiceMixin [definition, in choice]
prod_enumP [lemma, in fintype]
prod_eqMixin [definition, in eqtype]
prod_finMixin [definition, in fintype]
prod_factors_monic [lemma, in poly]
prod_eqType [definition, in eqtype]
prod_countType [definition, in choice]
prod_choiceType [definition, in choice]
prod_enum [definition, in fintype]
prod_nat_const_nat [lemma, in bigop]
prod_nat_const [lemma, in bigop]
Projection [section, in vector]
Projection.K [variable, in vector]
Projection.Sumv_Pi [section, in vector]
Projection.Sumv_Pi.P [variable, in vector]
Projection.Sumv_Pi.I [variable, in vector]
Projection.Sumv_Pi.V_ [variable, in vector]
Projection.V [variable, in vector]
projv [definition, in vector]
projv_id [lemma, in vector]
proj_mx_0 [lemma, in mxalgebra]
proj_mx_compl_sub [lemma, in mxalgebra]
proj_mx [definition, in mxalgebra]
proj_mx_id [lemma, in mxalgebra]
proj_mx_hom [lemma, in mxrepresentation]
proj_factmodS [lemma, in mxrepresentation]
proj_mx_sub [lemma, in mxalgebra]
proj_mx_proj [lemma, in mxalgebra]
proper [definition, in fintype]
properD [lemma, in finset]
properD1 [lemma, in finset]
properE [lemma, in fintype]
properEcard [lemma, in finset]
properEneq [lemma, in finset]
properG_ltn_log [lemma, in pgroup]
properI [lemma, in finset]
properIl [lemma, in finset]
properIr [lemma, in finset]
properIset [lemma, in finset]
properJ [lemma, in fingroup]
ProperMxsum [constructor, in mxalgebra]
ProperMxsumExpr [constructor, in mxalgebra]
properP [lemma, in fintype]
ProperSumv [constructor, in vector]
ProperSumvExpr [constructor, in vector]
properT [lemma, in finset]
PropertiesDefs [section, in nilpotent]
PropertiesDefs.A [variable, in nilpotent]
PropertiesDefs.gT [variable, in nilpotent]
properU [lemma, in finset]
properUl [lemma, in finset]
properUr [lemma, in finset]
properxx [lemma, in fintype]
proper_mxsum_rank [projection, in mxalgebra]
proper_sub [lemma, in fintype]
proper_neq [lemma, in finset]
proper_mxsumP [definition, in mxalgebra]
proper_subn [lemma, in fintype]
proper_irrefl [lemma, in fintype]
proper_trans [lemma, in fintype]
proper_sub_trans [lemma, in fintype]
proper_card [lemma, in fintype]
proper_mxsum_val [projection, in mxalgebra]
proper_addvP [definition, in vector]
proper_addv_val [projection, in vector]
proper_addv_dim [projection, in vector]
proper_addv_expr [record, in vector]
proper_mxsum_expr [record, in mxalgebra]
proper0 [lemma, in finset]
proper1G [lemma, in fingroup]
proper1set [lemma, in finset]
prop_congr [lemma, in ssrbool]
prop_in3 [definition, in ssrbool]
prop_in111 [definition, in ssrbool]
prop_in21 [definition, in ssrbool]
prop_on1 [definition, in ssrbool]
prop_in12 [definition, in ssrbool]
prop_for [definition, in ssrbool]
prop_on2 [definition, in ssrbool]
prop_in11 [definition, in ssrbool]
prop_in1 [definition, in ssrbool]
prop_in2 [definition, in ssrbool]
protect_term [definition, in ssreflect]
pseries [definition, in pgroup]
PseriesDefs [section, in pgroup]
PseriesDefs.A [variable, in pgroup]
PseriesDefs.gT [variable, in pgroup]
PseriesDefs.pis [variable, in pgroup]
pseriesJ [lemma, in pgroup]
pseriesS [lemma, in pgroup]
pseries_pgFun [definition, in pgroup]
pseries_gFun [definition, in pgroup]
pseries_igFun [definition, in pgroup]
pseries_group [definition, in pgroup]
pseries_subfun [lemma, in pgroup]
pseries_char_catr [lemma, in pgroup]
pseries_rcons_id [lemma, in pgroup]
pseries_norm2 [lemma, in pgroup]
pseries_rcons [lemma, in pgroup]
pseries_catl_id [lemma, in pgroup]
pseries_pop2 [lemma, in pgroup]
pseries_sub_catl [lemma, in pgroup]
pseries_char [lemma, in pgroup]
pseries_catr_id [lemma, in pgroup]
pseries_char_catl [lemma, in pgroup]
pseries_normal [lemma, in pgroup]
pseries_sub_catr [lemma, in pgroup]
pseries_sub [lemma, in pgroup]
pseries_pop [lemma, in pgroup]
pseries_group_set [lemma, in pgroup]
pseries1 [lemma, in pgroup]
psubgroup [definition, in pgroup]
psubgroupJ [lemma, in pgroup]
psubgroup1 [lemma, in pgroup]
pT [abbreviation, in perm]
pvaddE [lemma, in vector]
pval [definition, in perm]
pvalE [lemma, in perm]
pvf [definition, in vector]
pvfK [lemma, in vector]
pvoppE [lemma, in vector]
pvscaleE [lemma, in vector]
pv2p [definition, in vector]
pv2pK [lemma, in vector]
pX1p2id [lemma, in extraspecial]
pX1p2n_pgroup [lemma, in extraspecial]
pX1p2n_extraspecial [lemma, in extraspecial]
pX1p2S [lemma, in extraspecial]
pX1p2_extraspecial [lemma, in extraspecial]
pX1p2_pgroup [lemma, in extraspecial]
pZ [definition, in maximal]
p_rankElem_max [lemma, in abelian]
p_elt_exp [lemma, in pgroup]
p_elt_constt [lemma, in pgroup]
p_group1 [lemma, in pgroup]
p_abelem_split1 [lemma, in maximal]
p_maximal_normal [lemma, in maximal]
p_rankJ [lemma, in abelian]
p_rank_abelem [lemma, in abelian]
p_group [definition, in pgroup]
p_natP [lemma, in prime]
p_elt [definition, in pgroup]
p_eltM_norm [lemma, in pgroup]
p_rank_witness [lemma, in abelian]
p_rank_le_logn [lemma, in abelian]
p_Sylow [lemma, in pgroup]
p_part_eq1 [lemma, in prime]
p_rank_pmaxElem_exists [lemma, in abelian]
p_rank [definition, in abelian]
p_rank_abelian [lemma, in abelian]
p_rank_geP [lemma, in abelian]
p_A [abbreviation, in mxpoly]
p_gt1 [definition, in maximal]
p_eltNK [lemma, in pgroup]
p_groupP [lemma, in pgroup]
p_eltJ [lemma, in pgroup]
p_gt0 [definition, in mxabelem]
p_eltX [lemma, in pgroup]
p_rank_gt0 [lemma, in abelian]
p_part_gt1 [lemma, in prime]
p_rank_Hall [lemma, in abelian]
p_gt1 [definition, in mxabelem]
p_rank1 [lemma, in abelian]
p_gt0 [definition, in maximal]
p_index_maximal [lemma, in maximal]
p_pr [definition, in mxabelem]
p_gt1 [definition, in extremal]
p_maximal_index [lemma, in maximal]
p_pr [definition, in maximal]
p_rank_p'quotient [lemma, in abelian]
p_rank_quotient [lemma, in abelian]
p_rank_Ohm1 [lemma, in abelian]
p_gt1 [definition, in extraspecial]
p_rank_le_rank [lemma, in abelian]
p_core_Fitting [lemma, in maximal]
p_elt1 [lemma, in pgroup]
p_pr [definition, in maximal]
p_eltM [lemma, in pgroup]
p_gt0 [definition, in extremal]
p_eltV [lemma, in pgroup]
p_pr [definition, in mxabelem]
p_part [lemma, in prime]
p_rank_Sylow [lemma, in abelian]
p_rankS [lemma, in abelian]
p_gt0 [definition, in extraspecial]
p_rank_dprod [lemma, in abelian]
p_groupJ [lemma, in pgroup]
p'groupEpi [lemma, in pgroup]
p'group_quotient_cent_prime [lemma, in pgroup]
p'natE [lemma, in prime]
p'natEpi [lemma, in prime]
p'nat_coprime [lemma, in prime]
p'_elt_constt [lemma, in pgroup]
p1ElemE [lemma, in abelian]
p2Elem_dprodP [lemma, in abelian]
p2group_abelian [lemma, in sylow]
p2pv [definition, in vector]
p2pvK [lemma, in vector]
p3group_extraspecial [lemma, in maximal]



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)