P (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

P (Lemmas)

p'_elt_constt [prf, in mathcomp.solvable.pgroup]
p'group_quotient_cent_prime [prf, in mathcomp.solvable.pgroup]
p'groupEpi [prf, in mathcomp.solvable.pgroup]
p'nat_coprime [prf, in mathcomp.boot.prime]
p'natE [prf, in mathcomp.boot.prime]
p'natEpi [prf, in mathcomp.boot.prime]
p1ElemE [prf, in mathcomp.solvable.abelian]
p2Elem_dprodP [prf, in mathcomp.solvable.abelian]
p2group_abelian [prf, in mathcomp.solvable.sylow]
p3group_extraspecial [prf, in mathcomp.solvable.maximal]
p_abelem_split1 [prf, in mathcomp.solvable.maximal]
p_core_Fitting [prf, in mathcomp.solvable.maximal]
p_elt1 [prf, in mathcomp.solvable.pgroup]
p_elt_constt [prf, in mathcomp.solvable.pgroup]
p_elt_exp [prf, in mathcomp.solvable.pgroup]
p_eltJ [prf, in mathcomp.solvable.pgroup]
p_eltM [prf, in mathcomp.solvable.pgroup]
p_eltM_norm [prf, in mathcomp.solvable.pgroup]
p_eltNK [prf, in mathcomp.solvable.pgroup]
p_eltV [prf, in mathcomp.solvable.pgroup]
p_eltX [prf, in mathcomp.solvable.pgroup]
p_group1 [prf, in mathcomp.solvable.pgroup]
p_groupJ [prf, in mathcomp.solvable.pgroup]
p_groupP [prf, in mathcomp.solvable.pgroup]
p_index_maximal [prf, in mathcomp.solvable.maximal]
p_maximal_index [prf, in mathcomp.solvable.maximal]
p_maximal_normal [prf, in mathcomp.solvable.maximal]
p_natP [prf, in mathcomp.boot.prime]
p_part [prf, in mathcomp.boot.prime]
p_part_eq1 [prf, in mathcomp.boot.prime]
p_part_gt1 [prf, in mathcomp.boot.prime]
p_rank1 [prf, in mathcomp.solvable.abelian]
p_rank_abelem [prf, in mathcomp.solvable.abelian]
p_rank_abelian [prf, in mathcomp.solvable.abelian]
p_rank_dprod [prf, in mathcomp.solvable.abelian]
p_rank_geP [prf, in mathcomp.solvable.abelian]
p_rank_gt0 [prf, in mathcomp.solvable.abelian]
p_rank_Hall [prf, in mathcomp.solvable.abelian]
p_rank_le_logn [prf, in mathcomp.solvable.abelian]
p_rank_le_rank [prf, in mathcomp.solvable.abelian]
p_rank_Ohm1 [prf, in mathcomp.solvable.abelian]
p_rank_p'quotient [prf, in mathcomp.solvable.abelian]
p_rank_pmaxElem_exists [prf, in mathcomp.solvable.abelian]
p_rank_quotient [prf, in mathcomp.solvable.abelian]
p_rank_Sylow [prf, in mathcomp.solvable.abelian]
p_rank_witness [prf, in mathcomp.solvable.abelian]
p_rankElem_max [prf, in mathcomp.solvable.abelian]
p_rankJ [prf, in mathcomp.solvable.abelian]
p_rankS [prf, in mathcomp.solvable.abelian]
p_Sylow [prf, in mathcomp.solvable.pgroup]
PackSocleK [prf, in mathcomp.group_representation.mxrepresentation]
pair1g_morphM [prf, in mathcomp.finite_group.gproduct]
pair_add0r [prf, in mathcomp.boot.nmodule]
pair_addNr [prf, in mathcomp.boot.nmodule]
pair_addrA [prf, in mathcomp.boot.nmodule]
pair_addrC [prf, in mathcomp.boot.nmodule]
pair_big [prf, in mathcomp.boot.bigop]
pair_big_dep [prf, in mathcomp.boot.bigop]
pair_big_dep_idem [prf, in mathcomp.boot.bigop]
pair_big_idem [prf, in mathcomp.boot.bigop]
pair_bigA [prf, in mathcomp.boot.bigop]
pair_bigA_idem [prf, in mathcomp.boot.bigop]
pair_eq1 [prf, in mathcomp.boot.eqtype]
pair_eq2 [prf, in mathcomp.boot.eqtype]
pair_eqE [prf, in mathcomp.boot.eqtype]
pair_eqP [prf, in mathcomp.boot.eqtype]
pair_invr_out [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
pair_mul0r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_mul1g [prf, in mathcomp.boot.monoid]
pair_mul1l [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_mul1r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_mulA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_mulC [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_mulDl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_mulDr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_mulg1 [prf, in mathcomp.boot.monoid]
pair_mulgA [prf, in mathcomp.boot.monoid]
pair_mulgV [prf, in mathcomp.boot.monoid]
pair_mulr0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_mulVg [prf, in mathcomp.boot.monoid]
pair_mulVl [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
pair_mulVr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
pair_of_tagK [prf, in mathcomp.boot.choice]
pair_one_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_scale0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_scale1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_scaleA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_scaleAl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_scaleAr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_scaleDl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_scaleDr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pair_unitP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
pair_vect_iso [prf, in mathcomp.algebra.vector]
pairg1_morphM [prf, in mathcomp.finite_group.gproduct]
pairmap_bseqP [prf, in mathcomp.boot.tuple]
pairmap_cat [prf, in mathcomp.boot.seq]
pairmap_tupleP [prf, in mathcomp.boot.tuple]
pairmapK [prf, in mathcomp.boot.seq]
pairMnE [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pairwise2 [prf, in mathcomp.boot.seq]
pairwise_all2rel [prf, in mathcomp.boot.seq]
pairwise_cat [prf, in mathcomp.boot.seq]
pairwise_cons [prf, in mathcomp.boot.seq]
pairwise_eq [prf, in mathcomp.boot.seq]
pairwise_filter [prf, in mathcomp.boot.seq]
pairwise_map [prf, in mathcomp.boot.seq]
pairwise_mask [prf, in mathcomp.boot.seq]
pairwise_orthogonal_cat [prf, in mathcomp.group_representation.classfun]
pairwise_orthogonal_cat [prf, in mathcomp.algebra.sesquilinear]
pairwise_orthogonalP [prf, in mathcomp.group_representation.classfun]
pairwise_orthogonalP [prf, in mathcomp.algebra.sesquilinear]
pairwise_rcons [prf, in mathcomp.boot.seq]
pairwise_relI [prf, in mathcomp.boot.seq]
pairwise_sort [prf, in mathcomp.boot.path]
pairwise_sorted [prf, in mathcomp.boot.path]
pairwise_trans [prf, in mathcomp.boot.seq]
pairwise_uniq [prf, in mathcomp.boot.seq]
pairwiseP [prf, in mathcomp.boot.seq]
part_gt0 [prf, in mathcomp.boot.prime]
part_p'nat [prf, in mathcomp.boot.prime]
part_pnat [prf, in mathcomp.boot.prime]
part_pnat_id [prf, in mathcomp.boot.prime]
partG_eq1 [prf, in mathcomp.solvable.pgroup]
partition0 [prf, in mathcomp.boot.finset]
partition_big [prf, in mathcomp.boot.bigop]
partition_big_idem [prf, in mathcomp.boot.bigop]
partition_big_imset [prf, in mathcomp.boot.finset]
partition_class_support [prf, in mathcomp.solvable.frobenius]
partition_disjoint_bigcup [prf, in mathcomp.boot.finset]
partition_neq0 [prf, in mathcomp.boot.finset]
partition_normedTI [prf, in mathcomp.solvable.frobenius]
partition_partition [prf, in mathcomp.boot.finset]
partition_pigeonhole [prf, in mathcomp.boot.finset]
partition_set0 [prf, in mathcomp.boot.finset]
partition_trivIset [prf, in mathcomp.boot.finset]
partitionD1 [prf, in mathcomp.boot.finset]
partitionS [prf, in mathcomp.boot.finset]
partitionU1 [prf, in mathcomp.boot.finset]
partn0 [prf, in mathcomp.boot.prime]
partn1 [prf, in mathcomp.boot.prime]
partn_biggcd [prf, in mathcomp.boot.prime]
partn_biglcm [prf, in mathcomp.boot.prime]
partn_dvd [prf, in mathcomp.boot.prime]
partn_eq1 [prf, in mathcomp.boot.prime]
partn_exponentS [prf, in mathcomp.solvable.abelian]
partn_gcd [prf, in mathcomp.boot.prime]
partn_lcm [prf, in mathcomp.boot.prime]
partn_part [prf, in mathcomp.boot.prime]
partn_pi [prf, in mathcomp.boot.prime]
partnC [prf, in mathcomp.boot.prime]
partnI [prf, in mathcomp.boot.prime]
partnM [prf, in mathcomp.boot.prime]
partnNK [prf, in mathcomp.boot.prime]
partnT [prf, in mathcomp.boot.prime]
partnX [prf, in mathcomp.boot.prime]
passmx.coord_rVof [prf, in mathcomp.algebra.vector]
passmx.coord_vecof [prf, in mathcomp.algebra.vector]
passmx.funmx_linear [prf, in mathcomp.algebra.vector]
passmx.hom_vecof [prf, in mathcomp.algebra.vector]
passmx.hommx1 [prf, in mathcomp.algebra.vector]
passmx.hommx_eq0 [prf, in mathcomp.algebra.vector]
passmx.hommx_linear [prf, in mathcomp.algebra.vector]
passmx.hommx_mul [prf, in mathcomp.algebra.vector]
passmx.hommxE [prf, in mathcomp.algebra.vector]
passmx.hommxK [prf, in mathcomp.algebra.vector]
passmx.leigenspaceE [prf, in mathcomp.algebra.vector]
passmx.limgE [prf, in mathcomp.algebra.vector]
passmx.lker_ker [prf, in mathcomp.algebra.vector]
passmx.mem_vecof [prf, in mathcomp.algebra.vector]
passmx.msof0 [prf, in mathcomp.algebra.vector]
passmx.msof_eq0 [prf, in mathcomp.algebra.vector]
passmx.msof_sub [prf, in mathcomp.algebra.vector]
passmx.msofK [prf, in mathcomp.algebra.vector]
passmx.mul_mxof [prf, in mathcomp.algebra.vector]
passmx.mxof1 [prf, in mathcomp.algebra.vector]
passmx.mxof_comp [prf, in mathcomp.algebra.vector]
passmx.mxof_eq0 [prf, in mathcomp.algebra.vector]
passmx.mxof_linear [prf, in mathcomp.algebra.vector]
passmx.mxofK [prf, in mathcomp.algebra.vector]
passmx.rVof_app [prf, in mathcomp.algebra.vector]
passmx.rVof_eq0 [prf, in mathcomp.algebra.vector]
passmx.rVof_linear [prf, in mathcomp.algebra.vector]
passmx.rVof_mul [prf, in mathcomp.algebra.vector]
passmx.rVof_sub [prf, in mathcomp.algebra.vector]
passmx.rVofE [prf, in mathcomp.algebra.vector]
passmx.rVofK [prf, in mathcomp.algebra.vector]
passmx.sub_msof [prf, in mathcomp.algebra.vector]
passmx.sub_vsof [prf, in mathcomp.algebra.vector]
passmx.vecof_delta [prf, in mathcomp.algebra.vector]
passmx.vecof_eq0 [prf, in mathcomp.algebra.vector]
passmx.vecof_linear [prf, in mathcomp.algebra.vector]
passmx.vecof_mul [prf, in mathcomp.algebra.vector]
passmx.vecofK [prf, in mathcomp.algebra.vector]
passmx.vsof0 [prf, in mathcomp.algebra.vector]
passmx.vsof_eq0 [prf, in mathcomp.algebra.vector]
passmx.vsof_sub [prf, in mathcomp.algebra.vector]
passmx.vsofK [prf, in mathcomp.algebra.vector]
path_connect [prf, in mathcomp.boot.fingraph]
path_filter [prf, in mathcomp.boot.path]
path_filter_in [prf, in mathcomp.boot.path]
path_le [prf, in mathcomp.boot.path]
path_map [prf, in mathcomp.boot.path]
path_mask [prf, in mathcomp.boot.path]
path_mask_in [prf, in mathcomp.boot.path]
path_min_sorted [prf, in mathcomp.boot.path]
path_pairwise [prf, in mathcomp.boot.path]
path_pairwise_in [prf, in mathcomp.boot.path]
path_relI [prf, in mathcomp.boot.path]
path_sorted [prf, in mathcomp.boot.path]
path_sorted_inE [prf, in mathcomp.boot.path]
path_sortedE [prf, in mathcomp.boot.path]
pathP [prf, in mathcomp.boot.path]
pblock_equivalence [prf, in mathcomp.boot.finset]
pblock_equivalence_partition [prf, in mathcomp.boot.finset]
pblock_inj [prf, in mathcomp.boot.finset]
pblock_mem [prf, in mathcomp.boot.finset]
pblock_transversal [prf, in mathcomp.boot.finset]
pblockK [prf, in mathcomp.boot.finset]
pcan_enumP [prf, in mathcomp.boot.fintype]
pcan_pickleK [prf, in mathcomp.boot.choice]
PCanHasChoice [prf, in mathcomp.boot.choice]
pchar0_PET [prf, in mathcomp.field.separable]
pchar_Fp [prf, in mathcomp.algebra.zmodp]
pchar_Fp_0 [prf, in mathcomp.algebra.zmodp]
pchar_poly [prf, in mathcomp.algebra.poly]
pchar_prim_root [prf, in mathcomp.algebra.poly]
pchar_qpoly [prf, in mathcomp.algebra.qpoly]
pchar_Zp [prf, in mathcomp.algebra.zmodp]
pcharf0_separable [prf, in mathcomp.field.separable]
pcharf_n_separable [prf, in mathcomp.field.separable]
pcharf_p_separable [prf, in mathcomp.field.separable]
pcore_char [prf, in mathcomp.solvable.pgroup]
pcore_faithful_irr_act [prf, in mathcomp.solvable.sylow]
pcore_faithful_mx_irr_pchar [prf, in mathcomp.group_representation.mxabelem]
pcore_Fitting [prf, in mathcomp.solvable.maximal]
pcore_max [prf, in mathcomp.solvable.pgroup]
pcore_mod1 [prf, in mathcomp.solvable.pgroup]
pcore_mod_res [prf, in mathcomp.solvable.pgroup]
pcore_mod_sub [prf, in mathcomp.solvable.pgroup]
pcore_modp [prf, in mathcomp.solvable.pgroup]
pcore_normal [prf, in mathcomp.solvable.pgroup]
pcore_pgroup [prf, in mathcomp.solvable.pgroup]
pcore_pgroup_id [prf, in mathcomp.solvable.pgroup]
pcore_psubgroup [prf, in mathcomp.solvable.pgroup]
pcore_setI_normal [prf, in mathcomp.solvable.pgroup]
pcore_sub [prf, in mathcomp.solvable.pgroup]
pcore_sub_astab_irr [prf, in mathcomp.solvable.sylow]
pcore_sub_Hall [prf, in mathcomp.solvable.pgroup]
pcore_sub_rker_mx_irr_pchar [prf, in mathcomp.group_representation.mxabelem]
pcore_sub_rstab_mxsimple_pchar [prf, in mathcomp.group_representation.mxabelem]
pcoreI [prf, in mathcomp.solvable.pgroup]
pcoreJ [prf, in mathcomp.solvable.pgroup]
pcoreNK [prf, in mathcomp.solvable.pgroup]
pcoreS [prf, in mathcomp.solvable.pgroup]
Pdeg2.Field.deg2_poly_canonical [prf, in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_factor [prf, in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_root1 [prf, in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_root2 [prf, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_canonical [prf, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_factor [prf, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_root1 [prf, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_root2 [prf, in mathcomp.algebra.poly]
Pdiv.ClosedField.coprimepP [prf, in mathcomp.algebra.polydiv]
Pdiv.ClosedField.root_coprimep [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Bezout_coprimepP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Bezout_coprimepPn [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Bezoutp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprime0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprime1p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_addl_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_comp_poly [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_def [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_div_gcd [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_dvdl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_dvdr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_expl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_expr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_gdco [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_modl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_modr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_pexpl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_pexpr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_root [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_size_gcd [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_sym [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_XsubC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_XsubC2 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepMl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepMr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepPn [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepX [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepZl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepZr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.div0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp_dvd [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp_eq0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divp_small [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.divpN0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvd0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvd0pP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvd1p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvd_eqp_divl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_add [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_add_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_addl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_addr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_comp_poly [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_div_eq0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_eqp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp2l [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp2r [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp_sub [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp_XsubCP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcd [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcd_idl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcd_idr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcdl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcdlr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gcdr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_gdco [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_leq [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mod [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mul2l [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mul2r [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mul_XsubC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mulIl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mulIr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_mulr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_Pexp2l [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_pexp2r [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_prod_XsubC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_size_eqp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_sub [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_subl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_subr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_trans [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_XsubCl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpN0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpNl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpNr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpZl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpZr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdUp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdp_recP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdpE [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdpP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eq_dvdp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp01 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_coprimepl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_coprimepr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_div_XsubC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_dvdl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_dvdr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_exp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_gcd [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_gcdl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_gcdr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_ltrans [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_monic [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_mul2l [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_mul2r [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_mulr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_rdiv_div [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_rgcd_gcd [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_rmod_mod [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_root [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_rtrans [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_scale [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_size [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_sym [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqp_trans [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqpP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqpW [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.eqpxx [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_dvdp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_dvdpl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_dvdpr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_gcdpl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.Gauss_gcdpr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcd0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcd1p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_addl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_addl_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_addr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_comp_poly [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_def [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_eq0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_eqp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_exp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_modl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_modr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_mul2l [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_mul2r [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_mulr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_scalel [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_scaler [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdpC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdpE [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdpp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gdcop0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gdcop_recP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gdcopP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gtNdvdp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.irredp_neq0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.irredp_XaddC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.irredp_XsubC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.irredp_XsubCP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_divp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_divpl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_divpr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_gcdpl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_gcdpr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.leq_modp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.ltn_divpl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.ltn_divpr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.ltn_modp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.ltn_modpN0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.mod0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_coprime [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_eq0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_eq0P [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_id [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_mulr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_small [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modp_XsubC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modpC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.modpp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.mulp_gcdl [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.mulp_gcdr [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.polyC_eqp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.polyXsubC_eqp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.polyXsubCP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.rcoprimep_coprimep [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_biggcd [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_bigmul [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_dvdp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_factor_theorem [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_gcd [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.root_gdco [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.scalp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size2_dvdp_gdco [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size_divp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size_gcd1p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size_gcdp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.size_poly_eq1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.uniq_roots_dvdp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.comm_redivpP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.leq_rdivp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.leq_rmodp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.ltn_rmodp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.ltn_rmodpN0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.Nrdvdp_small [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdiv0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdivp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdivp_small [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvd0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvd0pP [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvd1p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdp_leq [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdpN0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.redivp_def [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.redivp_key [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgcd0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgcdp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgcdpE [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgdcop0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmod0p [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp_eq0 [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp_eq0P [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp_small [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodpC [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodpp [prf, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rscalp_small [prf, in mathcomp.algebra.polydiv]
Pdiv.ComRing.rdivp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.ComRing.rdvdp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.ComRing.rdvdp_eqP [prf, in mathcomp.algebra.polydiv]
Pdiv.ComRing.redivpP [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.Bezout_eq1_coprimepP [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.coprimep_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.cubic_irreducible [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_addl_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_addl_mul_small [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_divl [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_modpP [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_mulA [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_mulAC [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_mulCA [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_pmul2l [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divp_pmul2r [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpAC [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpD [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpE [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpK [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpKC [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpN [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpp [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpP [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpZl [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.divpZr [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_eq_div [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_eq_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_gdcor [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.dvdp_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.dvdpE [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.dvdpP [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.edivp_def [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.edivp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.edivp_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.edivpP [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.egcdp_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_div [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_divl [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_divr [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_gdcol [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_gdcor [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_mod [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_modpl [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_modpr [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqp_rgdco_gdco [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqpf_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.eqpfP [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.expp_sub [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.gcdp_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.gdcop_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.gdcop_rec_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.horner_mod [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.leq_divMp [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.map_divp [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.map_modp [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modNp [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modp_addl_mul_small [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modp_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modpD [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modpE [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modpN [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modpP [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modpZl [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.modpZr [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mu_prod_XsubC [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mulKp [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mulpK [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mup_geq [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mup_leq [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mup_ltn [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mup_XsubCX [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mupM [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mupMl [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mupMr [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.mupNroot [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.prod_XsubC_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.redivp_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.reducible_cubic_root [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.scalp_map [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.scalpE [prf, in mathcomp.algebra.polydiv]
Pdiv.Field.XsubC_dvd [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.edivp_key [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.divp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.divpE [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.divpp [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.drop_poly_divp [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.dvdp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.dvdpP [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.modpE [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.mulKp [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.mulpK [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.scalpE [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.take_poly_modp [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_addl_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_addl_mul_small [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_divl [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_mulA [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_mulAC [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_mulCA [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_pmul2l [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divp_pmul2r [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpAC [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpD [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpK [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpKC [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpN [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpp [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpP [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpZl [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpZr [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.dvdp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.dvdp_eq_div [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.dvdp_eq_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.dvdpP [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.edivpP [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.eqp_divl [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.eqp_modpl [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.expp_sub [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.leq_divMp [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modp_addl_mul_small [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modp_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpD [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpN [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpP [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpZl [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpZr [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.mulKp [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.mulpK [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.ucl_eqp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.ulc_eqpP [prf, in mathcomp.algebra.polydiv]
Pdiv.Ring.polyXsubCP [prf, in mathcomp.algebra.polydiv]
Pdiv.Ring.rdivp1 [prf, in mathcomp.algebra.polydiv]
Pdiv.Ring.rdvdp_XsubCl [prf, in mathcomp.algebra.polydiv]
Pdiv.Ring.root_factor_theorem [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.eq_rdvdp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdivp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdivpK [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdivpp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdvdp_eqP [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdvdp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rdvdpp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.redivp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rmodp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.RingComRreg.rmodpp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.drop_poly_rdivp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.eq_rdvdp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_addl_mul [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_addl_mul_small [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpDl [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpDr [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpK [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdvdp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdvdpP [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdvdpp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.redivp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_addl_mul_small [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_compr [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_id [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_mull [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_mulml [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_mulmr [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_sum [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpB [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpD [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpN [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpp [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpX [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpZ [prf, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.take_poly_rmodp [prf, in mathcomp.algebra.polydiv]
Pdiv.UnitRing.uniq_roots_rdvdp [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divpE [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divpK [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divpKC [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.divpp [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.dvdp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.dvdpE [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.dvdpP [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.edivp_def [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.edivp_eq [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.edivp_redivp [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.edivpP [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.lc_expn_scalp_neq0 [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.modpE [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.mulKp [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.mulpK [prf, in mathcomp.algebra.polydiv]
Pdiv.WeakIdomain.scalpE [prf, in mathcomp.algebra.polydiv]
pdiv_dvd [prf, in mathcomp.boot.prime]
pdiv_gt0 [prf, in mathcomp.boot.prime]
pdiv_id [prf, in mathcomp.boot.prime]
pdiv_leq [prf, in mathcomp.boot.prime]
pdiv_min_dvd [prf, in mathcomp.boot.prime]
pdiv_p_elt [prf, in mathcomp.solvable.abelian]
pdiv_pfactor [prf, in mathcomp.boot.prime]
pdiv_prime [prf, in mathcomp.boot.prime]
pdivP [prf, in mathcomp.boot.prime]
pElemI [prf, in mathcomp.solvable.abelian]
pElemJ [prf, in mathcomp.solvable.abelian]
pElemP [prf, in mathcomp.solvable.abelian]
pElemS [prf, in mathcomp.solvable.abelian]
perm1 [prf, in mathcomp.finite_group.perm]
perm_act1P [prf, in mathcomp.finite_group.action]
perm_addr1X [prf, in mathcomp.algebra.zmodp]
perm_all [prf, in mathcomp.boot.seq]
perm_allpairs [prf, in mathcomp.boot.seq]
perm_allpairs_catr [prf, in mathcomp.boot.seq]
perm_allpairs_consr [prf, in mathcomp.boot.seq]
perm_allpairs_dep [prf, in mathcomp.boot.seq]
perm_basis [prf, in mathcomp.algebra.vector]
perm_big [prf, in mathcomp.boot.bigop]
perm_big_supp [prf, in mathcomp.boot.bigop]
perm_big_supp_cond [prf, in mathcomp.boot.bigop]
perm_bigcprod [prf, in mathcomp.finite_group.gproduct]
perm_cat [prf, in mathcomp.boot.seq]
perm_cat2l [prf, in mathcomp.boot.seq]
perm_cat2r [prf, in mathcomp.boot.seq]
perm_catAC [prf, in mathcomp.boot.seq]
perm_catACA [prf, in mathcomp.boot.seq]
perm_catC [prf, in mathcomp.boot.seq]
perm_catCA [prf, in mathcomp.boot.seq]
perm_catl [prf, in mathcomp.boot.seq]
perm_catr [prf, in mathcomp.boot.seq]
perm_closed [prf, in mathcomp.finite_group.perm]
perm_cons [prf, in mathcomp.boot.seq]
perm_consP [prf, in mathcomp.boot.seq]
perm_count_undup [prf, in mathcomp.boot.seq]
perm_faithful [prf, in mathcomp.finite_group.action]
perm_filter [prf, in mathcomp.boot.seq]
perm_filterC [prf, in mathcomp.boot.seq]
perm_flatten [prf, in mathcomp.boot.seq]
perm_free [prf, in mathcomp.algebra.vector]
perm_has [prf, in mathcomp.boot.seq]
perm_in_inj [prf, in mathcomp.finite_group.automorphism]
perm_in_on [prf, in mathcomp.finite_group.automorphism]
perm_inE [prf, in mathcomp.finite_group.automorphism]
perm_inj [prf, in mathcomp.finite_group.perm]
perm_invK [prf, in mathcomp.finite_group.perm]
perm_invP [prf, in mathcomp.finite_group.perm]
perm_iota_sort [prf, in mathcomp.boot.path]
perm_iotaP [prf, in mathcomp.boot.seq]
perm_mact [prf, in mathcomp.finite_group.action]
perm_map [prf, in mathcomp.boot.seq]
perm_map_inj [prf, in mathcomp.boot.seq]
perm_mem [prf, in mathcomp.boot.seq]
perm_merge [prf, in mathcomp.boot.path]
perm_mulP [prf, in mathcomp.finite_group.perm]
perm_mx1 [prf, in mathcomp.algebra.matrix]
perm_mx_is_perm [prf, in mathcomp.algebra.matrix]
perm_mxEsub [prf, in mathcomp.algebra.matrix]
perm_mxM [prf, in mathcomp.algebra.matrix]
perm_mxV [prf, in mathcomp.algebra.matrix]
perm_nilP [prf, in mathcomp.boot.seq]
perm_on1 [prf, in mathcomp.finite_group.perm]
perm_on_id [prf, in mathcomp.finite_group.perm]
perm_onC [prf, in mathcomp.finite_group.perm]
perm_oneP [prf, in mathcomp.finite_group.perm]
perm_onM [prf, in mathcomp.finite_group.perm]
perm_onto [prf, in mathcomp.finite_group.perm]
perm_onV [prf, in mathcomp.finite_group.perm]
perm_permutations [prf, in mathcomp.boot.seq]
perm_pmap [prf, in mathcomp.boot.seq]
perm_prime_astab [prf, in mathcomp.finite_group.action]
perm_prime_atrans [prf, in mathcomp.finite_group.action]
perm_prime_orbit [prf, in mathcomp.finite_group.action]
perm_proof [prf, in mathcomp.finite_group.perm]
perm_rcons [prf, in mathcomp.boot.seq]
perm_refl [prf, in mathcomp.boot.seq]
perm_rev [prf, in mathcomp.boot.seq]
perm_rot [prf, in mathcomp.boot.seq]
perm_rotr [prf, in mathcomp.boot.seq]
perm_size [prf, in mathcomp.boot.seq]
perm_small_eq [prf, in mathcomp.boot.seq]
perm_sort [prf, in mathcomp.boot.path]
perm_sort_inP [prf, in mathcomp.boot.path]
perm_sortP [prf, in mathcomp.boot.path]
perm_sumn [prf, in mathcomp.boot.seq]
perm_sym [prf, in mathcomp.boot.seq]
perm_tact [prf, in mathcomp.finite_group.perm]
perm_tally [prf, in mathcomp.boot.seq]
perm_tally_seq [prf, in mathcomp.boot.seq]
perm_to_rem [prf, in mathcomp.boot.seq]
perm_to_subseq [prf, in mathcomp.boot.seq]
perm_trans [prf, in mathcomp.boot.seq]
perm_undup [prf, in mathcomp.boot.seq]
perm_uniq [prf, in mathcomp.boot.seq]
perm_zip1 [prf, in mathcomp.boot.seq]
perm_zip2 [prf, in mathcomp.boot.seq]
perm_zip_sym [prf, in mathcomp.boot.seq]
permE [prf, in mathcomp.finite_group.perm]
permEl [prf, in mathcomp.boot.seq]
permJ [prf, in mathcomp.finite_group.perm]
permK [prf, in mathcomp.finite_group.perm]
permKV [prf, in mathcomp.finite_group.perm]
permM [prf, in mathcomp.finite_group.perm]
permP [prf, in mathcomp.finite_group.perm]
permP [prf, in mathcomp.boot.seq]
permPl [prf, in mathcomp.boot.seq]
permPr [prf, in mathcomp.boot.seq]
permS0 [prf, in mathcomp.finite_group.perm]
permS01 [prf, in mathcomp.finite_group.perm]
permS1 [prf, in mathcomp.finite_group.perm]
permutations_all_uniq [prf, in mathcomp.boot.seq]
permutations_uniq [prf, in mathcomp.boot.seq]
permutationsE [prf, in mathcomp.boot.seq]
permutationsErot [prf, in mathcomp.boot.seq]
permX [prf, in mathcomp.finite_group.perm]
permX_fix [prf, in mathcomp.finite_group.perm]
pexpIrz [prf, in mathcomp.algebra.ssrint]
pexprz_eq1 [prf, in mathcomp.algebra.ssrint]
Pextraspecial.actP [prf, in mathcomp.solvable.extraspecial]
Pextraspecial.gactP [prf, in mathcomp.solvable.extraspecial]
Pextraspecial.gtype_key [prf, in mathcomp.solvable.extraspecial]
pfactor_coprime [prf, in mathcomp.boot.prime]
pfactor_dvdn [prf, in mathcomp.boot.prime]
pfactor_dvdnn [prf, in mathcomp.boot.prime]
pfactor_gt0 [prf, in mathcomp.boot.prime]
pfactorK [prf, in mathcomp.boot.prime]
pfactorKpdiv [prf, in mathcomp.boot.prime]
pfamilyP [prf, in mathcomp.boot.finfun]
pffun_onP [prf, in mathcomp.boot.finfun]
pFrobenius_aut_int [prf, in mathcomp.algebra.ssrint]
pFrobenius_autMz [prf, in mathcomp.algebra.ssrint]
pgroup1 [prf, in mathcomp.solvable.pgroup]
pgroup_cyclic_faithful [prf, in mathcomp.group_representation.character]
pgroup_fix_mod [prf, in mathcomp.solvable.sylow]
pgroup_nil [prf, in mathcomp.solvable.sylow]
pgroup_p [prf, in mathcomp.solvable.pgroup]
pgroup_pdiv [prf, in mathcomp.solvable.pgroup]
pgroup_pi [prf, in mathcomp.solvable.pgroup]
pgroup_sol [prf, in mathcomp.solvable.sylow]
pgroupE [prf, in mathcomp.solvable.pgroup]
pgroupJ [prf, in mathcomp.solvable.pgroup]
pgroupM [prf, in mathcomp.solvable.pgroup]
pgroupNK [prf, in mathcomp.solvable.pgroup]
pgroupP [prf, in mathcomp.solvable.pgroup]
pgroupS [prf, in mathcomp.solvable.pgroup]
pHall_Hall [prf, in mathcomp.solvable.pgroup]
pHall_id [prf, in mathcomp.solvable.pgroup]
pHall_pgroup [prf, in mathcomp.solvable.pgroup]
pHall_sub [prf, in mathcomp.solvable.pgroup]
pHall_subl [prf, in mathcomp.solvable.pgroup]
pHallE [prf, in mathcomp.solvable.pgroup]
pHallJ [prf, in mathcomp.solvable.pgroup]
pHallJ2 [prf, in mathcomp.solvable.pgroup]
pHallJnorm [prf, in mathcomp.solvable.pgroup]
pHallNK [prf, in mathcomp.solvable.pgroup]
pHallP [prf, in mathcomp.solvable.pgroup]
Phi_char [prf, in mathcomp.solvable.maximal]
Phi_cprod [prf, in mathcomp.solvable.maximal]
Phi_joing [prf, in mathcomp.solvable.maximal]
Phi_Mho [prf, in mathcomp.solvable.maximal]
Phi_min [prf, in mathcomp.solvable.maximal]
Phi_mulg [prf, in mathcomp.solvable.maximal]
Phi_nongen [prf, in mathcomp.solvable.maximal]
Phi_normal [prf, in mathcomp.solvable.maximal]
Phi_proper [prf, in mathcomp.solvable.maximal]
Phi_quotient_abelem [prf, in mathcomp.solvable.maximal]
Phi_quotient_cyclic [prf, in mathcomp.solvable.maximal]
Phi_quotient_id [prf, in mathcomp.solvable.maximal]
Phi_sub [prf, in mathcomp.solvable.maximal]
Phi_sub_max [prf, in mathcomp.solvable.maximal]
PhiJ [prf, in mathcomp.solvable.maximal]
PhiS [prf, in mathcomp.solvable.maximal]
pi'_p'group [prf, in mathcomp.solvable.pgroup]
pi'_p'nat [prf, in mathcomp.boot.prime]
pi_center_nilpotent [prf, in mathcomp.solvable.sylow]
pi_is_monoid_morphism [prf, in mathcomp.algebra.ring_quotient]
pi_is_zmod_morphism [prf, in mathcomp.algebra.ring_quotient]
pi_max_pdiv [prf, in mathcomp.boot.prime]
pi_mono1 [prf, in mathcomp.boot.generic_quotient]
pi_mono2 [prf, in mathcomp.boot.generic_quotient]
pi_morph1 [prf, in mathcomp.boot.generic_quotient]
pi_morph11 [prf, in mathcomp.boot.generic_quotient]
pi_morph2 [prf, in mathcomp.boot.generic_quotient]
pi_of_dvd [prf, in mathcomp.boot.prime]
pi_of_exp [prf, in mathcomp.boot.prime]
pi_of_exponent [prf, in mathcomp.solvable.abelian]
pi_of_part [prf, in mathcomp.boot.prime]
pi_of_prime [prf, in mathcomp.boot.prime]
pi_ofM [prf, in mathcomp.boot.prime]
pi_p'group [prf, in mathcomp.solvable.pgroup]
pi_p'nat [prf, in mathcomp.boot.prime]
pi_pdiv [prf, in mathcomp.boot.prime]
pi_pgroup [prf, in mathcomp.solvable.pgroup]
pi_pnat [prf, in mathcomp.boot.prime]
pi_subfext_add [prf, in mathcomp.field.fieldext]
pi_subfext_inv [prf, in mathcomp.field.fieldext]
pi_subfext_mul [prf, in mathcomp.field.fieldext]
pi_subfext_opp [prf, in mathcomp.field.fieldext]
pi_subfx_inj [prf, in mathcomp.field.fieldext]
pick_set1 [prf, in mathcomp.boot.finset]
pickle_invK [prf, in mathcomp.boot.choice]
pickle_seqK [prf, in mathcomp.boot.choice]
pickle_taggedK [prf, in mathcomp.boot.choice]
pickleK_inv [prf, in mathcomp.boot.choice]
pickP [prf, in mathcomp.boot.fintype]
pid_mx_0 [prf, in mathcomp.algebra.matrix]
pid_mx_1 [prf, in mathcomp.algebra.matrix]
pid_mx_block [prf, in mathcomp.algebra.matrix]
pid_mx_col [prf, in mathcomp.algebra.matrix]
pid_mx_id [prf, in mathcomp.algebra.matrix]
pid_mx_key [prf, in mathcomp.algebra.matrix]
pid_mx_minh [prf, in mathcomp.algebra.matrix]
pid_mx_minv [prf, in mathcomp.algebra.matrix]
pid_mx_row [prf, in mathcomp.algebra.matrix]
pid_mxEcol [prf, in mathcomp.algebra.matrix]
pid_mxErow [prf, in mathcomp.algebra.matrix]
pinvmx_free [prf, in mathcomp.algebra.mxalgebra]
pinvmx_full [prf, in mathcomp.algebra.mxalgebra]
pinvmx_unitary [prf, in mathcomp.algebra.spectral]
pinvmxE [prf, in mathcomp.algebra.mxalgebra]
piOhm1 [prf, in mathcomp.solvable.abelian]
piP [prf, in mathcomp.boot.generic_quotient]
piSg [prf, in mathcomp.finite_group.fingroup]
plogp0 [prf, in mathcomp.field.qfpoly]
plogp1 [prf, in mathcomp.field.qfpoly]
plogp_div_eq0 [prf, in mathcomp.field.qfpoly]
plogp_lt [prf, in mathcomp.field.qfpoly]
plogp_X [prf, in mathcomp.field.qfpoly]
plogpD [prf, in mathcomp.field.qfpoly]
plusE [prf, in mathcomp.boot.ssrnat]
pmap_cat [prf, in mathcomp.boot.seq]
pmap_filter [prf, in mathcomp.boot.seq]
pmap_sub_uniq [prf, in mathcomp.boot.seq]
pmap_uniq [prf, in mathcomp.boot.seq]
pmapS_filter [prf, in mathcomp.boot.seq]
pmaxElem_exists [prf, in mathcomp.solvable.abelian]
pmaxElem_extraspecial [prf, in mathcomp.solvable.maximal]
pmaxElem_LdivP [prf, in mathcomp.solvable.abelian]
pmaxElemJ [prf, in mathcomp.solvable.abelian]
pmaxElemP [prf, in mathcomp.solvable.abelian]
pmaxElemS [prf, in mathcomp.solvable.abelian]
pmorphim_pgroup [prf, in mathcomp.solvable.pgroup]
pmorphim_pHall [prf, in mathcomp.solvable.pgroup]
pmorphimF [prf, in mathcomp.solvable.gfunctor]
pmulrn [prf, in mathcomp.algebra.ssrint]
pmulrz_lge0 [prf, in mathcomp.algebra.ssrint]
pmulrz_lgt0 [prf, in mathcomp.algebra.ssrint]
pmulrz_lle0 [prf, in mathcomp.algebra.ssrint]
pmulrz_llt0 [prf, in mathcomp.algebra.ssrint]
pmulrz_rge0 [prf, in mathcomp.algebra.ssrint]
pmulrz_rgt0 [prf, in mathcomp.algebra.ssrint]
pmulrz_rle0 [prf, in mathcomp.algebra.ssrint]
pmulrz_rlt0 [prf, in mathcomp.algebra.ssrint]
pnat_1 [prf, in mathcomp.boot.prime]
pnat_coprime [prf, in mathcomp.boot.prime]
pnat_div [prf, in mathcomp.boot.prime]
pnat_dvd [prf, in mathcomp.boot.prime]
pnat_exponent [prf, in mathcomp.solvable.abelian]
pnat_id [prf, in mathcomp.boot.prime]
pnat_pi [prf, in mathcomp.boot.prime]
pnatE [prf, in mathcomp.boot.prime]
pnatI [prf, in mathcomp.boot.prime]
pnatM [prf, in mathcomp.boot.prime]
pnatNK [prf, in mathcomp.boot.prime]
pnatP [prf, in mathcomp.boot.prime]
pnatPpi [prf, in mathcomp.boot.prime]
pnatX [prf, in mathcomp.boot.prime]
pnElem0 [prf, in mathcomp.solvable.abelian]
pnElem_prime [prf, in mathcomp.solvable.abelian]
pnElemE [prf, in mathcomp.solvable.abelian]
pnElemI [prf, in mathcomp.solvable.abelian]
pnElemJ [prf, in mathcomp.solvable.abelian]
pnElemP [prf, in mathcomp.solvable.abelian]
pnElemPcard [prf, in mathcomp.solvable.abelian]
pnElemS [prf, in mathcomp.solvable.abelian]
poly0Vpos [prf, in mathcomp.algebra.poly]
poly1_neq0 [prf, in mathcomp.algebra.poly]
poly2_root [prf, in mathcomp.algebra.poly]
poly_alg_initial [prf, in mathcomp.algebra.poly]
poly_algR_pfactor [prf, in mathcomp.field.algC]
poly_def [prf, in mathcomp.algebra.poly]
poly_even_odd [prf, in mathcomp.algebra.poly]
poly_idomainAxiom [prf, in mathcomp.algebra.poly]
poly_ind [prf, in mathcomp.algebra.poly]
poly_initial [prf, in mathcomp.algebra.poly]
poly_inj [prf, in mathcomp.algebra.poly]
poly_intro_unit [prf, in mathcomp.algebra.poly]
poly_inv_out [prf, in mathcomp.algebra.poly]
poly_invE [prf, in mathcomp.algebra.poly]
poly_key [prf, in mathcomp.algebra.poly]
poly_morphX_comm [prf, in mathcomp.algebra.poly]
poly_mul_comm [prf, in mathcomp.algebra.poly]
poly_mulVp [prf, in mathcomp.algebra.poly]
poly_of_qpoly_sum [prf, in mathcomp.algebra.qpoly]
poly_of_qpolyD [prf, in mathcomp.algebra.qpoly]
poly_of_qpolyM [prf, in mathcomp.algebra.qpoly]
poly_of_qpolyX [prf, in mathcomp.algebra.qpoly]
poly_of_qpolyZ [prf, in mathcomp.algebra.qpoly]
poly_of_size_mod [prf, in mathcomp.algebra.qpoly]
poly_rV_is_linear [prf, in mathcomp.algebra.mxpoly]
poly_rV_is_semilinear [prf, in mathcomp.algebra.mxpoly]
poly_rV_K [prf, in mathcomp.algebra.mxpoly]
poly_square_freeP [prf, in mathcomp.field.separable]
poly_take_drop [prf, in mathcomp.algebra.poly]
poly_unitE [prf, in mathcomp.algebra.poly]
poly_XaY0 [prf, in mathcomp.algebra.polyXY]
poly_XaY_eq0 [prf, in mathcomp.algebra.polyXY]
poly_XmY0 [prf, in mathcomp.algebra.polyXY]
poly_XmY_eq0 [prf, in mathcomp.algebra.polyXY]
polyC0 [prf, in mathcomp.algebra.poly]
polyC1 [prf, in mathcomp.algebra.poly]
polyC_eq0 [prf, in mathcomp.algebra.poly]
polyC_exp [prf, in mathcomp.algebra.poly]
polyC_inj [prf, in mathcomp.algebra.poly]
polyC_is_monoid_morphism [prf, in mathcomp.algebra.poly]
polyC_natr [prf, in mathcomp.algebra.poly]
polyCB [prf, in mathcomp.algebra.poly]
polyCD [prf, in mathcomp.algebra.poly]
polyCK [prf, in mathcomp.algebra.poly]
polyCM [prf, in mathcomp.algebra.poly]
polyCMn [prf, in mathcomp.algebra.poly]
polyCMz [prf, in mathcomp.algebra.ssrint]
polyCN [prf, in mathcomp.algebra.poly]
polyCV [prf, in mathcomp.algebra.poly]
PolyK [prf, in mathcomp.algebra.poly]
polyn_is_semilinear [prf, in mathcomp.algebra.qpoly]
polyOver0 [prf, in mathcomp.algebra.poly]
polyOver1P [prf, in mathcomp.field.falgebra]
polyOver_comp [prf, in mathcomp.algebra.poly]
polyOver_deriv [prf, in mathcomp.algebra.poly]
polyOver_derivn [prf, in mathcomp.algebra.poly]
polyOver_dvdzP [prf, in mathcomp.algebra.intdiv]
polyOver_mul1_closed [prf, in mathcomp.algebra.poly]
polyOver_mulr_2closed [prf, in mathcomp.algebra.poly]
polyOver_nderivn [prf, in mathcomp.algebra.poly]
polyOver_nmod_closed [prf, in mathcomp.algebra.poly]
polyOver_poly [prf, in mathcomp.algebra.poly]
polyOver_subvs [prf, in mathcomp.field.fieldext]
polyOverC [prf, in mathcomp.algebra.poly]
polyOverNr [prf, in mathcomp.algebra.poly]
polyOverP [prf, in mathcomp.algebra.poly]
polyOverS [prf, in mathcomp.algebra.poly]
polyOverSv [prf, in mathcomp.field.fieldext]
polyOverX [prf, in mathcomp.algebra.poly]
polyOverXaddC [prf, in mathcomp.algebra.poly]
polyOverXn [prf, in mathcomp.algebra.poly]
polyOverXnaddC [prf, in mathcomp.algebra.poly]
polyOverXnsubC [prf, in mathcomp.algebra.poly]
polyOverXsubC [prf, in mathcomp.algebra.poly]
polyOverZ [prf, in mathcomp.algebra.poly]
polyP [prf, in mathcomp.algebra.poly]
polyseq0 [prf, in mathcomp.algebra.poly]
polyseq1 [prf, in mathcomp.algebra.poly]
polyseq_cons [prf, in mathcomp.algebra.poly]
polyseq_poly [prf, in mathcomp.algebra.poly]
polyseqC [prf, in mathcomp.algebra.poly]
polyseqK [prf, in mathcomp.algebra.poly]
polyseqMX [prf, in mathcomp.algebra.poly]
polyseqMXn [prf, in mathcomp.algebra.poly]
polyseqX [prf, in mathcomp.algebra.poly]
polyseqXaddC [prf, in mathcomp.algebra.poly]
polyseqXn [prf, in mathcomp.algebra.poly]
polyseqXsubC [prf, in mathcomp.algebra.poly]
polySpred [prf, in mathcomp.algebra.poly]
polyX_eq0 [prf, in mathcomp.algebra.poly]
polyX_key [prf, in mathcomp.algebra.poly]
polyXsubC_eq0 [prf, in mathcomp.algebra.poly]
porbit_actperm [prf, in mathcomp.finite_group.action]
porbit_id [prf, in mathcomp.finite_group.perm]
porbit_perm [prf, in mathcomp.finite_group.perm]
porbit_setP [prf, in mathcomp.finite_group.perm]
porbit_sym [prf, in mathcomp.finite_group.perm]
porbit_traject [prf, in mathcomp.finite_group.perm]
porbitE [prf, in mathcomp.finite_group.action]
porbitP [prf, in mathcomp.finite_group.perm]
porbitPmin [prf, in mathcomp.finite_group.perm]
porbits_mul_tperm [prf, in mathcomp.finite_group.perm]
porbitsV [prf, in mathcomp.finite_group.perm]
porbitV [prf, in mathcomp.finite_group.perm]
Pos.eqb_eq [prf, in mathcomp.boot.ssrAC]
Pos.nat_of_succ_bin [prf, in mathcomp.boot.ssrAC]
pos_nat1 [prf, in mathcomp.algebra.binnums]
pos_nat_compare [prf, in mathcomp.algebra.binnums]
pos_nat_compareP [prf, in mathcomp.algebra.binnums]
pos_nat_double [prf, in mathcomp.algebra.binnums]
pos_nat_doubleS [prf, in mathcomp.algebra.binnums]
pos_nat_eq [prf, in mathcomp.algebra.binnums]
pos_nat_exS [prf, in mathcomp.algebra.binnums]
pos_nat_ind [prf, in mathcomp.algebra.binnums]
pos_nat_le [prf, in mathcomp.algebra.binnums]
pos_nat_Pos_to_nat [prf, in mathcomp.algebra.binnums]
pos_nat_pred_double [prf, in mathcomp.algebra.binnums]
pos_natB [prf, in mathcomp.algebra.binnums]
pos_natD [prf, in mathcomp.algebra.binnums]
pos_natM [prf, in mathcomp.algebra.binnums]
pos_natP [prf, in mathcomp.algebra.binnums]
pos_natS [prf, in mathcomp.algebra.binnums]
Pos_sub_mask_Neg [prf, in mathcomp.algebra.binnums]
Pos_to_nat0F [prf, in mathcomp.algebra.binnums]
Pos_to_nat1 [prf, in mathcomp.algebra.binnums]
Pos_to_nat_double [prf, in mathcomp.algebra.binnums]
Pos_to_nat_doubleS [prf, in mathcomp.algebra.binnums]
Pos_to_nat_gt0 [prf, in mathcomp.algebra.binnums]
Pos_to_nat_pred_double [prf, in mathcomp.algebra.binnums]
Pos_to_natB [prf, in mathcomp.algebra.binnums]
Pos_to_natD [prf, in mathcomp.algebra.binnums]
Pos_to_natI [prf, in mathcomp.algebra.binnums]
Pos_to_natM [prf, in mathcomp.algebra.binnums]
Pos_to_natS [prf, in mathcomp.algebra.binnums]
posE [prf, in mathcomp.algebra.interval_inference]
posnP [prf, in mathcomp.boot.ssrnat]
posnum_subdef [prf, in mathcomp.algebra.interval_inference]
posnumP [prf, in mathcomp.algebra.interval_inference]
PoszD [prf, in mathcomp.algebra.ssrint]
PoszM [prf, in mathcomp.algebra.ssrint]
powerset0 [prf, in mathcomp.boot.finset]
powerset1 [prf, in mathcomp.boot.finset]
powersetCE [prf, in mathcomp.boot.finset]
powersetE [prf, in mathcomp.boot.finset]
powersetI [prf, in mathcomp.boot.finset]
powersetS [prf, in mathcomp.boot.finset]
powersetT [prf, in mathcomp.boot.finset]
powX_eq_mod [prf, in mathcomp.field.qfpoly]
pprimeChar_abelem [prf, in mathcomp.field.finfield]
pprimeChar_dimf [prf, in mathcomp.field.finfield]
pprimeChar_pgroup [prf, in mathcomp.field.finfield]
pprimeChar_scale1 [prf, in mathcomp.field.finfield]
pprimeChar_scaleA [prf, in mathcomp.field.finfield]
pprimeChar_scaleAl [prf, in mathcomp.field.finfield]
pprimeChar_scaleAr [prf, in mathcomp.field.finfield]
pprimeChar_scaleDl [prf, in mathcomp.field.finfield]
pprimeChar_scaleDr [prf, in mathcomp.field.finfield]
pprimeChar_vectAxiom [prf, in mathcomp.field.finfield]
pPrimePowerField [prf, in mathcomp.field.finfield]
pprod1g [prf, in mathcomp.finite_group.gproduct]
pprodE [prf, in mathcomp.finite_group.gproduct]
pprodEY [prf, in mathcomp.finite_group.gproduct]
pprodg1 [prf, in mathcomp.finite_group.gproduct]
pprodJ [prf, in mathcomp.finite_group.gproduct]
pprodmE [prf, in mathcomp.finite_group.gproduct]
pprodmEl [prf, in mathcomp.finite_group.gproduct]
pprodmEr [prf, in mathcomp.finite_group.gproduct]
pprodmM [prf, in mathcomp.finite_group.gproduct]
pprodP [prf, in mathcomp.finite_group.gproduct]
pprodW [prf, in mathcomp.finite_group.gproduct]
pprodWC [prf, in mathcomp.finite_group.gproduct]
pprodWY [prf, in mathcomp.finite_group.gproduct]
pquotient_pcore [prf, in mathcomp.solvable.pgroup]
pquotient_pgroup [prf, in mathcomp.solvable.pgroup]
pquotient_pHall [prf, in mathcomp.solvable.pgroup]
pre_image [prf, in mathcomp.boot.fintype]
PreClosedField.closed_nonrootP [prf, in mathcomp.algebra.poly]
PreClosedField.closed_rootP [prf, in mathcomp.algebra.poly]
pred0P [prf, in mathcomp.boot.fintype]
pred0Pn [prf, in mathcomp.boot.fintype]
pred1E [prf, in mathcomp.boot.eqtype]
pred2P [prf, in mathcomp.boot.eqtype]
predC_closed [prf, in mathcomp.boot.fingraph]
predC_itv [prf, in mathcomp.algebra.interval]
predC_itvl [prf, in mathcomp.algebra.interval]
predC_itvr [prf, in mathcomp.algebra.interval]
predD1P [prf, in mathcomp.boot.eqtype]
predn_doubleS [prf, in mathcomp.boot.ssrnat]
predn_exp [prf, in mathcomp.boot.binomial]
predn_int [prf, in mathcomp.algebra.ssrint]
predn_sub [prf, in mathcomp.boot.ssrnat]
prednK [prf, in mathcomp.boot.ssrnat]
predT_subset [prf, in mathcomp.boot.fintype]
predU1l [prf, in mathcomp.boot.eqtype]
predU1P [prf, in mathcomp.boot.eqtype]
predU1r [prf, in mathcomp.boot.eqtype]
predX_prod_enum [prf, in mathcomp.boot.fintype]
prefix0s [prf, in mathcomp.boot.seq]
prefix1s [prf, in mathcomp.boot.seq]
prefix_catl [prf, in mathcomp.boot.seq]
prefix_catr [prf, in mathcomp.boot.seq]
prefix_cons [prf, in mathcomp.boot.seq]
prefix_drop_gt0 [prf, in mathcomp.boot.seq]
prefix_index [prf, in mathcomp.boot.seq]
prefix_infix [prf, in mathcomp.boot.seq]
prefix_infix_trans [prf, in mathcomp.boot.seq]
prefix_path [prf, in mathcomp.boot.path]
prefix_prefix [prf, in mathcomp.boot.seq]
prefix_rcons [prf, in mathcomp.boot.seq]
prefix_refl [prf, in mathcomp.boot.seq]
prefix_rev [prf, in mathcomp.boot.seq]
prefix_revLR [prf, in mathcomp.boot.seq]
prefix_sorted [prf, in mathcomp.boot.path]
prefix_subseq [prf, in mathcomp.boot.seq]
prefix_suffix_trans [prf, in mathcomp.boot.seq]
prefix_take [prf, in mathcomp.boot.seq]
prefix_trans [prf, in mathcomp.boot.seq]
prefix_uniq [prf, in mathcomp.boot.seq]
prefixE [prf, in mathcomp.boot.seq]
prefixP [prf, in mathcomp.boot.seq]
prefixs0 [prf, in mathcomp.boot.seq]
prefixs1 [prf, in mathcomp.boot.seq]
prefixW [prf, in mathcomp.boot.seq]
preim_autE [prf, in mathcomp.finite_group.automorphism]
preim_iinv [prf, in mathcomp.boot.fintype]
preim_partition_pblock [prf, in mathcomp.boot.finset]
preim_partitionP [prf, in mathcomp.boot.finset]
preim_permV [prf, in mathcomp.finite_group.perm]
preimset0 [prf, in mathcomp.boot.finset]
preimset_proper [prf, in mathcomp.boot.finset]
preimsetC [prf, in mathcomp.boot.finset]
preimsetD [prf, in mathcomp.boot.finset]
preimsetI [prf, in mathcomp.boot.finset]
preimsetS [prf, in mathcomp.boot.finset]
preimsetT [prf, in mathcomp.boot.finset]
preimsetU [prf, in mathcomp.boot.finset]
prev_cycle [prf, in mathcomp.boot.path]
prev_map [prf, in mathcomp.boot.path]
prev_next [prf, in mathcomp.boot.path]
prev_nth [prf, in mathcomp.boot.path]
prev_rev [prf, in mathcomp.boot.path]
prev_rot [prf, in mathcomp.boot.path]
prev_rotr [prf, in mathcomp.boot.path]
prevE [prf, in mathcomp.boot.fingraph]
prim_expr_mod [prf, in mathcomp.algebra.poly]
prim_expr_order [prf, in mathcomp.algebra.poly]
prim_order_dvd [prf, in mathcomp.algebra.poly]
prim_order_exists [prf, in mathcomp.algebra.poly]
prim_order_gt0 [prf, in mathcomp.algebra.poly]
prim_root_dvd_eq0 [prf, in mathcomp.algebra.poly]
prim_root_eq0 [prf, in mathcomp.algebra.poly]
prim_root_exp_coprime [prf, in mathcomp.algebra.poly]
prim_root_natf_neq0 [prf, in mathcomp.algebra.poly]
prim_root_pcharF [prf, in mathcomp.algebra.poly]
prim_root_pi_eq0 [prf, in mathcomp.algebra.poly]
prim_rootP [prf, in mathcomp.algebra.poly]
prim_trans_norm [prf, in mathcomp.solvable.primitive_action]
prime_abelem [prf, in mathcomp.solvable.abelian]
prime_above [prf, in mathcomp.boot.prime]
prime_coprime [prf, in mathcomp.boot.prime]
prime_cyclic [prf, in mathcomp.solvable.cyclic]
prime_decomp_correct [prf, in mathcomp.boot.prime]
prime_decompE [prf, in mathcomp.boot.prime]
prime_dvd_bin [prf, in mathcomp.boot.binomial]
prime_FrobeniusP [prf, in mathcomp.solvable.frobenius]
prime_gt0 [prf, in mathcomp.boot.prime]
prime_gt1 [prf, in mathcomp.boot.prime]
prime_idealrM [prf, in mathcomp.algebra.ring_quotient]
prime_invariant_irr_extendible [prf, in mathcomp.group_representation.inertia]
prime_meetG [prf, in mathcomp.finite_group.fingroup]
prime_modn_expSn [prf, in mathcomp.boot.binomial]
prime_nt_dvdP [prf, in mathcomp.boot.prime]
prime_oddPn [prf, in mathcomp.boot.prime]
prime_Ohm1P [prf, in mathcomp.solvable.extremal]
prime_subgroupVti [prf, in mathcomp.solvable.pgroup]
prime_TIg [prf, in mathcomp.finite_group.fingroup]
PrimeDecompAux.edivn2P [prf, in mathcomp.boot.prime]
PrimeDecompAux.elogn2P [prf, in mathcomp.boot.prime]
PrimeDecompAux.ifnzP [prf, in mathcomp.boot.prime]
primeNsig [prf, in mathcomp.boot.prime]
primeP [prf, in mathcomp.boot.prime]
primePn [prf, in mathcomp.boot.prime]
primePns [prf, in mathcomp.boot.prime]
primes_class_simple_gt1 [prf, in mathcomp.group_representation.integral_char]
primes_eq0 [prf, in mathcomp.boot.prime]
primes_exponent [prf, in mathcomp.solvable.abelian]
primes_part [prf, in mathcomp.boot.prime]
primes_prime [prf, in mathcomp.boot.prime]
primes_uniq [prf, in mathcomp.boot.prime]
primesM [prf, in mathcomp.boot.prime]
primesX [prf, in mathcomp.boot.prime]
Primitive_Element_Theorem [prf, in mathcomp.field.separable]
primitive_mi [prf, in mathcomp.field.qfpoly]
primitive_poly_in_qpoly_eq0 [prf, in mathcomp.field.qfpoly]
primitive_polyP [prf, in mathcomp.field.qfpoly]
primitive_root_splitting_abelian [prf, in mathcomp.group_representation.mxrepresentation]
principal_comp_key [prf, in mathcomp.group_representation.mxrepresentation]
prod0v [prf, in mathcomp.field.falgebra]
prod1v [prf, in mathcomp.field.falgebra]
prod_card [prf, in mathcomp.algebra.tensor]
prod_cfunE [prf, in mathcomp.group_representation.classfun]
prod_constt [prf, in mathcomp.solvable.pgroup]
prod_Cyclotomic [prf, in mathcomp.field.cyclotomic]
prod_cyclotomic [prf, in mathcomp.field.cyclotomic]
prod_enumP [prf, in mathcomp.boot.fintype]
prod_fcat [prf, in mathcomp.algebra.tensor]
prod_map_poly [prf, in mathcomp.algebra.poly]
prod_mx_repr [prf, in mathcomp.group_representation.character]
prod_nat_const [prf, in mathcomp.boot.bigop]
prod_nat_const_nat [prf, in mathcomp.boot.bigop]
prod_nat_seq_eq0 [prf, in mathcomp.boot.bigop]
prod_nat_seq_eq1 [prf, in mathcomp.boot.bigop]
prod_nat_seq_neq0 [prf, in mathcomp.boot.bigop]
prod_nat_seq_neq1 [prf, in mathcomp.boot.bigop]
prod_nil [prf, in mathcomp.algebra.tensor]
prod_prime_decomp [prf, in mathcomp.boot.prime]
prod_repr_lin [prf, in mathcomp.group_representation.character]
prod_subG [prf, in mathcomp.finite_group.fingroup]
prod_t_correct [prf, in mathcomp.solvable.burnside_app]
prod_tpermP [prf, in mathcomp.finite_group.perm]
prodg_const [prf, in mathcomp.boot.monoid]
prodg_const_nat [prf, in mathcomp.boot.monoid]
prodg_ffun [prf, in mathcomp.finite_group.gproduct]
prodgM_commute [prf, in mathcomp.boot.monoid]
prodgMl_commute [prf, in mathcomp.boot.monoid]
prodgMr_commute [prf, in mathcomp.boot.monoid]
prodgV [prf, in mathcomp.boot.monoid]
prodgXr [prf, in mathcomp.boot.monoid]
prodMz [prf, in mathcomp.algebra.ssrint]
prodn_cond_gt0 [prf, in mathcomp.boot.bigop]
prodn_gt0 [prf, in mathcomp.boot.bigop]
prodsgP [prf, in mathcomp.finite_group.fingroup]
prodv0 [prf, in mathcomp.field.falgebra]
prodv1 [prf, in mathcomp.field.falgebra]
prodv_id [prf, in mathcomp.field.falgebra]
prodv_is_aspace [prf, in mathcomp.field.fieldext]
prodv_key [prf, in mathcomp.field.falgebra]
prodv_line [prf, in mathcomp.field.falgebra]
prodv_sub [prf, in mathcomp.field.falgebra]
prodvA [prf, in mathcomp.field.falgebra]
prodvAC [prf, in mathcomp.field.fieldext]
prodvC [prf, in mathcomp.field.fieldext]
prodvCA [prf, in mathcomp.field.fieldext]
prodvDl [prf, in mathcomp.field.falgebra]
prodvDr [prf, in mathcomp.field.falgebra]
prodvP [prf, in mathcomp.field.falgebra]
prodvS [prf, in mathcomp.field.falgebra]
prodvSl [prf, in mathcomp.field.falgebra]
prodvSr [prf, in mathcomp.field.falgebra]
proj_factmodS [prf, in mathcomp.group_representation.mxrepresentation]
proj_mx_0 [prf, in mathcomp.algebra.mxalgebra]
proj_mx_compl_sub [prf, in mathcomp.algebra.mxalgebra]
proj_mx_hom [prf, in mathcomp.group_representation.mxrepresentation]
proj_mx_id [prf, in mathcomp.algebra.mxalgebra]
proj_mx_proj [prf, in mathcomp.algebra.mxalgebra]
proj_mx_sub [prf, in mathcomp.algebra.mxalgebra]
proj_ortho_0 [prf, in mathcomp.algebra.spectral]
proj_ortho_compl_sub [prf, in mathcomp.algebra.spectral]
proj_ortho_id [prf, in mathcomp.algebra.spectral]
proj_ortho_proj [prf, in mathcomp.algebra.spectral]
proj_ortho_sub [prf, in mathcomp.algebra.spectral]
proj_orthoE [prf, in mathcomp.algebra.spectral]
projv_id [prf, in mathcomp.algebra.vector]
projv_proj [prf, in mathcomp.algebra.vector]
proper0 [prf, in mathcomp.boot.finset]
proper1G [prf, in mathcomp.finite_group.fingroup]
proper1set [prf, in mathcomp.boot.finset]
proper_card [prf, in mathcomp.boot.fintype]
proper_irrefl [prf, in mathcomp.boot.fintype]
proper_neq [prf, in mathcomp.boot.finset]
proper_sub [prf, in mathcomp.boot.fintype]
proper_sub_trans [prf, in mathcomp.boot.fintype]
proper_subn [prf, in mathcomp.boot.fintype]
proper_trans [prf, in mathcomp.boot.fintype]
properC [prf, in mathcomp.boot.finset]
properCl [prf, in mathcomp.boot.finset]
properCr [prf, in mathcomp.boot.finset]
properD [prf, in mathcomp.boot.finset]
properD1 [prf, in mathcomp.boot.finset]
properE [prf, in mathcomp.boot.fintype]
properEcard [prf, in mathcomp.boot.finset]
properEneq [prf, in mathcomp.boot.finset]
properG_ltn_log [prf, in mathcomp.solvable.pgroup]
properI [prf, in mathcomp.boot.finset]
properIl [prf, in mathcomp.boot.finset]
properIr [prf, in mathcomp.boot.finset]
properIset [prf, in mathcomp.boot.finset]
properJ [prf, in mathcomp.finite_group.fingroup]
properP [prf, in mathcomp.boot.fintype]
properT [prf, in mathcomp.boot.finset]
properU [prf, in mathcomp.boot.finset]
properUl [prf, in mathcomp.boot.finset]
properUr [prf, in mathcomp.boot.finset]
properxx [prf, in mathcomp.boot.fintype]
pseries1 [prf, in mathcomp.solvable.pgroup]
pseries_catl_id [prf, in mathcomp.solvable.pgroup]
pseries_catr_id [prf, in mathcomp.solvable.pgroup]
pseries_char [prf, in mathcomp.solvable.pgroup]
pseries_char_catl [prf, in mathcomp.solvable.pgroup]
pseries_char_catr [prf, in mathcomp.solvable.pgroup]
pseries_group_set [prf, in mathcomp.solvable.pgroup]
pseries_norm2 [prf, in mathcomp.solvable.pgroup]
pseries_normal [prf, in mathcomp.solvable.pgroup]
pseries_pop [prf, in mathcomp.solvable.pgroup]
pseries_pop2 [prf, in mathcomp.solvable.pgroup]
pseries_rcons [prf, in mathcomp.solvable.pgroup]
pseries_rcons_id [prf, in mathcomp.solvable.pgroup]
pseries_sub [prf, in mathcomp.solvable.pgroup]
pseries_sub_catl [prf, in mathcomp.solvable.pgroup]
pseries_sub_catr [prf, in mathcomp.solvable.pgroup]
pseries_subfun [prf, in mathcomp.solvable.pgroup]
pseriesJ [prf, in mathcomp.solvable.pgroup]
pseriesS [prf, in mathcomp.solvable.pgroup]
psubgroup1 [prf, in mathcomp.solvable.pgroup]
psubgroupJ [prf, in mathcomp.solvable.pgroup]
purely_inseparable_elementP_pchar [prf, in mathcomp.field.separable]
purely_inseparable_refl [prf, in mathcomp.field.separable]
purely_inseparable_trans [prf, in mathcomp.field.separable]
purely_inseparableP [prf, in mathcomp.field.separable]
pvalE [prf, in mathcomp.finite_group.perm]
pX1p2_extraspecial [prf, in mathcomp.solvable.extraspecial]
pX1p2_pgroup [prf, in mathcomp.solvable.extraspecial]
pX1p2id [prf, in mathcomp.solvable.extraspecial]
pX1p2n_extraspecial [prf, in mathcomp.solvable.extraspecial]
pX1p2n_pgroup [prf, in mathcomp.solvable.extraspecial]
pX1p2S [prf, in mathcomp.solvable.extraspecial]