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 (lemma)

PackSocleK [in mxrepresentation]
pairg1_morphM [in gproduct]
pairmapK [in seq]
pairmap_cat [in seq]
pairmap_tupleP [in tuple]
pair_big_dep [in bigop]
pair_eqP [in eqtype]
pair_of_tagK [in choice]
pair_big [in bigop]
pair_bigA [in bigop]
pair_eq1 [in eqtype]
pair_eqE [in eqtype]
pair_eq2 [in eqtype]
pair1g_morphM [in gproduct]
partG_eq1 [in pgroup]
partition_big_imset [in finset]
partition_big [in bigop]
partnC [in prime]
partnI [in prime]
partnNK [in prime]
partnT [in prime]
partn_gcd [in prime]
partn_exp [in prime]
partn_part [in prime]
partn_biglcm [in prime]
partn_exponentS [in abelian]
partn_lcm [in prime]
partn_dvd [in prime]
partn_eq1 [in prime]
partn_mul [in prime]
partn_biggcd [in prime]
partn_pi [in prime]
partn0 [in prime]
partn1 [in prime]
part_pnat_id [in prime]
part_pnat [in prime]
part_p'nat [in prime]
part_gt0 [in prime]
Pascal [in binomial]
pathP [in path]
path_cat [in path]
path_rev [in path]
path_connect [in fingraph]
path_sorted [in path]
path_merge [in path]
path_rcons [in path]
path_map [in path]
path_min_sorted [in path]
pcan_inj [in ssrfun]
pcan_pcomp [in ssrfun]
pcan_enumP [in fintype]
pcan_pickleK [in choice]
pcoreI [in pgroup]
pcoreJ [in pgroup]
pcoreNK [in pgroup]
pcoreS [in pgroup]
pcore_modp [in pgroup]
pcore_mod_res [in pgroup]
pcore_sub_Hall [in pgroup]
pcore_mod1 [in pgroup]
pcore_Fitting [in maximal]
pcore_max [in pgroup]
pcore_psubgroup [in pgroup]
pcore_faithful_mx_irr [in mxabelem]
pcore_sub [in pgroup]
pcore_pgroup_id [in pgroup]
pcore_char [in pgroup]
pcore_mod_sub [in pgroup]
pcore_sub_rstab_mxsimple [in mxabelem]
pcore_sub_rker_mx_irr [in mxabelem]
pcore_normal [in pgroup]
pcore_pgroup [in pgroup]
pcore_faithful_irr_act [in sylow]
pcore_sub_astab_irr [in sylow]
pcore_setI_normal [in pgroup]
pcycleE [in action]
pcycle_id [in perm]
pcycle_traject [in perm]
pcycle_actperm [in action]
pcycle_sym [in perm]
pcycle_perm [in perm]
pdivP [in prime]
pdiv_gt0 [in prime]
pdiv_min_dvd [in prime]
pdiv_leq [in prime]
pdiv_prime [in prime]
pdiv_pfactor [in prime]
pdiv_p_elt [in abelian]
pdiv_dvd [in prime]
pdiv_id [in prime]
pElemI [in abelian]
pElemJ [in abelian]
pElemP [in abelian]
pElemS [in abelian]
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]
perm_eqP [in seq]
perm_inj [in perm]
perm_cat2r [in seq]
perm_cat2l [in seq]
perm_oneP [in perm]
perm_eqrP [in seq]
perm_faithful [in action]
perm_eqlP [in seq]
perm_mx_is_perm [in matrix]
perm_mulP [in perm]
perm_onM [in perm]
perm_mx1 [in matrix]
perm_mxM [in matrix]
perm_catAC [in seq]
perm_sort [in path]
perm_invK [in perm]
perm_mact [in action]
perm_uniq [in seq]
perm_filterC [in seq]
perm_onto [in perm]
perm_cons [in seq]
perm_eq_uniq [in seq]
perm_proof [in perm]
perm_eq_size [in seq]
perm_sortP [in path]
perm_eq_refl [in seq]
perm_closed [in perm]
perm_inE [in automorphism]
perm_act1P [in action]
perm_invP [in perm]
perm_eq_trans [in seq]
perm_catC [in seq]
perm_on1 [in perm]
perm_merge [in path]
perm_eq_mem [in seq]
perm_mxV [in matrix]
perm_rot [in seq]
perm_eq_abelian_type [in abelian]
perm_in_on [in automorphism]
perm_in_inj [in automorphism]
perm_rcons [in seq]
perm_eq_sym [in seq]
perm_catCA [in seq]
perm_rotr [in seq]
perm1 [in perm]
Pextraspecial.actP [in extraspecial]
Pextraspecial.gactP [in extraspecial]
pfactorK [in prime]
pfactorKpdiv [in prime]
pfactor_dvdn [in prime]
pfactor_coprime [in prime]
pfactor_gt0 [in prime]
pfactor_dvdnn [in prime]
pfamilyP [in finfun]
pffun_onP [in finfun]
pgroupE [in pgroup]
pgroupJ [in pgroup]
pgroupM [in pgroup]
pgroupNK [in pgroup]
pgroupP [in pgroup]
pgroupS [in pgroup]
pgroup_pi [in pgroup]
pgroup_nil [in sylow]
pgroup_p [in pgroup]
pgroup_sol [in sylow]
pgroup_fix_mod [in sylow]
pgroup_pdiv [in pgroup]
pgroup1 [in pgroup]
pHallE [in pgroup]
pHallJ [in pgroup]
pHallJnorm [in pgroup]
pHallJ2 [in pgroup]
pHallNK [in pgroup]
pHallP [in pgroup]
pHall_id [in pgroup]
pHall_subl [in pgroup]
pHall_Hall [in pgroup]
pHall_sub [in pgroup]
pHall_pgroup [in pgroup]
phiE [in prime]
PhiJ [in maximal]
PhiS [in maximal]
Phi_quotient_id [in maximal]
Phi_proper [in maximal]
phi_gen [in cyclic]
Phi_normal [in maximal]
Phi_quotient_cyclic [in maximal]
phi_coprime [in prime]
Phi_min [in maximal]
phi_pfactor [in prime]
Phi_mulg [in maximal]
Phi_char [in maximal]
Phi_nongen [in maximal]
Phi_cprod [in maximal]
phi_gt0 [in prime]
Phi_joing [in maximal]
Phi_quotient_abelem [in maximal]
Phi_sub_max [in maximal]
Phi_sub [in maximal]
phi_count_coprime [in prime]
pickleK [in choice]
pickleK_inv [in choice]
pickle_invK [in choice]
pickP [in fintype]
pid_mx_block [in matrix]
pid_mx_id [in matrix]
pid_mx_minv [in matrix]
pid_mx_1 [in matrix]
pid_mx_col [in matrix]
pid_mx_minh [in matrix]
pid_mx_row [in matrix]
pid_mx_0 [in matrix]
piOhm1 [in abelian]
piSg [in fingroup]
pi_of_prime [in prime]
pi_max_pdiv [in prime]
pi_of_partn [in prime]
pi_pnat [in prime]
pi_pdiv [in prime]
pi_of_muln [in prime]
pi_of_exponent [in abelian]
pi_center_nilpotent [in sylow]
pi_p'nat [in prime]
pi_of_exp [in prime]
pi_p'group [in pgroup]
pi_pgroup [in pgroup]
pi_of_dvd [in prime]
pi'_p'group [in pgroup]
pi'_p'nat [in prime]
plusE [in ssrnat]
pmapS_filter [in seq]
pmap_uniq [in seq]
pmap_filter [in seq]
pmap_sub_uniq [in seq]
pmaxElemJ [in abelian]
pmaxElemP [in abelian]
pmaxElemS [in abelian]
pmaxElem_LdivP [in abelian]
pmaxElem_exists [in abelian]
pmaxElem_extraspecial [in maximal]
pmorphimF [in gfunctor]
pmorphim_pgroup [in pgroup]
pmorphim_pHall [in pgroup]
pnatE [in prime]
pnatI [in prime]
pnatNK [in prime]
pnatP [in prime]
pnatPpi [in prime]
pnat_div [in prime]
pnat_coprime [in prime]
pnat_1 [in prime]
pnat_mul [in prime]
pnat_dvd [in prime]
pnat_exponent [in abelian]
pnat_exp [in prime]
pnat_id [in prime]
pnat_pi [in prime]
pnElemE [in abelian]
pnElemI [in abelian]
pnElemJ [in abelian]
pnElemP [in abelian]
pnElemPcard [in abelian]
pnElemS [in abelian]
pnElem_prime [in abelian]
pnElem0 [in abelian]
polyC_opp [in poly]
polyC_exp [in poly]
polyC_eq0 [in poly]
polyC_natmul [in poly]
polyC_inj [in poly]
polyC_add [in poly]
polyC_is_rmorphism [in poly]
polyC_mul [in poly]
polyC_sub [in poly]
polyC0 [in poly]
polyC1 [in poly]
PolyK [in poly]
polyP [in poly]
polyseqC [in poly]
polyseqK [in poly]
polyseqX [in poly]
polyseq_cons [in poly]
polyseq_poly [in poly]
polyseq1 [in poly]
polySpred [in poly]
poly_rV_is_linear [in mxpoly]
poly_mulC [in poly]
poly_idomainMixin [in poly]
poly_comp_scall [in poly]
poly_ind [in poly]
poly_cons_def [in poly]
poly_comp_addl [in poly]
poly_compA [in poly]
poly_comp_is_additive [in poly]
poly_comp_subl [in poly]
poly_compE [in poly]
poly_initial [in poly]
poly_com0p [in poly]
poly_comp_amulX [in poly]
poly_comp_rmorphr [in poly]
poly_comXp [in poly]
poly_compC [in poly]
poly_comp_mull [in poly]
poly_comp0 [in poly]
poly_mulVp [in poly]
poly_comp_translateK [in poly]
poly_inj [in poly]
poly_compX [in poly]
poly_intro_unit [in poly]
poly_inv_out [in poly]
poly_def [in poly]
poly_morphX_comm [in poly]
poly_rV_K [in mxpoly]
poly_comp_is_linear [in poly]
poly0Vpos [in poly]
posnP [in ssrnat]
pprodE [in gproduct]
pprodEY [in gproduct]
pprodg1 [in gproduct]
pprodmE [in gproduct]
pprodmEl [in gproduct]
pprodmEr [in gproduct]
pprodmM [in gproduct]
pprodP [in gproduct]
pprod1g [in gproduct]
pquotient_pHall [in pgroup]
pquotient_pcore [in pgroup]
pquotient_pgroup [in pgroup]
predC_closed [in fingraph]
predD1P [in eqtype]
predE [in ssrnat]
prednK [in ssrnat]
predn_subS [in ssrnat]
predn_exp [in binomial]
predn_sub [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]
preimset_proper [in finset]
preimset0 [in finset]
preim_permV [in perm]
preim_partitionP [in finset]
preim_iinv [in fintype]
preim_autE [in automorphism]
prev_cycle [in path]
prev_rev [in path]
prev_rotr [in path]
prev_nth [in path]
prev_rot [in path]
prev_map [in path]
prev_next [in path]
pre_image [in fintype]
primeP [in prime]
primePn [in prime]
primePns [in prime]
primes_mul [in prime]
primes_prime [in prime]
primes_exp [in prime]
primes_exponent [in abelian]
primes_uniq [in prime]
primes_part [in prime]
prime_TIg [in fingroup]
prime_nt_dvdP [in prime]
prime_subgroupVti [in pgroup]
prime_gt0 [in prime]
prime_meetG [in fingroup]
prime_coprime [in prime]
prime_dvd_bin [in binomial]
prime_gt1 [in prime]
prime_decomp_correct [in prime]
prime_Ohm1P [in extremal]
prime_abelem [in abelian]
prime_oddPn [in prime]
prime_cyclic [in cyclic]
prime_decompE [in prime]
primitive_root_splitting_abelian [in mxrepresentation]
prim_trans_norm [in primitive_action]
prim_order_dvd [in poly]
prim_expr_mod [in poly]
prim_expr_order [in poly]
prim_order_exists [in poly]
prim_order_gt0 [in poly]
prim_rootP [in poly]
principal_comp_subproof [in mxrepresentation]
prodn_cond_gt0 [in bigop]
prodn_gt0 [in bigop]
prodsgP [in fingroup]
prod_tpermP [in perm]
prod_constt [in pgroup]
prod_prime_decomp [in prime]
prod_factors_of_unity [in poly]
prod_enumP [in fintype]
prod_factors_monic [in poly]
prod_nat_const_nat [in bigop]
prod_nat_const [in bigop]
projv_id [in vector]
proj_mx_0 [in mxalgebra]
proj_mx_compl_sub [in mxalgebra]
proj_mx_id [in mxalgebra]
proj_mx_hom [in mxrepresentation]
proj_factmodS [in mxrepresentation]
proj_mx_sub [in mxalgebra]
proj_mx_proj [in mxalgebra]
properD [in finset]
properD1 [in finset]
properE [in fintype]
properEcard [in finset]
properEneq [in finset]
properG_ltn_log [in pgroup]
properI [in finset]
properIl [in finset]
properIr [in finset]
properIset [in finset]
properJ [in fingroup]
properP [in fintype]
properT [in finset]
properU [in finset]
properUl [in finset]
properUr [in finset]
properxx [in fintype]
proper_sub [in fintype]
proper_neq [in finset]
proper_subn [in fintype]
proper_irrefl [in fintype]
proper_trans [in fintype]
proper_sub_trans [in fintype]
proper_card [in fintype]
proper0 [in finset]
proper1G [in fingroup]
proper1set [in finset]
prop_congr [in ssrbool]
pseriesJ [in pgroup]
pseriesS [in pgroup]
pseries_subfun [in pgroup]
pseries_char_catr [in pgroup]
pseries_rcons_id [in pgroup]
pseries_norm2 [in pgroup]
pseries_rcons [in pgroup]
pseries_catl_id [in pgroup]
pseries_pop2 [in pgroup]
pseries_sub_catl [in pgroup]
pseries_char [in pgroup]
pseries_catr_id [in pgroup]
pseries_char_catl [in pgroup]
pseries_normal [in pgroup]
pseries_sub_catr [in pgroup]
pseries_sub [in pgroup]
pseries_pop [in pgroup]
pseries_group_set [in pgroup]
pseries1 [in pgroup]
psubgroupJ [in pgroup]
psubgroup1 [in pgroup]
pvaddE [in vector]
pvalE [in perm]
pvfK [in vector]
pvoppE [in vector]
pvscaleE [in vector]
pv2pK [in vector]
pX1p2id [in extraspecial]
pX1p2n_pgroup [in extraspecial]
pX1p2n_extraspecial [in extraspecial]
pX1p2S [in extraspecial]
pX1p2_extraspecial [in extraspecial]
pX1p2_pgroup [in extraspecial]
p_rankElem_max [in abelian]
p_elt_exp [in pgroup]
p_elt_constt [in pgroup]
p_group1 [in pgroup]
p_abelem_split1 [in maximal]
p_maximal_normal [in maximal]
p_rankJ [in abelian]
p_rank_abelem [in abelian]
p_natP [in prime]
p_eltM_norm [in pgroup]
p_rank_witness [in abelian]
p_rank_le_logn [in abelian]
p_Sylow [in pgroup]
p_part_eq1 [in prime]
p_rank_pmaxElem_exists [in abelian]
p_rank_abelian [in abelian]
p_rank_geP [in abelian]
p_eltNK [in pgroup]
p_groupP [in pgroup]
p_eltJ [in pgroup]
p_eltX [in pgroup]
p_rank_gt0 [in abelian]
p_part_gt1 [in prime]
p_rank_Hall [in abelian]
p_rank1 [in abelian]
p_index_maximal [in maximal]
p_maximal_index [in maximal]
p_rank_p'quotient [in abelian]
p_rank_quotient [in abelian]
p_rank_Ohm1 [in abelian]
p_rank_le_rank [in abelian]
p_core_Fitting [in maximal]
p_elt1 [in pgroup]
p_eltM [in pgroup]
p_eltV [in pgroup]
p_part [in prime]
p_rank_Sylow [in abelian]
p_rankS [in abelian]
p_rank_dprod [in abelian]
p_groupJ [in pgroup]
p'groupEpi [in pgroup]
p'group_quotient_cent_prime [in pgroup]
p'natE [in prime]
p'natEpi [in prime]
p'nat_coprime [in prime]
p'_elt_constt [in pgroup]
p1ElemE [in abelian]
p2Elem_dprodP [in abelian]
p2group_abelian [in sylow]
p2pvK [in vector]
p3group_extraspecial [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)