Files

  • mathcomp

    • Top

    P (Global Index)

    Files ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Definitions ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Lemmas ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Abbreviations ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Global Index ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Notations

    P

    p [abbrev, in mathcomp.boot.fintype]
    P [abbrev, in mathcomp.boot.finset]
    p [abbrev, in mathcomp.algebra.zmodp]
    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_A [abbrev, in mathcomp.algebra.mxpoly]
    p_abelem_split1 [prf, in mathcomp.solvable.maximal]
    p_core_Fitting [prf, in mathcomp.solvable.maximal]
    p_elt [def, in mathcomp.solvable.pgroup]
    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_group [def, 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_rank [def, in mathcomp.solvable.abelian]
    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]
    PackSocle [constr, in mathcomp.group_representation.mxrepresentation]
    PackSocleK [prf, in mathcomp.group_representation.mxrepresentation]
    pair1g [def, in mathcomp.finite_group.gproduct]
    pair1g_morphism [def, in mathcomp.finite_group.gproduct]
    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_eq [def, in mathcomp.boot.eqtype]
    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 [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
    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_interval [def, in mathcomp.algebra.interval]
    pair_of_mxvec_index [def, in mathcomp.algebra.matrix]
    pair_of_sd [def, in mathcomp.finite_group.gproduct]
    pair_of_section [def, in mathcomp.solvable.jordanholder]
    pair_of_tag [def, in mathcomp.boot.choice]
    pair_of_tagK [prf, in mathcomp.boot.choice]
    pair_one_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    pair_opp [def, in mathcomp.boot.nmodule]
    pair_ortho_rec [def, in mathcomp.group_representation.classfun]
    pair_ortho_rec [def, in mathcomp.algebra.sesquilinear]
    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_unitr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
    pair_vect_iso [prf, in mathcomp.algebra.vector]
    pair_zero [def, in mathcomp.boot.nmodule]
    pairg1 [def, in mathcomp.finite_group.gproduct]
    pairg1_morphism [def, in mathcomp.finite_group.gproduct]
    pairg1_morphM [prf, in mathcomp.finite_group.gproduct]
    pairmap [def, in mathcomp.boot.seq]
    pairmap_bseq [def, in mathcomp.boot.tuple]
    pairmap_bseqP [prf, in mathcomp.boot.tuple]
    pairmap_cat [prf, in mathcomp.boot.seq]
    pairmap_tuple [def, in mathcomp.boot.tuple]
    pairmap_tupleP [prf, in mathcomp.boot.tuple]
    pairmapK [prf, in mathcomp.boot.seq]
    pairMnE [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    pairwise [def, in mathcomp.boot.seq]
    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 [def, in mathcomp.group_representation.classfun]
    pairwise_orthogonal [def, in mathcomp.algebra.sesquilinear]
    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]
    parse [def, in mathcomp.algebra.rat]
    parse [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    parse_int [def, in mathcomp.algebra.ssrint]
    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]
    partial_product [def, in mathcomp.finite_group.gproduct]
    partition [def, in mathcomp.boot.finset]
    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]
    partn [def, in mathcomp.boot.prime]
    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]
    Pascal [def, in mathcomp.boot.binomial]
    passmx [mod, in mathcomp.algebra.vector]
    passmx.coord_rVof [prf, in mathcomp.algebra.vector]
    passmx.coord_vecof [prf, in mathcomp.algebra.vector]
    passmx.funmx [def, in mathcomp.algebra.vector]
    passmx.funmx_linear [prf, in mathcomp.algebra.vector]
    passmx.hom_vecof [prf, in mathcomp.algebra.vector]
    passmx.hommx [def, 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.leigenspace [def, in mathcomp.algebra.vector]
    passmx.leigenspaceE [prf, in mathcomp.algebra.vector]
    passmx.leigenvalue [def, in mathcomp.algebra.vector]
    passmx.limgE [prf, in mathcomp.algebra.vector]
    passmx.lker_ker [prf, in mathcomp.algebra.vector]
    passmx.m [abbrev, in mathcomp.algebra.vector]
    passmx.m [abbrev, in mathcomp.algebra.vector]
    passmx.m [abbrev, in mathcomp.algebra.vector]
    passmx.mem_vecof [prf, in mathcomp.algebra.vector]
    passmx.msof [def, 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.mxof [def, 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.n [abbrev, in mathcomp.algebra.vector]
    passmx.n [abbrev, in mathcomp.algebra.vector]
    passmx.n [abbrev, in mathcomp.algebra.vector]
    passmx.n [abbrev, in mathcomp.algebra.vector]
    passmx.p [abbrev, in mathcomp.algebra.vector]
    passmx.rVof [def, 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 [def, 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.vsof [def, 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 [file, in mathcomp.boot.path]
    path [abbrev, in mathcomp.boot.path]
    path [abbrev, in mathcomp.boot.path]
    path [def, in mathcomp.boot.path]
    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 [def, in mathcomp.boot.finset]
    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]
    pcan_type [def, in mathcomp.boot.eqtype]
    PCanHasChoice [prf, in mathcomp.boot.choice]
    PCanIsCountable [def, in mathcomp.boot.choice]
    PCanIsFinite [def, in mathcomp.boot.fintype]
    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 [def, in mathcomp.solvable.pgroup]
    pcore_char [prf, in mathcomp.solvable.pgroup]
    pcore_faithful_irr_act [prf, in mathcomp.solvable.sylow]
    pcore_faithful_mx_irr [abbrev, in mathcomp.group_representation.mxabelem]
    pcore_faithful_mx_irr_pchar [prf, in mathcomp.group_representation.mxabelem]
    pcore_Fitting [prf, in mathcomp.solvable.maximal]
    pcore_gFun [def, in mathcomp.solvable.pgroup]
    pcore_group [def, in mathcomp.solvable.pgroup]
    pcore_igFun [def, in mathcomp.solvable.pgroup]
    pcore_max [prf, in mathcomp.solvable.pgroup]
    pcore_mod [def, in mathcomp.solvable.pgroup]
    pcore_mod1 [prf, in mathcomp.solvable.pgroup]
    pcore_mod_group [def, 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_pgFun [def, 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 [abbrev, in mathcomp.group_representation.mxabelem]
    pcore_sub_rker_mx_irr_pchar [prf, in mathcomp.group_representation.mxabelem]
    pcore_sub_rstab_mxsimple [abbrev, 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 [mod, in mathcomp.algebra.poly]
    Pdeg2.Field [mod, in mathcomp.algebra.poly]
    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 [mod, 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 [def, in mathcomp.boot.prime]
    Pdiv [mod, in mathcomp.algebra.polydiv]
    Pdiv.ClosedField [mod, in mathcomp.algebra.polydiv]
    Pdiv.ClosedField.coprimepP [prf, in mathcomp.algebra.polydiv]
    Pdiv.ClosedField.root_coprimep [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain [mod, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.apply_irredp [def, 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.coprimep [def, 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.egcdp [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.egcdp0 [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.egcdp_rec [def, 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.gcdp [def, 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.gdcop [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.gdcop0 [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.gdcop_rec [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.gdcop_recP [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.gdcop_spec [ind, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.gdcopP [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonIdomain.GdcopSpec [constr, 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.irreducible_poly [def, 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 [mod, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.ComEdivnSpec [constr, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.comm_redivp_spec [ind, 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.rcoprimep [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rdiv0p [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rdivp [def, 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.rdvdp [def, 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, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.redivp_def [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.redivp_expanded_def [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.redivp_key [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.redivp_rec [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.redivp_unlockable [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rgcd0p [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rgcdp [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rgcdp0 [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rgcdpE [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rgdcop [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rgdcop0 [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rgdcop_rec [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rmod0p [prf, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rmodp [def, 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 [def, in mathcomp.algebra.polydiv]
    Pdiv.CommonRing.rscalp_small [prf, in mathcomp.algebra.polydiv]
    Pdiv.ComRing [mod, in mathcomp.algebra.polydiv]
    Pdiv.ComRing.EdivnSpec [constr, 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.redivp_spec [ind, in mathcomp.algebra.polydiv]
    Pdiv.ComRing.redivpP [prf, in mathcomp.algebra.polydiv]
    Pdiv.Field [mod, 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.edivp_spec [ind, in mathcomp.algebra.polydiv]
    Pdiv.Field.edivpP [prf, in mathcomp.algebra.polydiv]
    Pdiv.Field.EdivpSpec [constr, 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.leq_trunc_divp [abbrev, 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 [def, 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.Idomain [mod, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs [mod, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.divp [def, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.dvdp [def, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.edivp [def, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.edivp_expanded_def [def, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.edivp_key [prf, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.edivp_unlockable [def, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.eqp [def, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.modp [def, in mathcomp.algebra.polydiv]
    Pdiv.IdomainDefs.scalp [def, in mathcomp.algebra.polydiv]
    Pdiv.IdomainMonic [mod, 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 [mod, 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.leq_trunc_divp [abbrev, 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 [mod, 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 [mod, 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 [constr, in mathcomp.algebra.polydiv]
    Pdiv.RingComRreg.rdvdp_eqP [prf, in mathcomp.algebra.polydiv]
    Pdiv.RingComRreg.rdvdp_mull [prf, in mathcomp.algebra.polydiv]
    Pdiv.RingComRreg.rdvdp_spec [ind, in mathcomp.algebra.polydiv]
    Pdiv.RingComRreg.RdvdpN [constr, 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 [mod, 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 [mod, in mathcomp.algebra.polydiv]
    Pdiv.UnitRing.uniq_roots_rdvdp [prf, in mathcomp.algebra.polydiv]
    Pdiv.WeakIdomain [mod, 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.edivp_spec [ind, in mathcomp.algebra.polydiv]
    Pdiv.WeakIdomain.edivpP [prf, in mathcomp.algebra.polydiv]
    Pdiv.WeakIdomain.Fedivp_spec [constr, 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.Redivp_spec [constr, 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]
    pElem [def, in mathcomp.solvable.abelian]
    pElemI [prf, in mathcomp.solvable.abelian]
    pElemJ [prf, in mathcomp.solvable.abelian]
    pElemP [prf, in mathcomp.solvable.abelian]
    pElemS [prf, in mathcomp.solvable.abelian]
    perm [file, in mathcomp.finite_group.perm]
    perm [abbrev, in mathcomp.finite_group.perm]
    perm [mod, in mathcomp.finite_group.perm]
    Perm [constr, in mathcomp.finite_group.perm]
    perm.body [def, in mathcomp.finite_group.perm]
    perm.unlock [def, in mathcomp.finite_group.perm]
    perm1 [prf, in mathcomp.finite_group.perm]
    perm_act1P [prf, in mathcomp.finite_group.action]
    perm_action [def, 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_eq [def, in mathcomp.boot.seq]
    perm_eql [abbrev, in mathcomp.boot.seq]
    perm_eql [abbrev, in mathcomp.boot.seq]
    perm_eqr [abbrev, in mathcomp.boot.seq]
    perm_eqr [abbrev, 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 [def, in mathcomp.finite_group.automorphism]
    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_inv [def, 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_Locked [modtype, in mathcomp.finite_group.perm]
    perm_Locked.body [ax, in mathcomp.finite_group.perm]
    perm_Locked.unlock [ax, in mathcomp.finite_group.perm]
    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_mul [def, in mathcomp.finite_group.perm]
    perm_mulP [prf, in mathcomp.finite_group.perm]
    perm_mx [def, in mathcomp.algebra.matrix]
    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_of [def, in mathcomp.finite_group.perm]
    perm_on [def, in mathcomp.finite_group.perm]
    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_one [def, 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_tseq [abbrev, in mathcomp.boot.seq]
    perm_type [ind, in mathcomp.finite_group.perm]
    perm_type_ind [scheme, in mathcomp.finite_group.perm]
    perm_type_rec [scheme, in mathcomp.finite_group.perm]
    perm_type_rect [scheme, in mathcomp.finite_group.perm]
    perm_type_sind [scheme, in mathcomp.finite_group.perm]
    perm_undup [prf, in mathcomp.boot.seq]
    perm_uniq [prf, in mathcomp.boot.seq]
    perm_unlock [def, in mathcomp.finite_group.perm]
    perm_unlock_subterm [def, in mathcomp.finite_group.perm]
    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]
    perms [abbrev, 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]
    perms_rec [def, in mathcomp.boot.seq]
    permutations [def, in mathcomp.boot.seq]
    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 [mod, in mathcomp.solvable.extraspecial]
    Pextraspecial.act [def, in mathcomp.solvable.extraspecial]
    Pextraspecial.action [def, in mathcomp.solvable.extraspecial]
    Pextraspecial.actP [prf, in mathcomp.solvable.extraspecial]
    Pextraspecial.gactP [prf, in mathcomp.solvable.extraspecial]
    Pextraspecial.groupAction [def, in mathcomp.solvable.extraspecial]
    Pextraspecial.gtype [def, in mathcomp.solvable.extraspecial]
    Pextraspecial.gtype_key [prf, in mathcomp.solvable.extraspecial]
    Pextraspecial.ngtype [def, in mathcomp.solvable.extraspecial]
    Pextraspecial.ngtypeQ [def, in mathcomp.solvable.extraspecial]
    pfactor [def, in mathcomp.boot.prime]
    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]
    pfamily [abbrev, in mathcomp.boot.finfun]
    pfamily_mem [def, in mathcomp.boot.finfun]
    pfamilyP [prf, in mathcomp.boot.finfun]
    pffun_on [abbrev, in mathcomp.boot.finfun]
    pffun_on_mem [def, in mathcomp.boot.finfun]
    pffun_onP [prf, in mathcomp.boot.finfun]
    pFrobenius_aut [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    pFrobenius_aut_int [prf, in mathcomp.algebra.ssrint]
    pFrobenius_autMz [prf, in mathcomp.algebra.ssrint]
    pFtoE [abbrev, in mathcomp.algebra.polyXY]
    pgroup [file, in mathcomp.solvable.pgroup]
    pgroup [def, in mathcomp.solvable.pgroup]
    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 [def, 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 [abbrev, in mathcomp.boot.generic_quotient]
    pi [mod, in mathcomp.boot.generic_quotient]
    pi'_p'group [prf, in mathcomp.solvable.pgroup]
    pi'_p'nat [prf, in mathcomp.boot.prime]
    pi.body [def, in mathcomp.boot.generic_quotient]
    pi.unlock [def, in mathcomp.boot.generic_quotient]
    pi_add_quot_morph [def, in mathcomp.algebra.ring_quotient]
    pi_addr [def, in mathcomp.algebra.ring_quotient]
    pi_arg [def, in mathcomp.boot.prime]
    pi_arg_of_fin_pred [def, in mathcomp.boot.prime]
    pi_arg_of_nat [def, in mathcomp.boot.prime]
    pi_center_nilpotent [prf, in mathcomp.solvable.sylow]
    pi_eq_quot [def, in mathcomp.boot.generic_quotient]
    pi_eq_quot_mono [def, in mathcomp.boot.generic_quotient]
    pi_inv_quot_morph [def, in mathcomp.algebra.ring_quotient]
    pi_invr [def, in mathcomp.algebra.ring_quotient]
    pi_is_additive [def, in mathcomp.algebra.ring_quotient]
    pi_is_monoid_morphism [prf, in mathcomp.algebra.ring_quotient]
    pi_is_multiplicative [def, in mathcomp.algebra.ring_quotient]
    pi_is_zmod_morphism [prf, in mathcomp.algebra.ring_quotient]
    pi_Locked [modtype, in mathcomp.boot.generic_quotient]
    pi_Locked.body [ax, in mathcomp.boot.generic_quotient]
    pi_Locked.unlock [ax, in mathcomp.boot.generic_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_mul_quot_morph [def, in mathcomp.algebra.ring_quotient]
    pi_mulr [def, in mathcomp.algebra.ring_quotient]
    pi_of [def, in mathcomp.boot.prime]
    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_one_quot_morph [def, in mathcomp.algebra.ring_quotient]
    pi_oner [def, in mathcomp.algebra.ring_quotient]
    pi_opp_quot_morph [def, in mathcomp.algebra.ring_quotient]
    pi_oppr [def, in mathcomp.algebra.ring_quotient]
    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_spec [ind, in mathcomp.boot.generic_quotient]
    pi_subdef [def, in mathcomp.boot.generic_quotient]
    pi_subfext_add [prf, in mathcomp.field.fieldext]
    pi_subfext_inv [prf, in mathcomp.field.fieldext]
    pi_subfext_inv_morph [def, in mathcomp.field.fieldext]
    pi_subfext_mul [prf, in mathcomp.field.fieldext]
    pi_subfext_mul_morph [def, in mathcomp.field.fieldext]
    pi_subfext_opp [prf, in mathcomp.field.fieldext]
    pi_subfext_opp_morph [def, in mathcomp.field.fieldext]
    pi_subfx_add_morph [def, in mathcomp.field.fieldext]
    pi_subfx_inj [prf, in mathcomp.field.fieldext]
    pi_subfx_inj_morph [def, in mathcomp.field.fieldext]
    pi_unit_quot_morph [def, in mathcomp.algebra.ring_quotient]
    pi_unitr [def, in mathcomp.algebra.ring_quotient]
    pi_unlock [def, in mathcomp.boot.generic_quotient]
    pi_unlock_subterm [def, in mathcomp.boot.generic_quotient]
    pi_zero_quot_morph [def, in mathcomp.algebra.ring_quotient]
    pi_zeror [def, in mathcomp.algebra.ring_quotient]
    Pick [constr, in mathcomp.boot.fintype]
    pick [def, in mathcomp.boot.fintype]
    pick_set1 [prf, in mathcomp.boot.finset]
    pick_spec [ind, in mathcomp.boot.fintype]
    pick_true [def, in mathcomp.boot.fintype]
    pickle [def, in mathcomp.boot.choice]
    pickle_inv [def, in mathcomp.boot.choice]
    pickle_invK [prf, in mathcomp.boot.choice]
    pickle_seq [def, in mathcomp.boot.choice]
    pickle_seqK [prf, in mathcomp.boot.choice]
    pickle_tagged [def, in mathcomp.boot.choice]
    pickle_taggedK [prf, in mathcomp.boot.choice]
    pickleK [def, in mathcomp.boot.choice]
    pickleK_inv [prf, in mathcomp.boot.choice]
    pickP [prf, in mathcomp.boot.fintype]
    PiConst [abbrev, in mathcomp.boot.generic_quotient]
    pid_mx [def, in mathcomp.algebra.matrix]
    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]
    piE [abbrev, in mathcomp.boot.generic_quotient]
    PiEmbed [abbrev, in mathcomp.boot.generic_quotient]
    PiMono1 [abbrev, in mathcomp.boot.generic_quotient]
    PiMono2 [abbrev, in mathcomp.boot.generic_quotient]
    PiMorph [abbrev, in mathcomp.boot.generic_quotient]
    PiMorph1 [abbrev, in mathcomp.boot.generic_quotient]
    PiMorph11 [abbrev, in mathcomp.boot.generic_quotient]
    PiMorph2 [abbrev, in mathcomp.boot.generic_quotient]
    pinvmx [def, in mathcomp.algebra.mxalgebra]
    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]
    PiSpec [constr, in mathcomp.boot.generic_quotient]
    plogp [def, in mathcomp.field.qfpoly]
    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 [def, in mathcomp.boot.seq]
    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 [def, in mathcomp.solvable.abelian]
    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 [def, in mathcomp.boot.prime]
    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]
    pnElem [def, in mathcomp.solvable.abelian]
    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]
    poly [file, in mathcomp.algebra.poly]
    poly [def, in mathcomp.algebra.poly]
    Poly [def, in mathcomp.algebra.poly]
    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_expanded_def [def, 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 [def, 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_nil [def, 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 [def, in mathcomp.algebra.qpoly]
    poly_of_size_mod [prf, in mathcomp.algebra.qpoly]
    poly_of_size_pred [def, in mathcomp.algebra.qpoly]
    poly_rV [def, in mathcomp.algebra.mxpoly]
    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_unit [def, in mathcomp.algebra.poly]
    poly_unitE [prf, in mathcomp.algebra.poly]
    poly_unlockable [def, in mathcomp.algebra.poly]
    poly_XaY [def, in mathcomp.algebra.polyXY]
    poly_XaY0 [prf, in mathcomp.algebra.polyXY]
    poly_XaY_eq0 [prf, in mathcomp.algebra.polyXY]
    poly_XmY [def, in mathcomp.algebra.polyXY]
    poly_XmY0 [prf, in mathcomp.algebra.polyXY]
    poly_XmY_eq0 [prf, in mathcomp.algebra.polyXY]
    polyC [def, in mathcomp.algebra.poly]
    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_multiplicative [def, 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]
    polydiv [file, in mathcomp.algebra.polydiv]
    PolyK [prf, in mathcomp.algebra.poly]
    polyn [proj, in mathcomp.algebra.qpoly]
    polyn_is_semilinear [prf, in mathcomp.algebra.qpoly]
    polynomial [rec, in mathcomp.algebra.poly]
    polyOver [def, in mathcomp.algebra.poly]
    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_pred [def, 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]
    polyseq [proj, 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 [def, in mathcomp.algebra.poly]
    polyX_def [def, in mathcomp.algebra.poly]
    polyX_eq0 [prf, in mathcomp.algebra.poly]
    polyX_key [prf, in mathcomp.algebra.poly]
    polyX_unlockable [def, in mathcomp.algebra.poly]
    polyXsubC_eq0 [prf, in mathcomp.algebra.poly]
    polyXY [file, in mathcomp.algebra.polyXY]
    pop_succn [def, in mathcomp.boot.ssrnat]
    porbit [abbrev, in mathcomp.finite_group.perm]
    porbit [mod, in mathcomp.finite_group.perm]
    porbit.body [def, in mathcomp.finite_group.perm]
    porbit.unlock [def, in mathcomp.finite_group.perm]
    porbit_actperm [prf, in mathcomp.finite_group.action]
    porbit_id [prf, in mathcomp.finite_group.perm]
    porbit_Locked [modtype, in mathcomp.finite_group.perm]
    porbit_Locked.body [ax, in mathcomp.finite_group.perm]
    porbit_Locked.unlock [ax, 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]
    porbit_unlock_subterm [def, in mathcomp.finite_group.perm]
    porbit_unlockable [def, 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 [def, 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 [mod, in mathcomp.boot.ssrAC]
    Pos.eqb_eq [prf, in mathcomp.boot.ssrAC]
    Pos.nat_of_succ_bin [prf, in mathcomp.boot.ssrAC]
    Pos.Nsucc [def, in mathcomp.boot.ssrAC]
    Pos.of_hex_int [def, in mathcomp.boot.ssrAC]
    Pos.of_hex_uint [def, in mathcomp.boot.ssrAC]
    Pos.of_hex_uint_acc [def, in mathcomp.boot.ssrAC]
    Pos.of_int [def, in mathcomp.boot.ssrAC]
    Pos.of_num_int [def, in mathcomp.boot.ssrAC]
    Pos.of_uint [def, in mathcomp.boot.ssrAC]
    Pos.of_uint_acc [def, in mathcomp.boot.ssrAC]
    Pos.sixteen [abbrev, in mathcomp.boot.ssrAC]
    Pos.ten [abbrev, in mathcomp.boot.ssrAC]
    Pos.to_little_uint [def, in mathcomp.boot.ssrAC]
    Pos.to_num_uint [def, in mathcomp.boot.ssrAC]
    Pos.to_uint [def, in mathcomp.boot.ssrAC]
    pos_nat [def, in mathcomp.algebra.binnums]
    pos_nat1 [prf, in mathcomp.algebra.binnums]
    pos_nat_compare [prf, in mathcomp.algebra.binnums]
    pos_nat_compare_spec [ind, in mathcomp.algebra.binnums]
    Pos_nat_compare_spec_Eq [constr, in mathcomp.algebra.binnums]
    Pos_nat_compare_spec_Gt [constr, in mathcomp.algebra.binnums]
    Pos_nat_compare_spec_Lt [constr, 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_nat_spec [ind, in mathcomp.algebra.binnums]
    Pos_nat_spec_false [constr, in mathcomp.algebra.binnums]
    Pos_nat_spec_xH [constr, in mathcomp.algebra.binnums]
    Pos_nat_spec_xI [constr, in mathcomp.algebra.binnums]
    Pos_nat_spec_xO [constr, in mathcomp.algebra.binnums]
    pos_natB [prf, in mathcomp.algebra.binnums]
    pos_natD [prf, in mathcomp.algebra.binnums]
    pos_natE [def, 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_of_nat [def, in mathcomp.boot.ssrnat]
    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_natE [def, 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]
    PosNotEq0 [constr, in mathcomp.boot.ssrnat]
    posnP [prf, in mathcomp.boot.ssrnat]
    PosNum [def, in mathcomp.algebra.interval_inference]
    posnum_spec [ind, in mathcomp.algebra.interval_inference]
    posnum_subdef [prf, in mathcomp.algebra.interval_inference]
    posnumP [prf, in mathcomp.algebra.interval_inference]
    Posz [constr, in mathcomp.algebra.ssrint]
    PoszD [prf, in mathcomp.algebra.ssrint]
    PoszM [prf, in mathcomp.algebra.ssrint]
    powers_mx [def, in mathcomp.algebra.mxpoly]
    powerset [def, in mathcomp.boot.finset]
    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_scale [def, 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]
    pPrimeCharType [def, in mathcomp.field.finfield]
    pPrimePowerField [prf, in mathcomp.field.finfield]
    pprod [abbrev, in mathcomp.finite_group.gproduct]
    pprod [abbrev, in mathcomp.finite_group.gproduct]
    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]
    pprodm [def, in mathcomp.finite_group.gproduct]
    pprodm_morphism [def, 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]
    pQtoC [abbrev, in mathcomp.field.cyclotomic]
    pQtoC [abbrev, in mathcomp.field.algnum]
    pQtoC [abbrev, in mathcomp.field.algC]
    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 [mod, in mathcomp.algebra.poly]
    PreClosedField.closed_nonrootP [prf, in mathcomp.algebra.poly]
    PreClosedField.closed_rootP [prf, in mathcomp.algebra.poly]
    pred0b [def, in mathcomp.boot.fintype]
    pred0P [prf, in mathcomp.boot.fintype]
    pred0Pn [prf, in mathcomp.boot.fintype]
    pred1 [def, in mathcomp.boot.eqtype]
    pred1E [prf, in mathcomp.boot.eqtype]
    pred2 [def, in mathcomp.boot.eqtype]
    pred2P [prf, in mathcomp.boot.eqtype]
    pred3 [def, in mathcomp.boot.eqtype]
    pred4 [def, in mathcomp.boot.eqtype]
    pred_Nirr [def, in mathcomp.group_representation.character]
    pred_of_itv [def, in mathcomp.algebra.interval]
    pred_of_seq [def, in mathcomp.boot.seq]
    pred_of_set [abbrev, in mathcomp.boot.finset]
    pred_of_set [mod, in mathcomp.boot.finset]
    pred_of_set.body [def, in mathcomp.boot.finset]
    pred_of_set.unlock [def, in mathcomp.boot.finset]
    pred_of_set_Locked [modtype, in mathcomp.boot.finset]
    pred_of_set_Locked.body [ax, in mathcomp.boot.finset]
    pred_of_set_Locked.unlock [ax, in mathcomp.boot.finset]
    pred_of_set_unlock [def, in mathcomp.boot.finset]
    pred_of_set_unlock_subterm [def, in mathcomp.boot.finset]
    pred_of_vspace [def, in mathcomp.algebra.vector]
    predC1 [def, 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]
    predD1 [def, in mathcomp.boot.eqtype]
    predD1P [prf, in mathcomp.boot.eqtype]
    predn [abbrev, in mathcomp.boot.ssrnat]
    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]
    predOfType [abbrev, in mathcomp.boot.finset]
    predT_subset [prf, in mathcomp.boot.fintype]
    predU1 [def, in mathcomp.boot.eqtype]
    predU1l [prf, in mathcomp.boot.eqtype]
    predU1P [prf, in mathcomp.boot.eqtype]
    predU1r [prf, in mathcomp.boot.eqtype]
    predX [def, in mathcomp.boot.eqtype]
    predX_prod_enum [prf, in mathcomp.boot.fintype]
    prefix [def, in mathcomp.boot.seq]
    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 [def, in mathcomp.boot.finset]
    preim_partition_pblock [prf, in mathcomp.boot.finset]
    preim_partitionP [prf, in mathcomp.boot.finset]
    preim_permV [prf, in mathcomp.finite_group.perm]
    preim_seq [def, in mathcomp.boot.fintype]
    preimset [def, in mathcomp.boot.finset]
    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]
    preorder [file, in mathcomp.order.preorder]
    presentation [file, in mathcomp.finite_group.presentation]
    Presentation [mod, in mathcomp.finite_group.presentation]
    Presentation.And [constr, in mathcomp.finite_group.presentation]
    Presentation.and_rel [def, in mathcomp.finite_group.presentation]
    Presentation.bool_of_rel [def, in mathcomp.finite_group.presentation]
    Presentation.Cast [def, in mathcomp.finite_group.presentation]
    Presentation.Comm [constr, in mathcomp.finite_group.presentation]
    Presentation.Conj [constr, in mathcomp.finite_group.presentation]
    Presentation.Cst [constr, in mathcomp.finite_group.presentation]
    Presentation.Env [constr, in mathcomp.finite_group.presentation]
    Presentation.env [ind, in mathcomp.finite_group.presentation]
    Presentation.env1 [def, in mathcomp.finite_group.presentation]
    Presentation.env_ind [scheme, in mathcomp.finite_group.presentation]
    Presentation.env_rec [scheme, in mathcomp.finite_group.presentation]
    Presentation.env_rect [scheme, in mathcomp.finite_group.presentation]
    Presentation.env_sind [scheme, in mathcomp.finite_group.presentation]
    Presentation.Eq1 [def, in mathcomp.finite_group.presentation]
    Presentation.Eq2 [constr, in mathcomp.finite_group.presentation]
    Presentation.Eq3 [def, in mathcomp.finite_group.presentation]
    Presentation.eval [def, in mathcomp.finite_group.presentation]
    Presentation.Exp [constr, in mathcomp.finite_group.presentation]
    Presentation.Formula [constr, in mathcomp.finite_group.presentation]
    Presentation.formula [ind, in mathcomp.finite_group.presentation]
    Presentation.formula_ind [scheme, in mathcomp.finite_group.presentation]
    Presentation.formula_rec [scheme, in mathcomp.finite_group.presentation]
    Presentation.formula_rect [scheme, in mathcomp.finite_group.presentation]
    Presentation.formula_sind [scheme, in mathcomp.finite_group.presentation]
    Presentation.Generator [constr, in mathcomp.finite_group.presentation]
    Presentation.hom [def, in mathcomp.finite_group.presentation]
    Presentation.Idx [constr, in mathcomp.finite_group.presentation]
    Presentation.Inv [constr, in mathcomp.finite_group.presentation]
    Presentation.iso [def, in mathcomp.finite_group.presentation]
    Presentation.Mul [constr, in mathcomp.finite_group.presentation]
    Presentation.NoRel [constr, in mathcomp.finite_group.presentation]
    Presentation.rel [def, in mathcomp.finite_group.presentation]
    Presentation.Rel [constr, in mathcomp.finite_group.presentation]
    Presentation.rel_type [ind, in mathcomp.finite_group.presentation]
    Presentation.rel_type_ind [scheme, in mathcomp.finite_group.presentation]
    Presentation.rel_type_rec [scheme, in mathcomp.finite_group.presentation]
    Presentation.rel_type_rect [scheme, in mathcomp.finite_group.presentation]
    Presentation.rel_type_sind [scheme, in mathcomp.finite_group.presentation]
    Presentation.sat [def, in mathcomp.finite_group.presentation]
    Presentation.term [ind, in mathcomp.finite_group.presentation]
    Presentation.term_ind [scheme, in mathcomp.finite_group.presentation]
    Presentation.term_rec [scheme, in mathcomp.finite_group.presentation]
    Presentation.term_rect [scheme, in mathcomp.finite_group.presentation]
    Presentation.term_sind [scheme, in mathcomp.finite_group.presentation]
    Presentation.type [ind, in mathcomp.finite_group.presentation]
    Presentation.type_ind [scheme, in mathcomp.finite_group.presentation]
    Presentation.type_rec [scheme, in mathcomp.finite_group.presentation]
    Presentation.type_rect [scheme, in mathcomp.finite_group.presentation]
    Presentation.type_sind [scheme, in mathcomp.finite_group.presentation]
    prev [def, in mathcomp.boot.path]
    prev_at [def, in mathcomp.boot.path]
    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_charF [abbrev, 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 [file, in mathcomp.boot.prime]
    prime [def, in mathcomp.boot.prime]
    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 [def, in mathcomp.boot.prime]
    prime_decomp_correct [prf, in mathcomp.boot.prime]
    prime_decomp_rec [def, 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_idealr_closed [def, in mathcomp.algebra.ring_quotient]
    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]
    primeChar_abelem [abbrev, in mathcomp.field.finfield]
    primeChar_dimf [abbrev, in mathcomp.field.finfield]
    primeChar_pgroup [abbrev, in mathcomp.field.finfield]
    primeChar_scale [abbrev, in mathcomp.field.finfield]
    primeChar_scale1 [abbrev, in mathcomp.field.finfield]
    primeChar_scaleA [abbrev, in mathcomp.field.finfield]
    primeChar_scaleAl [abbrev, in mathcomp.field.finfield]
    primeChar_scaleAr [abbrev, in mathcomp.field.finfield]
    primeChar_scaleDl [abbrev, in mathcomp.field.finfield]
    primeChar_scaleDr [abbrev, in mathcomp.field.finfield]
    primeChar_vectAxiom [abbrev, in mathcomp.field.finfield]
    PrimeCharType [abbrev, in mathcomp.field.finfield]
    PrimeDecompAux [mod, in mathcomp.boot.prime]
    PrimeDecompAux.add_divisors [def, in mathcomp.boot.prime]
    PrimeDecompAux.add_totient_factor [def, in mathcomp.boot.prime]
    PrimeDecompAux.cons_pfactor [def, in mathcomp.boot.prime]
    PrimeDecompAux.edivn2 [def, in mathcomp.boot.prime]
    PrimeDecompAux.edivn2P [prf, in mathcomp.boot.prime]
    PrimeDecompAux.elogn2 [def, in mathcomp.boot.prime]
    PrimeDecompAux.elogn2_spec [ind, in mathcomp.boot.prime]
    PrimeDecompAux.elogn2P [prf, in mathcomp.boot.prime]
    PrimeDecompAux.Elogn2Spec [constr, in mathcomp.boot.prime]
    PrimeDecompAux.ifnz [def, in mathcomp.boot.prime]
    PrimeDecompAux.ifnz_spec [ind, in mathcomp.boot.prime]
    PrimeDecompAux.ifnzP [prf, in mathcomp.boot.prime]
    PrimeDecompAux.IfnzPos [constr, in mathcomp.boot.prime]
    PrimeDecompAux.IfnzZero [constr, in mathcomp.boot.prime]
    PrimeIdealr [abbrev, in mathcomp.algebra.ring_quotient]
    PrimeIdealr [mod, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.Algebra_isAddClosed_mixin [proj, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.Algebra_isOppClosed_mixin [proj, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.axioms_ [rec, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.class [proj, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.clone [abbrev, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.copy [abbrev, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.Exports [mod, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.Exports.prime_idealr [abbrev, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.on [abbrev, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.on_ [abbrev, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.pack_ [def, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.phant_clone [def, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.phant_on_ [def, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.ring_quotient_isPrimeIdealrClosed_mixin [proj, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.ring_quotient_isProperIdeal_mixin [proj, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.sort [proj, in mathcomp.algebra.ring_quotient]
    PrimeIdealr.type [rec, in mathcomp.algebra.ring_quotient]
    PrimeIdealrElpiOperations [mod, in mathcomp.algebra.ring_quotient]
    primeNsig [prf, in mathcomp.boot.prime]
    primeP [prf, in mathcomp.boot.prime]
    primePn [prf, in mathcomp.boot.prime]
    primePns [prf, in mathcomp.boot.prime]
    PrimePowerField [abbrev, in mathcomp.field.finfield]
    primes [def, 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 [def, in mathcomp.solvable.primitive_action]
    primitive_action [file, in mathcomp.solvable.primitive_action]
    Primitive_Element_Theorem [prf, in mathcomp.field.separable]
    primitive_mi [prf, in mathcomp.field.qfpoly]
    primitive_poly [def, in mathcomp.field.qfpoly]
    primitive_poly_in_qpoly_eq0 [prf, in mathcomp.field.qfpoly]
    primitive_polyP [prf, in mathcomp.field.qfpoly]
    primitive_root_of_unity [def, in mathcomp.algebra.poly]
    primitive_root_splitting_abelian [prf, in mathcomp.group_representation.mxrepresentation]
    principal_comp [def, in mathcomp.group_representation.mxrepresentation]
    principal_comp_def [def, in mathcomp.group_representation.mxrepresentation]
    principal_comp_key [prf, in mathcomp.group_representation.mxrepresentation]
    print [def, in mathcomp.algebra.rat]
    print [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    print_int [def, in mathcomp.algebra.ssrint]
    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_enum [def, in mathcomp.boot.fintype]
    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 [def, in mathcomp.group_representation.character]
    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]
    prod_tuple [def, in mathcomp.solvable.burnside_app]
    prod_unsplit [def, in mathcomp.algebra.tensor]
    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]
    prodv [def, in mathcomp.field.falgebra]
    prodv0 [prf, in mathcomp.field.falgebra]
    prodv1 [prf, in mathcomp.field.falgebra]
    prodv_aspace [def, in mathcomp.field.fieldext]
    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]
    prodv_unlockable [def, 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 [def, in mathcomp.algebra.mxalgebra]
    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 [def, in mathcomp.algebra.spectral]
    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 [def, in mathcomp.algebra.vector]
    projv_id [prf, in mathcomp.algebra.vector]
    projv_proj [prf, in mathcomp.algebra.vector]
    proper [def, in mathcomp.boot.fintype]
    proper0 [prf, in mathcomp.boot.finset]
    proper1G [prf, in mathcomp.finite_group.fingroup]
    proper1set [prf, in mathcomp.boot.finset]
    proper_addv [def, in mathcomp.algebra.vector]
    proper_addv_dim [proj, in mathcomp.algebra.vector]
    proper_addv_expr [rec, in mathcomp.algebra.vector]
    proper_addv_val [proj, in mathcomp.algebra.vector]
    proper_addvP [def, in mathcomp.algebra.vector]
    proper_card [prf, in mathcomp.boot.fintype]
    proper_ideal [def, in mathcomp.algebra.ring_quotient]
    proper_irrefl [prf, in mathcomp.boot.fintype]
    proper_mxsum_expr [rec, in mathcomp.algebra.mxalgebra]
    proper_mxsum_rank [proj, in mathcomp.algebra.mxalgebra]
    proper_mxsum_val [proj, in mathcomp.algebra.mxalgebra]
    proper_mxsumP [def, in mathcomp.algebra.mxalgebra]
    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]
    ProperIdeal [abbrev, in mathcomp.algebra.ring_quotient]
    ProperIdeal [mod, in mathcomp.algebra.ring_quotient]
    ProperIdeal.axioms_ [rec, in mathcomp.algebra.ring_quotient]
    ProperIdeal.class [proj, in mathcomp.algebra.ring_quotient]
    ProperIdeal.clone [abbrev, in mathcomp.algebra.ring_quotient]
    ProperIdeal.copy [abbrev, in mathcomp.algebra.ring_quotient]
    ProperIdeal.Exports [mod, in mathcomp.algebra.ring_quotient]
    ProperIdeal.Exports.proper_ideal [abbrev, in mathcomp.algebra.ring_quotient]
    ProperIdeal.on [abbrev, in mathcomp.algebra.ring_quotient]
    ProperIdeal.on_ [abbrev, in mathcomp.algebra.ring_quotient]
    ProperIdeal.pack_ [def, in mathcomp.algebra.ring_quotient]
    ProperIdeal.phant_clone [def, in mathcomp.algebra.ring_quotient]
    ProperIdeal.phant_on_ [def, in mathcomp.algebra.ring_quotient]
    ProperIdeal.ring_quotient_isProperIdeal_mixin [proj, in mathcomp.algebra.ring_quotient]
    ProperIdeal.sort [proj, in mathcomp.algebra.ring_quotient]
    ProperIdeal.type [rec, in mathcomp.algebra.ring_quotient]
    ProperIdealElpiOperations [mod, in mathcomp.algebra.ring_quotient]
    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]
    ProperMxsum [constr, in mathcomp.algebra.mxalgebra]
    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]
    pseries [def, in mathcomp.solvable.pgroup]
    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_gFun [def, in mathcomp.solvable.pgroup]
    pseries_group [def, in mathcomp.solvable.pgroup]
    pseries_group_set [prf, in mathcomp.solvable.pgroup]
    pseries_igFun [def, in mathcomp.solvable.pgroup]
    pseries_norm2 [prf, in mathcomp.solvable.pgroup]
    pseries_normal [prf, in mathcomp.solvable.pgroup]
    pseries_pgFun [def, 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]
    psubgroup [def, in mathcomp.solvable.pgroup]
    psubgroup1 [prf, in mathcomp.solvable.pgroup]
    psubgroupJ [prf, in mathcomp.solvable.pgroup]
    purely_inseparable [def, in mathcomp.field.separable]
    purely_inseparable_element [def, in mathcomp.field.separable]
    purely_inseparable_elementP [abbrev, in mathcomp.field.separable]
    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]
    push_invariant [def, in mathcomp.boot.path]
    pval [def, in mathcomp.finite_group.perm]
    pvalE [prf, in mathcomp.finite_group.perm]
    Px [abbrev, in mathcomp.field.galois]
    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]
    pZtoC [abbrev, in mathcomp.field.cyclotomic]
    pZtoC [abbrev, in mathcomp.field.algnum]
    pZtoC [abbrev, in mathcomp.field.algC]
    pZtoQ [abbrev, in mathcomp.field.cyclotomic]
    pZtoQ [abbrev, in mathcomp.field.algnum]
    pZtoQ [abbrev, in mathcomp.field.algC]
    pZtoQ [abbrev, in mathcomp.algebra.rat]
    Generated by rocqnavi