From ed05182cece6bb3706e09b2ce14af4a41a2e8141 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Apr 2018 10:54:22 +0200 Subject: generate the documentation for 1.7 --- docs/htmldoc/index_lemma_P.html | 2014 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 2014 insertions(+) create mode 100644 docs/htmldoc/index_lemma_P.html (limited to 'docs/htmldoc/index_lemma_P.html') diff --git a/docs/htmldoc/index_lemma_P.html b/docs/htmldoc/index_lemma_P.html new file mode 100644 index 0000000..4907493 --- /dev/null +++ b/docs/htmldoc/index_lemma_P.html @@ -0,0 +1,2014 @@ + + + + + +mathcomp.ssreflect.tuple + + + + +
+ + + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(23233 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1373 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(213 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3475 entries)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(89 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(11853 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(359 entries)
Axiom IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(47 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(103 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(266 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1118 entries)
Abbreviation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(691 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3461 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(185 entries)
+

P (lemma)

+PackSocleK [in mathcomp.character.mxrepresentation]
+pairg1_morphM [in mathcomp.fingroup.gproduct]
+pairmapK [in mathcomp.ssreflect.seq]
+pairmap_tupleP [in mathcomp.ssreflect.tuple]
+pairmap_cat [in mathcomp.ssreflect.seq]
+pairwise_orthogonal_cat [in mathcomp.character.classfun]
+pairwise_orthogonalP [in mathcomp.character.classfun]
+pair_invr_out [in mathcomp.algebra.ssralg]
+pair_unitP [in mathcomp.algebra.ssralg]
+pair_mulVr [in mathcomp.algebra.ssralg]
+pair_mulVl [in mathcomp.algebra.ssralg]
+pair_scaleAr [in mathcomp.algebra.ssralg]
+pair_scaleAl [in mathcomp.algebra.ssralg]
+pair_scaleDl [in mathcomp.algebra.ssralg]
+pair_scaleDr [in mathcomp.algebra.ssralg]
+pair_scale1 [in mathcomp.algebra.ssralg]
+pair_scaleA [in mathcomp.algebra.ssralg]
+pair_mulC [in mathcomp.algebra.ssralg]
+pair_one_neq0 [in mathcomp.algebra.ssralg]
+pair_mulDr [in mathcomp.algebra.ssralg]
+pair_mulDl [in mathcomp.algebra.ssralg]
+pair_mul1r [in mathcomp.algebra.ssralg]
+pair_mul1l [in mathcomp.algebra.ssralg]
+pair_mulA [in mathcomp.algebra.ssralg]
+pair_addN [in mathcomp.algebra.ssralg]
+pair_add0 [in mathcomp.algebra.ssralg]
+pair_addC [in mathcomp.algebra.ssralg]
+pair_addA [in mathcomp.algebra.ssralg]
+pair_vect_iso [in mathcomp.algebra.vector]
+pair_of_tagK [in mathcomp.ssreflect.choice]
+pair_bigA [in mathcomp.ssreflect.bigop]
+pair_big [in mathcomp.ssreflect.bigop]
+pair_big_dep [in mathcomp.ssreflect.bigop]
+pair_eq2 [in mathcomp.ssreflect.eqtype]
+pair_eq1 [in mathcomp.ssreflect.eqtype]
+pair_eqE [in mathcomp.ssreflect.eqtype]
+pair_eqP [in mathcomp.ssreflect.eqtype]
+pair1g_morphM [in mathcomp.fingroup.gproduct]
+partG_eq1 [in mathcomp.solvable.pgroup]
+partition_normedTI [in mathcomp.solvable.frobenius]
+partition_class_support [in mathcomp.solvable.frobenius]
+partition_big [in mathcomp.ssreflect.bigop]
+partition_partition [in mathcomp.ssreflect.finset]
+partition_disjoint_bigcup [in mathcomp.ssreflect.finset]
+partition_big_imset [in mathcomp.ssreflect.finset]
+partnC [in mathcomp.ssreflect.prime]
+partnI [in mathcomp.ssreflect.prime]
+partnM [in mathcomp.ssreflect.prime]
+partnNK [in mathcomp.ssreflect.prime]
+partnT [in mathcomp.ssreflect.prime]
+partnX [in mathcomp.ssreflect.prime]
+partn_part [in mathcomp.ssreflect.prime]
+partn_eq1 [in mathcomp.ssreflect.prime]
+partn_biggcd [in mathcomp.ssreflect.prime]
+partn_biglcm [in mathcomp.ssreflect.prime]
+partn_gcd [in mathcomp.ssreflect.prime]
+partn_lcm [in mathcomp.ssreflect.prime]
+partn_pi [in mathcomp.ssreflect.prime]
+partn_dvd [in mathcomp.ssreflect.prime]
+partn_exponentS [in mathcomp.solvable.abelian]
+partn0 [in mathcomp.ssreflect.prime]
+partn1 [in mathcomp.ssreflect.prime]
+part_p'nat [in mathcomp.ssreflect.prime]
+part_pnat_id [in mathcomp.ssreflect.prime]
+part_pnat [in mathcomp.ssreflect.prime]
+part_gt0 [in mathcomp.ssreflect.prime]
+Pascal [in mathcomp.ssreflect.binomial]
+pathP [in mathcomp.ssreflect.path]
+path_min_sorted [in mathcomp.ssreflect.path]
+path_sorted [in mathcomp.ssreflect.path]
+path_connect [in mathcomp.ssreflect.fingraph]
+pblockK [in mathcomp.ssreflect.finset]
+pblock_transversal [in mathcomp.ssreflect.finset]
+pblock_inj [in mathcomp.ssreflect.finset]
+pblock_equivalence [in mathcomp.ssreflect.finset]
+pblock_equivalence_partition [in mathcomp.ssreflect.finset]
+pblock_mem [in mathcomp.ssreflect.finset]
+PcanChoiceMixin [in mathcomp.ssreflect.choice]
+pcan_pickleK [in mathcomp.ssreflect.choice]
+pcan_enumP [in mathcomp.ssreflect.fintype]
+pcoreI [in mathcomp.solvable.pgroup]
+pcoreJ [in mathcomp.solvable.pgroup]
+pcoreNK [in mathcomp.solvable.pgroup]
+pcoreS [in mathcomp.solvable.pgroup]
+pcore_setI_normal [in mathcomp.solvable.pgroup]
+pcore_modp [in mathcomp.solvable.pgroup]
+pcore_mod1 [in mathcomp.solvable.pgroup]
+pcore_mod_res [in mathcomp.solvable.pgroup]
+pcore_mod_sub [in mathcomp.solvable.pgroup]
+pcore_char [in mathcomp.solvable.pgroup]
+pcore_normal [in mathcomp.solvable.pgroup]
+pcore_pgroup_id [in mathcomp.solvable.pgroup]
+pcore_max [in mathcomp.solvable.pgroup]
+pcore_sub_Hall [in mathcomp.solvable.pgroup]
+pcore_sub [in mathcomp.solvable.pgroup]
+pcore_pgroup [in mathcomp.solvable.pgroup]
+pcore_psubgroup [in mathcomp.solvable.pgroup]
+pcore_Fitting [in mathcomp.solvable.maximal]
+pcore_faithful_mx_irr [in mathcomp.character.mxabelem]
+pcore_sub_rker_mx_irr [in mathcomp.character.mxabelem]
+pcore_sub_rstab_mxsimple [in mathcomp.character.mxabelem]
+pcore_faithful_irr_act [in mathcomp.solvable.sylow]
+pcore_sub_astab_irr [in mathcomp.solvable.sylow]
+pcycleE [in mathcomp.fingroup.action]
+pcycle_perm [in mathcomp.fingroup.perm]
+pcycle_sym [in mathcomp.fingroup.perm]
+pcycle_traject [in mathcomp.fingroup.perm]
+pcycle_id [in mathcomp.fingroup.perm]
+pcycle_actperm [in mathcomp.fingroup.action]
+pdivP [in mathcomp.ssreflect.prime]
+pdiv_pfactor [in mathcomp.ssreflect.prime]
+pdiv_id [in mathcomp.ssreflect.prime]
+pdiv_min_dvd [in mathcomp.ssreflect.prime]
+pdiv_gt0 [in mathcomp.ssreflect.prime]
+pdiv_leq [in mathcomp.ssreflect.prime]
+pdiv_dvd [in mathcomp.ssreflect.prime]
+pdiv_prime [in mathcomp.ssreflect.prime]
+pdiv_p_elt [in mathcomp.solvable.abelian]
+Pdiv.ClosedField.coprimepP [in mathcomp.algebra.polydiv]
+Pdiv.ClosedField.root_coprimep [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.Bezoutp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.Bezout_coprimepPn [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.Bezout_coprimepP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimepP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimepp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimepPn [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimepX [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_XsubC [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_addl_mul [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_comp_poly [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_gdco [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_div_gcd [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_expr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_expl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_pexpr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_pexpl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_mull [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_mulr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_root [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_modr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_modl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_dvdr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_dvdl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_sym [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_scaler [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_scalel [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_def [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep_size_gcd [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprimep1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprime0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.coprime1p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.divpN0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.divp_eq0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.divp_dvd [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.divp_small [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.divp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.divp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.div0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdpN0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdpp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_prod_XsubC [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mul_XsubC [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_comp_poly [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_gdco [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_pexp2r [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_div_eq0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_gcd_idr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_gcd_idl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_gcd [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_gcdr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_gcdl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_gcdlr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_size_eqp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_opp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_scalel [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_scaler [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_eqp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_XsubCl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_exp_sub [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_exp2r [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_Pexp2l [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_exp2l [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_exp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mul2l [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mul2r [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mulIr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mulIl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_trans [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mod [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_sub [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_subl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_subr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_add_eq [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_add [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_addl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_addr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mul [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mulr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_mull [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp_leq [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvdUp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvd_eqp_divl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvd0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvd0pP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.dvd1p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.egcdpE [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.egcdpP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.egcdp_recP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.egcdp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqpP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqpxx [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_monic [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_coprimepl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_coprimepr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_rgcd_gcd [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_gcd [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_gcdl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_gcdr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_rdiv_div [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_rmod_mod [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_root [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_exp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_mulr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_mull [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_mul2l [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_mul2r [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_dvdl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_dvdr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_size [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_scale [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_rtrans [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_ltrans [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_trans [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_sym [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_eq [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp_div_XsubC [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eqp01 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.eq_dvdp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.Gauss_gcdpl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.Gauss_gcdpr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.Gauss_dvdp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.Gauss_dvdpr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.Gauss_dvdpl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdpC [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdpE [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdpp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_comp_poly [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_mul2r [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_mul2l [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_eqp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_def [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_modl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_modr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_eq0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_exp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_scaler [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_scalel [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_mulr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_mull [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_addr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_addl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp_addl_mul [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcdp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcd0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gcd1p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gdcopP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gdcop_recP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gdcop0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.gtNdvdp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.irredp_XsubCP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.irredp_XsubC [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.irredp_neq0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.leq_gcdpr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.leq_gcdpl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.leq_divpl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.leq_modp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.leq_divpr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.leq_divp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.ltn_divpr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.ltn_modpN0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.ltn_divpl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.ltn_modp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modpC [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modpp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp_XsubC [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp_coprime [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp_eq0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp_eq0P [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp_mod [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp_mulr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp_mull [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp_small [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.modp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.mod0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.mulp_gcdl [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.mulp_gcdr [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.polyC_eqp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.polyXsubCP [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.polyXsubC_eqp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.rcoprimep_coprimep [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.root_gdco [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.root_biggcd [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.root_gcd [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.root_bigmul [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.root_factor_theorem [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.scalp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.size_gcdp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.size_gcd1p [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.size_poly_eq1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.size_divp [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.size2_dvdp_gdco [in mathcomp.algebra.polydiv]
+Pdiv.CommonIdomain.uniq_roots_dvdp [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.comm_redivpP [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.leq_rmodp [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.leq_rdivp [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.ltn_rmodpN0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.ltn_rmodp [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.Nrdvdp_small [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdivp_small [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdivp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdiv0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdvdpN0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdvdp_leq [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdvdp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdvdp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdvd0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdvd0pP [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rdvd1p [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.redivp_def [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.redivp_key [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rgcdpE [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rgcdp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rgcd0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rgdcop0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rmodpC [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rmodpp [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rmodp_eq0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rmodp_eq0P [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rmodp_small [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rmodp0 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rmodp1 [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rmod0p [in mathcomp.algebra.polydiv]
+Pdiv.CommonRing.rscalp_small [in mathcomp.algebra.polydiv]
+Pdiv.ComRing.rdivp_eq [in mathcomp.algebra.polydiv]
+Pdiv.ComRing.rdvdp_eq [in mathcomp.algebra.polydiv]
+Pdiv.ComRing.rdvdp_eqP [in mathcomp.algebra.polydiv]
+Pdiv.ComRing.redivpP [in mathcomp.algebra.polydiv]
+Pdiv.Field.Bezout_eq1_coprimepP [in mathcomp.algebra.polydiv]
+Pdiv.Field.coprimep_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.cubic_irreducible [in mathcomp.algebra.polydiv]
+Pdiv.Field.divpAC [in mathcomp.algebra.polydiv]
+Pdiv.Field.divpE [in mathcomp.algebra.polydiv]
+Pdiv.Field.divpK [in mathcomp.algebra.polydiv]
+Pdiv.Field.divpKC [in mathcomp.algebra.polydiv]
+Pdiv.Field.divpp [in mathcomp.algebra.polydiv]
+Pdiv.Field.divpP [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_divl [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_pmul2r [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_pmul2l [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_mulCA [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_mulAC [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_mulA [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_addl_mul [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_addl_mul_small [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_add [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_opp [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_scaler [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_scalel [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_modpP [in mathcomp.algebra.polydiv]
+Pdiv.Field.divp_eq [in mathcomp.algebra.polydiv]
+Pdiv.Field.dvdpE [in mathcomp.algebra.polydiv]
+Pdiv.Field.dvdpP [in mathcomp.algebra.polydiv]
+Pdiv.Field.dvdp_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.dvdp_gdcor [in mathcomp.algebra.polydiv]
+Pdiv.Field.dvdp_eq_mul [in mathcomp.algebra.polydiv]
+Pdiv.Field.dvdp_eq_div [in mathcomp.algebra.polydiv]
+Pdiv.Field.dvdp_eq [in mathcomp.algebra.polydiv]
+Pdiv.Field.edivpP [in mathcomp.algebra.polydiv]
+Pdiv.Field.edivp_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.edivp_eq [in mathcomp.algebra.polydiv]
+Pdiv.Field.edivp_def [in mathcomp.algebra.polydiv]
+Pdiv.Field.egcdp_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqpfP [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqpf_eq [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_rgdco_gdco [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_gdcol [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_gdcor [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_div [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_divr [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_mod [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_modpr [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_divl [in mathcomp.algebra.polydiv]
+Pdiv.Field.eqp_modpl [in mathcomp.algebra.polydiv]
+Pdiv.Field.expp_sub [in mathcomp.algebra.polydiv]
+Pdiv.Field.gcdp_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.gdcop_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.gdcop_rec_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.leq_trunc_divp [in mathcomp.algebra.polydiv]
+Pdiv.Field.map_modp [in mathcomp.algebra.polydiv]
+Pdiv.Field.map_divp [in mathcomp.algebra.polydiv]
+Pdiv.Field.modNp [in mathcomp.algebra.polydiv]
+Pdiv.Field.modpE [in mathcomp.algebra.polydiv]
+Pdiv.Field.modpP [in mathcomp.algebra.polydiv]
+Pdiv.Field.modp_mul [in mathcomp.algebra.polydiv]
+Pdiv.Field.modp_addl_mul_small [in mathcomp.algebra.polydiv]
+Pdiv.Field.modp_add [in mathcomp.algebra.polydiv]
+Pdiv.Field.modp_opp [in mathcomp.algebra.polydiv]
+Pdiv.Field.modp_scaler [in mathcomp.algebra.polydiv]
+Pdiv.Field.modp_scalel [in mathcomp.algebra.polydiv]
+Pdiv.Field.mulKp [in mathcomp.algebra.polydiv]
+Pdiv.Field.mulpK [in mathcomp.algebra.polydiv]
+Pdiv.Field.redivp_map [in mathcomp.algebra.polydiv]
+Pdiv.Field.reducible_cubic_root [in mathcomp.algebra.polydiv]
+Pdiv.Field.scalpE [in mathcomp.algebra.polydiv]
+Pdiv.Field.scalp_map [in mathcomp.algebra.polydiv]
+Pdiv.IdomainDefs.edivp_key [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.divpE [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.divpp [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.divp_eq [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.dvdpP [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.dvdp_eq [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.modpE [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.mulKp [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.mulpK [in mathcomp.algebra.polydiv]
+Pdiv.IdomainMonic.scalpE [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divpAC [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divpK [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divpKC [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divpp [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divpP [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_scaler [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_divl [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_pmul2r [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_pmul2l [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_mulCA [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_mulAC [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_mulA [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_addl_mul [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_addl_mul_small [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_add [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_opp [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_scalel [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.divp_eq [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.dvdpP [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.dvdp_eq_mul [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.dvdp_eq_div [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.dvdp_eq [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.edivpP [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.eqp_divl [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.eqp_modpl [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.expp_sub [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.leq_trunc_divp [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.modpP [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.modp_scaler [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.modp_mul [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.modp_addl_mul_small [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.modp_add [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.modp_opp [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.modp_scalel [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.mulKp [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.mulpK [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.ucl_eqp_eq [in mathcomp.algebra.polydiv]
+Pdiv.IdomainUnit.ulc_eqpP [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.eq_rdvdp [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.rdivpK [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.rdivpp [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.rdivp_eq [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.rdvdpp [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.rdvdp_mull [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.rdvdp_eqP [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.redivp_eq [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.rmodpp [in mathcomp.algebra.polydiv]
+Pdiv.RingComRreg.rmodp_mull [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.eq_rdvdp [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdivpK [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdivpp [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdivp_mull [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdivp_addr [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdivp_addl [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdivp_addl_mul [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdivp_addl_mul_small [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdivp_eq [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdvdpP [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdvdpp [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rdvdp_mull [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.redivp_eq [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rmodpp [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rmodp_mulmr [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rmodp_add [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rmodp_addl_mul_small [in mathcomp.algebra.polydiv]
+Pdiv.RingMonic.rmodp_mull [in mathcomp.algebra.polydiv]
+Pdiv.Ring.polyXsubCP [in mathcomp.algebra.polydiv]
+Pdiv.Ring.rdivp1 [in mathcomp.algebra.polydiv]
+Pdiv.Ring.rdvdp_XsubCl [in mathcomp.algebra.polydiv]
+Pdiv.Ring.root_factor_theorem [in mathcomp.algebra.polydiv]
+Pdiv.UnitRing.uniq_roots_rdvdp [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.divpE [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.divpK [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.divpKC [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.divpp [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.divp_eq [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.dvdpE [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.dvdpP [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.dvdp_eq [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.edivpP [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.edivp_eq [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.edivp_redivp [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.edivp_def [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.lc_expn_scalp_neq0 [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.modpE [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.mulKp [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.mulpK [in mathcomp.algebra.polydiv]
+Pdiv.WeakIdomain.scalpE [in mathcomp.algebra.polydiv]
+pElemI [in mathcomp.solvable.abelian]
+pElemJ [in mathcomp.solvable.abelian]
+pElemP [in mathcomp.solvable.abelian]
+pElemS [in mathcomp.solvable.abelian]
+PermDef.fun_of_permE [in mathcomp.fingroup.perm]
+PermDef.permE [in mathcomp.fingroup.perm]
+permE [in mathcomp.fingroup.perm]
+permJ [in mathcomp.fingroup.perm]
+permK [in mathcomp.fingroup.perm]
+permKV [in mathcomp.fingroup.perm]
+permM [in mathcomp.fingroup.perm]
+permP [in mathcomp.fingroup.perm]
+permX [in mathcomp.fingroup.perm]
+perm_sortP [in mathcomp.ssreflect.path]
+perm_sort [in mathcomp.ssreflect.path]
+perm_merge [in mathcomp.ssreflect.path]
+perm_onM [in mathcomp.fingroup.perm]
+perm_on1 [in mathcomp.fingroup.perm]
+perm_closed [in mathcomp.fingroup.perm]
+perm_mulP [in mathcomp.fingroup.perm]
+perm_invP [in mathcomp.fingroup.perm]
+perm_oneP [in mathcomp.fingroup.perm]
+perm_invK [in mathcomp.fingroup.perm]
+perm_onto [in mathcomp.fingroup.perm]
+perm_inj [in mathcomp.fingroup.perm]
+perm_proof [in mathcomp.fingroup.perm]
+perm_bigcprod [in mathcomp.fingroup.gproduct]
+perm_basis [in mathcomp.algebra.vector]
+perm_free [in mathcomp.algebra.vector]
+perm_mxV [in mathcomp.algebra.matrix]
+perm_mx_is_perm [in mathcomp.algebra.matrix]
+perm_mxM [in mathcomp.algebra.matrix]
+perm_mx1 [in mathcomp.algebra.matrix]
+perm_inE [in mathcomp.fingroup.automorphism]
+perm_in_on [in mathcomp.fingroup.automorphism]
+perm_in_inj [in mathcomp.fingroup.automorphism]
+perm_undup_count [in mathcomp.ssreflect.seq]
+perm_eq_iotaP [in mathcomp.ssreflect.seq]
+perm_map [in mathcomp.ssreflect.seq]
+perm_to_subseq [in mathcomp.ssreflect.seq]
+perm_to_rem [in mathcomp.ssreflect.seq]
+perm_eq_uniq [in mathcomp.ssreflect.seq]
+perm_uniq [in mathcomp.ssreflect.seq]
+perm_eq_small [in mathcomp.ssreflect.seq]
+perm_eq_size [in mathcomp.ssreflect.seq]
+perm_eq_all [in mathcomp.ssreflect.seq]
+perm_eq_mem [in mathcomp.ssreflect.seq]
+perm_filterC [in mathcomp.ssreflect.seq]
+perm_filter [in mathcomp.ssreflect.seq]
+perm_eq_rev [in mathcomp.ssreflect.seq]
+perm_rotr [in mathcomp.ssreflect.seq]
+perm_rot [in mathcomp.ssreflect.seq]
+perm_rcons [in mathcomp.ssreflect.seq]
+perm_catCA [in mathcomp.ssreflect.seq]
+perm_catAC [in mathcomp.ssreflect.seq]
+perm_cat2r [in mathcomp.ssreflect.seq]
+perm_cons [in mathcomp.ssreflect.seq]
+perm_cat2l [in mathcomp.ssreflect.seq]
+perm_catC [in mathcomp.ssreflect.seq]
+perm_eqrP [in mathcomp.ssreflect.seq]
+perm_eqlP [in mathcomp.ssreflect.seq]
+perm_eqlE [in mathcomp.ssreflect.seq]
+perm_eq_trans [in mathcomp.ssreflect.seq]
+perm_eq_sym [in mathcomp.ssreflect.seq]
+perm_eq_refl [in mathcomp.ssreflect.seq]
+perm_eqP [in mathcomp.ssreflect.seq]
+perm_eq_abelian_type [in mathcomp.solvable.abelian]
+perm_faithful [in mathcomp.fingroup.action]
+perm_act1P [in mathcomp.fingroup.action]
+perm_mact [in mathcomp.fingroup.action]
+perm1 [in mathcomp.fingroup.perm]
+pexpIrz [in mathcomp.algebra.ssrint]
+pexprz_eq1 [in mathcomp.algebra.ssrint]
+Pextraspecial.actP [in mathcomp.solvable.extraspecial]
+Pextraspecial.gactP [in mathcomp.solvable.extraspecial]
+Pextraspecial.gtype_key [in mathcomp.solvable.extraspecial]
+pfactorK [in mathcomp.ssreflect.prime]
+pfactorKpdiv [in mathcomp.ssreflect.prime]
+pfactor_coprime [in mathcomp.ssreflect.prime]
+pfactor_dvdnn [in mathcomp.ssreflect.prime]
+pfactor_dvdn [in mathcomp.ssreflect.prime]
+pfactor_gt0 [in mathcomp.ssreflect.prime]
+pfamilyP [in mathcomp.ssreflect.finfun]
+pffun_onP [in mathcomp.ssreflect.finfun]
+pgroupE [in mathcomp.solvable.pgroup]
+pgroupJ [in mathcomp.solvable.pgroup]
+pgroupM [in mathcomp.solvable.pgroup]
+pgroupNK [in mathcomp.solvable.pgroup]
+pgroupP [in mathcomp.solvable.pgroup]
+pgroupS [in mathcomp.solvable.pgroup]
+pgroup_pdiv [in mathcomp.solvable.pgroup]
+pgroup_p [in mathcomp.solvable.pgroup]
+pgroup_pi [in mathcomp.solvable.pgroup]
+pgroup_cyclic_faithful [in mathcomp.character.character]
+pgroup_sol [in mathcomp.solvable.sylow]
+pgroup_nil [in mathcomp.solvable.sylow]
+pgroup_fix_mod [in mathcomp.solvable.sylow]
+pgroup1 [in mathcomp.solvable.pgroup]
+pHallE [in mathcomp.solvable.pgroup]
+pHallJ [in mathcomp.solvable.pgroup]
+pHallJnorm [in mathcomp.solvable.pgroup]
+pHallJ2 [in mathcomp.solvable.pgroup]
+pHallNK [in mathcomp.solvable.pgroup]
+pHallP [in mathcomp.solvable.pgroup]
+pHall_id [in mathcomp.solvable.pgroup]
+pHall_subl [in mathcomp.solvable.pgroup]
+pHall_Hall [in mathcomp.solvable.pgroup]
+pHall_pgroup [in mathcomp.solvable.pgroup]
+pHall_sub [in mathcomp.solvable.pgroup]
+PhiJ [in mathcomp.solvable.maximal]
+PhiS [in mathcomp.solvable.maximal]
+Phi_mulg [in mathcomp.solvable.maximal]
+Phi_cprod [in mathcomp.solvable.maximal]
+Phi_min [in mathcomp.solvable.maximal]
+Phi_Mho [in mathcomp.solvable.maximal]
+Phi_joing [in mathcomp.solvable.maximal]
+Phi_quotient_abelem [in mathcomp.solvable.maximal]
+Phi_quotient_cyclic [in mathcomp.solvable.maximal]
+Phi_quotient_id [in mathcomp.solvable.maximal]
+Phi_normal [in mathcomp.solvable.maximal]
+Phi_char [in mathcomp.solvable.maximal]
+Phi_nongen [in mathcomp.solvable.maximal]
+Phi_proper [in mathcomp.solvable.maximal]
+Phi_sub_max [in mathcomp.solvable.maximal]
+Phi_sub [in mathcomp.solvable.maximal]
+pickleK [in mathcomp.ssreflect.choice]
+pickleK_inv [in mathcomp.ssreflect.choice]
+pickle_taggedK [in mathcomp.ssreflect.choice]
+pickle_seqK [in mathcomp.ssreflect.choice]
+pickle_invK [in mathcomp.ssreflect.choice]
+pickP [in mathcomp.ssreflect.fintype]
+pid_mx_id [in mathcomp.algebra.matrix]
+pid_mx_minh [in mathcomp.algebra.matrix]
+pid_mx_minv [in mathcomp.algebra.matrix]
+pid_mx_block [in mathcomp.algebra.matrix]
+pid_mx_col [in mathcomp.algebra.matrix]
+pid_mx_row [in mathcomp.algebra.matrix]
+pid_mx_1 [in mathcomp.algebra.matrix]
+pid_mx_0 [in mathcomp.algebra.matrix]
+pid_mx_key [in mathcomp.algebra.matrix]
+piOhm1 [in mathcomp.solvable.abelian]
+piP [in mathcomp.ssreflect.generic_quotient]
+piSg [in mathcomp.fingroup.fingroup]
+pi_p'group [in mathcomp.solvable.pgroup]
+pi_pgroup [in mathcomp.solvable.pgroup]
+pi_subfext_inv [in mathcomp.field.fieldext]
+pi_subfext_mul [in mathcomp.field.fieldext]
+pi_subfext_opp [in mathcomp.field.fieldext]
+pi_subfext_add [in mathcomp.field.fieldext]
+pi_subfx_inj [in mathcomp.field.fieldext]
+pi_p'nat [in mathcomp.ssreflect.prime]
+pi_pnat [in mathcomp.ssreflect.prime]
+pi_of_prime [in mathcomp.ssreflect.prime]
+pi_of_exp [in mathcomp.ssreflect.prime]
+pi_of_part [in mathcomp.ssreflect.prime]
+pi_ofM [in mathcomp.ssreflect.prime]
+pi_of_dvd [in mathcomp.ssreflect.prime]
+pi_max_pdiv [in mathcomp.ssreflect.prime]
+pi_pdiv [in mathcomp.ssreflect.prime]
+pi_invr [in mathcomp.algebra.ring_quotient]
+pi_unitr [in mathcomp.algebra.ring_quotient]
+pi_is_multiplicative [in mathcomp.algebra.ring_quotient]
+pi_mulr [in mathcomp.algebra.ring_quotient]
+pi_oner [in mathcomp.algebra.ring_quotient]
+pi_is_additive [in mathcomp.algebra.ring_quotient]
+pi_addr [in mathcomp.algebra.ring_quotient]
+pi_oppr [in mathcomp.algebra.ring_quotient]
+pi_zeror [in mathcomp.algebra.ring_quotient]
+pi_eq_quot [in mathcomp.ssreflect.generic_quotient]
+pi_morph11 [in mathcomp.ssreflect.generic_quotient]
+pi_mono2 [in mathcomp.ssreflect.generic_quotient]
+pi_mono1 [in mathcomp.ssreflect.generic_quotient]
+pi_morph2 [in mathcomp.ssreflect.generic_quotient]
+pi_morph1 [in mathcomp.ssreflect.generic_quotient]
+pi_of_exponent [in mathcomp.solvable.abelian]
+pi_center_nilpotent [in mathcomp.solvable.sylow]
+pi'_p'group [in mathcomp.solvable.pgroup]
+pi'_p'nat [in mathcomp.ssreflect.prime]
+plusE [in mathcomp.ssreflect.ssrnat]
+pmapS_filter [in mathcomp.ssreflect.seq]
+pmap_sub_uniq [in mathcomp.ssreflect.seq]
+pmap_uniq [in mathcomp.ssreflect.seq]
+pmap_filter [in mathcomp.ssreflect.seq]
+pmaxElemJ [in mathcomp.solvable.abelian]
+pmaxElemP [in mathcomp.solvable.abelian]
+pmaxElemS [in mathcomp.solvable.abelian]
+pmaxElem_LdivP [in mathcomp.solvable.abelian]
+pmaxElem_exists [in mathcomp.solvable.abelian]
+pmaxElem_extraspecial [in mathcomp.solvable.maximal]
+pmorphimF [in mathcomp.solvable.gfunctor]
+pmorphim_pHall [in mathcomp.solvable.pgroup]
+pmorphim_pgroup [in mathcomp.solvable.pgroup]
+pmulrn [in mathcomp.algebra.ssrint]
+pmulrz_rle0 [in mathcomp.algebra.ssrint]
+pmulrz_rge0 [in mathcomp.algebra.ssrint]
+pmulrz_rlt0 [in mathcomp.algebra.ssrint]
+pmulrz_rgt0 [in mathcomp.algebra.ssrint]
+pmulrz_lle0 [in mathcomp.algebra.ssrint]
+pmulrz_lge0 [in mathcomp.algebra.ssrint]
+pmulrz_llt0 [in mathcomp.algebra.ssrint]
+pmulrz_lgt0 [in mathcomp.algebra.ssrint]
+pnatE [in mathcomp.ssreflect.prime]
+pnatI [in mathcomp.ssreflect.prime]
+pnatNK [in mathcomp.ssreflect.prime]
+pnatP [in mathcomp.ssreflect.prime]
+pnatPpi [in mathcomp.ssreflect.prime]
+pnat_1 [in mathcomp.ssreflect.prime]
+pnat_coprime [in mathcomp.ssreflect.prime]
+pnat_div [in mathcomp.ssreflect.prime]
+pnat_dvd [in mathcomp.ssreflect.prime]
+pnat_pi [in mathcomp.ssreflect.prime]
+pnat_id [in mathcomp.ssreflect.prime]
+pnat_exp [in mathcomp.ssreflect.prime]
+pnat_mul [in mathcomp.ssreflect.prime]
+pnat_exponent [in mathcomp.solvable.abelian]
+pnElemE [in mathcomp.solvable.abelian]
+pnElemI [in mathcomp.solvable.abelian]
+pnElemJ [in mathcomp.solvable.abelian]
+pnElemP [in mathcomp.solvable.abelian]
+pnElemPcard [in mathcomp.solvable.abelian]
+pnElemS [in mathcomp.solvable.abelian]
+pnElem_prime [in mathcomp.solvable.abelian]
+pnElem0 [in mathcomp.solvable.abelian]
+polyCK [in mathcomp.algebra.poly]
+polyC_inv [in mathcomp.algebra.poly]
+polyC_exp [in mathcomp.algebra.poly]
+polyC_multiplicative [in mathcomp.algebra.poly]
+polyC_mul [in mathcomp.algebra.poly]
+polyC_muln [in mathcomp.algebra.poly]
+polyC_sub [in mathcomp.algebra.poly]
+polyC_opp [in mathcomp.algebra.poly]
+polyC_add [in mathcomp.algebra.poly]
+polyC_eq0 [in mathcomp.algebra.poly]
+polyC_inj [in mathcomp.algebra.poly]
+polyC_mulrz [in mathcomp.algebra.ssrint]
+polyC0 [in mathcomp.algebra.poly]
+polyC1 [in mathcomp.algebra.poly]
+PolyK [in mathcomp.algebra.poly]
+polyOverC [in mathcomp.algebra.poly]
+polyOverNr [in mathcomp.algebra.poly]
+polyOverP [in mathcomp.algebra.poly]
+polyOverS [in mathcomp.algebra.poly]
+polyOverSv [in mathcomp.field.fieldext]
+polyOverX [in mathcomp.algebra.poly]
+polyOverXsubC [in mathcomp.algebra.poly]
+polyOverZ [in mathcomp.algebra.poly]
+polyOver_subvs [in mathcomp.field.fieldext]
+polyOver_dvdzP [in mathcomp.algebra.intdiv]
+polyOver_comp [in mathcomp.algebra.poly]
+polyOver_nderivn [in mathcomp.algebra.poly]
+polyOver_derivn [in mathcomp.algebra.poly]
+polyOver_deriv [in mathcomp.algebra.poly]
+polyOver_mulr_closed [in mathcomp.algebra.poly]
+polyOver_addr_closed [in mathcomp.algebra.poly]
+polyOver_poly [in mathcomp.algebra.poly]
+polyOver_key [in mathcomp.algebra.poly]
+polyOver0 [in mathcomp.algebra.poly]
+polyOver1P [in mathcomp.field.falgebra]
+polyP [in mathcomp.algebra.poly]
+polyseqC [in mathcomp.algebra.poly]
+polyseqK [in mathcomp.algebra.poly]
+polyseqMX [in mathcomp.algebra.poly]
+polyseqMXn [in mathcomp.algebra.poly]
+polyseqX [in mathcomp.algebra.poly]
+polyseqXn [in mathcomp.algebra.poly]
+polyseqXsubC [in mathcomp.algebra.poly]
+polyseq_poly [in mathcomp.algebra.poly]
+polyseq_cons [in mathcomp.algebra.poly]
+polyseq0 [in mathcomp.algebra.poly]
+polyseq1 [in mathcomp.algebra.poly]
+polySpred [in mathcomp.algebra.poly]
+polyXsubC_eq0 [in mathcomp.algebra.poly]
+polyX_eq0 [in mathcomp.algebra.poly]
+polyX_key [in mathcomp.algebra.poly]
+poly_square_freeP [in mathcomp.field.separable]
+poly_rV_is_linear [in mathcomp.algebra.mxpoly]
+poly_rV_K [in mathcomp.algebra.mxpoly]
+poly_XmY_eq0 [in mathcomp.algebra.polyXY]
+poly_XaY_eq0 [in mathcomp.algebra.polyXY]
+poly_XmY0 [in mathcomp.algebra.polyXY]
+poly_XaY0 [in mathcomp.algebra.polyXY]
+poly_invE [in mathcomp.algebra.poly]
+poly_unitE [in mathcomp.algebra.poly]
+poly_inv_out [in mathcomp.algebra.poly]
+poly_intro_unit [in mathcomp.algebra.poly]
+poly_mulVp [in mathcomp.algebra.poly]
+poly_idomainAxiom [in mathcomp.algebra.poly]
+poly_mul_comm [in mathcomp.algebra.poly]
+poly_initial [in mathcomp.algebra.poly]
+poly_morphX_comm [in mathcomp.algebra.poly]
+poly_def [in mathcomp.algebra.poly]
+poly_ind [in mathcomp.algebra.poly]
+poly_key [in mathcomp.algebra.poly]
+poly_inj [in mathcomp.algebra.poly]
+poly0Vpos [in mathcomp.algebra.poly]
+poly1_neq0 [in mathcomp.algebra.poly]
+poly2_root [in mathcomp.algebra.poly]
+posnP [in mathcomp.ssreflect.ssrnat]
+PoszD [in mathcomp.algebra.ssrint]
+PoszM [in mathcomp.algebra.ssrint]
+powersetCE [in mathcomp.ssreflect.finset]
+powersetE [in mathcomp.ssreflect.finset]
+powersetI [in mathcomp.ssreflect.finset]
+powersetS [in mathcomp.ssreflect.finset]
+powersetT [in mathcomp.ssreflect.finset]
+powerset0 [in mathcomp.ssreflect.finset]
+powerset1 [in mathcomp.ssreflect.finset]
+pprodE [in mathcomp.fingroup.gproduct]
+pprodEY [in mathcomp.fingroup.gproduct]
+pprodg1 [in mathcomp.fingroup.gproduct]
+pprodJ [in mathcomp.fingroup.gproduct]
+pprodmE [in mathcomp.fingroup.gproduct]
+pprodmEl [in mathcomp.fingroup.gproduct]
+pprodmEr [in mathcomp.fingroup.gproduct]
+pprodmM [in mathcomp.fingroup.gproduct]
+pprodP [in mathcomp.fingroup.gproduct]
+pprodW [in mathcomp.fingroup.gproduct]
+pprodWC [in mathcomp.fingroup.gproduct]
+pprodWY [in mathcomp.fingroup.gproduct]
+pprod1g [in mathcomp.fingroup.gproduct]
+pquotient_pcore [in mathcomp.solvable.pgroup]
+pquotient_pHall [in mathcomp.solvable.pgroup]
+pquotient_pgroup [in mathcomp.solvable.pgroup]
+PreClosedField.closed_nonrootP [in mathcomp.algebra.poly]
+PreClosedField.closed_rootP [in mathcomp.algebra.poly]
+predC_closed [in mathcomp.ssreflect.fingraph]
+predD1P [in mathcomp.ssreflect.eqtype]
+prednK [in mathcomp.ssreflect.ssrnat]
+predn_exp [in mathcomp.ssreflect.binomial]
+predn_int [in mathcomp.algebra.ssrint]
+predT_subset [in mathcomp.ssreflect.fintype]
+predU1l [in mathcomp.ssreflect.eqtype]
+predU1P [in mathcomp.ssreflect.eqtype]
+predU1r [in mathcomp.ssreflect.eqtype]
+predX_prod_enum [in mathcomp.ssreflect.fintype]
+pred0P [in mathcomp.ssreflect.fintype]
+pred0Pn [in mathcomp.ssreflect.fintype]
+pred1E [in mathcomp.ssreflect.eqtype]
+pred2P [in mathcomp.ssreflect.eqtype]
+prefix_subseq [in mathcomp.ssreflect.seq]
+preimsetC [in mathcomp.ssreflect.finset]
+preimsetD [in mathcomp.ssreflect.finset]
+preimsetI [in mathcomp.ssreflect.finset]
+preimsetS [in mathcomp.ssreflect.finset]
+preimsetT [in mathcomp.ssreflect.finset]
+preimsetU [in mathcomp.ssreflect.finset]
+preimset_proper [in mathcomp.ssreflect.finset]
+preimset0 [in mathcomp.ssreflect.finset]
+preim_permV [in mathcomp.fingroup.perm]
+preim_autE [in mathcomp.fingroup.automorphism]
+preim_iinv [in mathcomp.ssreflect.fintype]
+preim_partition_pblock [in mathcomp.ssreflect.finset]
+preim_partitionP [in mathcomp.ssreflect.finset]
+prev_map [in mathcomp.ssreflect.path]
+prev_rev [in mathcomp.ssreflect.path]
+prev_rotr [in mathcomp.ssreflect.path]
+prev_rot [in mathcomp.ssreflect.path]
+prev_next [in mathcomp.ssreflect.path]
+prev_cycle [in mathcomp.ssreflect.path]
+prev_nth [in mathcomp.ssreflect.path]
+pre_image [in mathcomp.ssreflect.fintype]
+primeChar_dimf [in mathcomp.field.finfield]
+primeChar_vectAxiom [in mathcomp.field.finfield]
+primeChar_pgroup [in mathcomp.field.finfield]
+primeChar_abelem [in mathcomp.field.finfield]
+primeChar_scaleAr [in mathcomp.field.finfield]
+primeChar_scaleAl [in mathcomp.field.finfield]
+primeChar_scaleDl [in mathcomp.field.finfield]
+primeChar_scaleDr [in mathcomp.field.finfield]
+primeChar_scale1 [in mathcomp.field.finfield]
+primeChar_scaleA [in mathcomp.field.finfield]
+primeP [in mathcomp.ssreflect.prime]
+primePn [in mathcomp.ssreflect.prime]
+primePns [in mathcomp.ssreflect.prime]
+PrimePowerField [in mathcomp.field.finfield]
+primes_class_simple_gt1 [in mathcomp.character.integral_char]
+primes_part [in mathcomp.ssreflect.prime]
+primes_prime [in mathcomp.ssreflect.prime]
+primes_exp [in mathcomp.ssreflect.prime]
+primes_mul [in mathcomp.ssreflect.prime]
+primes_uniq [in mathcomp.ssreflect.prime]
+primes_exponent [in mathcomp.solvable.abelian]
+prime_subgroupVti [in mathcomp.solvable.pgroup]
+prime_dvd_bin [in mathcomp.ssreflect.binomial]
+prime_FrobeniusP [in mathcomp.solvable.frobenius]
+prime_decompE [in mathcomp.ssreflect.prime]
+prime_above [in mathcomp.ssreflect.prime]
+prime_coprime [in mathcomp.ssreflect.prime]
+prime_oddPn [in mathcomp.ssreflect.prime]
+prime_gt0 [in mathcomp.ssreflect.prime]
+prime_gt1 [in mathcomp.ssreflect.prime]
+prime_nt_dvdP [in mathcomp.ssreflect.prime]
+prime_decomp_correct [in mathcomp.ssreflect.prime]
+prime_idealrM [in mathcomp.algebra.ring_quotient]
+prime_Ohm1P [in mathcomp.solvable.extremal]
+prime_invariant_irr_extendible [in mathcomp.character.inertia]
+prime_abelem [in mathcomp.solvable.abelian]
+prime_meetG [in mathcomp.fingroup.fingroup]
+prime_TIg [in mathcomp.fingroup.fingroup]
+prime_cyclic [in mathcomp.solvable.cyclic]
+primitive_root_splitting_abelian [in mathcomp.character.mxrepresentation]
+Primitive_Element_Theorem [in mathcomp.field.separable]
+prim_trans_norm [in mathcomp.solvable.primitive_action]
+prim_rootP [in mathcomp.algebra.poly]
+prim_root_exp_coprime [in mathcomp.algebra.poly]
+prim_order_dvd [in mathcomp.algebra.poly]
+prim_expr_mod [in mathcomp.algebra.poly]
+prim_expr_order [in mathcomp.algebra.poly]
+prim_order_gt0 [in mathcomp.algebra.poly]
+prim_order_exists [in mathcomp.algebra.poly]
+principal_comp_key [in mathcomp.character.mxrepresentation]
+principal_comp_subproof [in mathcomp.character.mxrepresentation]
+prodMz [in mathcomp.algebra.ssrint]
+prodn_gt0 [in mathcomp.ssreflect.bigop]
+prodn_cond_gt0 [in mathcomp.ssreflect.bigop]
+prodsgP [in mathcomp.fingroup.fingroup]
+prodvA [in mathcomp.field.falgebra]
+prodvAC [in mathcomp.field.fieldext]
+prodvC [in mathcomp.field.fieldext]
+prodvCA [in mathcomp.field.fieldext]
+prodvDl [in mathcomp.field.falgebra]
+prodvDr [in mathcomp.field.falgebra]
+prodvP [in mathcomp.field.falgebra]
+prodvS [in mathcomp.field.falgebra]
+prodvSl [in mathcomp.field.falgebra]
+prodvSr [in mathcomp.field.falgebra]
+prodv_is_aspace [in mathcomp.field.fieldext]
+prodv_sub [in mathcomp.field.falgebra]
+prodv_id [in mathcomp.field.falgebra]
+prodv_line [in mathcomp.field.falgebra]
+prodv_key [in mathcomp.field.falgebra]
+prodv0 [in mathcomp.field.falgebra]
+prodv1 [in mathcomp.field.falgebra]
+prod_constt [in mathcomp.solvable.pgroup]
+prod_tpermP [in mathcomp.fingroup.perm]
+prod_prime_decomp [in mathcomp.ssreflect.prime]
+prod_Cyclotomic [in mathcomp.field.cyclotomic]
+prod_cyclotomic [in mathcomp.field.cyclotomic]
+prod_repr_lin [in mathcomp.character.character]
+prod_mx_repr [in mathcomp.character.character]
+prod_enumP [in mathcomp.ssreflect.fintype]
+prod_cfunE [in mathcomp.character.classfun]
+prod_nat_const_nat [in mathcomp.ssreflect.bigop]
+prod_nat_const [in mathcomp.ssreflect.bigop]
+prod_t_correct [in mathcomp.solvable.burnside_app]
+prod0v [in mathcomp.field.falgebra]
+prod1v [in mathcomp.field.falgebra]
+projv_proj [in mathcomp.algebra.vector]
+projv_id [in mathcomp.algebra.vector]
+proj_mx_hom [in mathcomp.character.mxrepresentation]
+proj_factmodS [in mathcomp.character.mxrepresentation]
+proj_mx_proj [in mathcomp.algebra.mxalgebra]
+proj_mx_0 [in mathcomp.algebra.mxalgebra]
+proj_mx_id [in mathcomp.algebra.mxalgebra]
+proj_mx_compl_sub [in mathcomp.algebra.mxalgebra]
+proj_mx_sub [in mathcomp.algebra.mxalgebra]
+properD [in mathcomp.ssreflect.finset]
+properD1 [in mathcomp.ssreflect.finset]
+properE [in mathcomp.ssreflect.fintype]
+properEcard [in mathcomp.ssreflect.finset]
+properEneq [in mathcomp.ssreflect.finset]
+properG_ltn_log [in mathcomp.solvable.pgroup]
+properI [in mathcomp.ssreflect.finset]
+properIl [in mathcomp.ssreflect.finset]
+properIr [in mathcomp.ssreflect.finset]
+properIset [in mathcomp.ssreflect.finset]
+properJ [in mathcomp.fingroup.fingroup]
+properP [in mathcomp.ssreflect.fintype]
+properT [in mathcomp.ssreflect.finset]
+properU [in mathcomp.ssreflect.finset]
+properUl [in mathcomp.ssreflect.finset]
+properUr [in mathcomp.ssreflect.finset]
+properxx [in mathcomp.ssreflect.fintype]
+proper_irrefl [in mathcomp.ssreflect.fintype]
+proper_card [in mathcomp.ssreflect.fintype]
+proper_sub_trans [in mathcomp.ssreflect.fintype]
+proper_trans [in mathcomp.ssreflect.fintype]
+proper_subn [in mathcomp.ssreflect.fintype]
+proper_sub [in mathcomp.ssreflect.fintype]
+proper_neq [in mathcomp.ssreflect.finset]
+proper0 [in mathcomp.ssreflect.finset]
+proper1G [in mathcomp.fingroup.fingroup]
+proper1set [in mathcomp.ssreflect.finset]
+pseriesJ [in mathcomp.solvable.pgroup]
+pseriesS [in mathcomp.solvable.pgroup]
+pseries_rcons_id [in mathcomp.solvable.pgroup]
+pseries_char_catr [in mathcomp.solvable.pgroup]
+pseries_catr_id [in mathcomp.solvable.pgroup]
+pseries_char_catl [in mathcomp.solvable.pgroup]
+pseries_catl_id [in mathcomp.solvable.pgroup]
+pseries_sub_catr [in mathcomp.solvable.pgroup]
+pseries_norm2 [in mathcomp.solvable.pgroup]
+pseries_sub_catl [in mathcomp.solvable.pgroup]
+pseries_pop2 [in mathcomp.solvable.pgroup]
+pseries_pop [in mathcomp.solvable.pgroup]
+pseries_normal [in mathcomp.solvable.pgroup]
+pseries_char [in mathcomp.solvable.pgroup]
+pseries_sub [in mathcomp.solvable.pgroup]
+pseries_subfun [in mathcomp.solvable.pgroup]
+pseries_rcons [in mathcomp.solvable.pgroup]
+pseries_group_set [in mathcomp.solvable.pgroup]
+pseries1 [in mathcomp.solvable.pgroup]
+psubgroupJ [in mathcomp.solvable.pgroup]
+psubgroup1 [in mathcomp.solvable.pgroup]
+purely_inseparable_trans [in mathcomp.field.separable]
+purely_inseparable_refl [in mathcomp.field.separable]
+purely_inseparableP [in mathcomp.field.separable]
+purely_inseparable_elementP [in mathcomp.field.separable]
+pvalE [in mathcomp.fingroup.perm]
+pX1p2id [in mathcomp.solvable.extraspecial]
+pX1p2n_extraspecial [in mathcomp.solvable.extraspecial]
+pX1p2n_pgroup [in mathcomp.solvable.extraspecial]
+pX1p2S [in mathcomp.solvable.extraspecial]
+pX1p2_extraspecial [in mathcomp.solvable.extraspecial]
+pX1p2_pgroup [in mathcomp.solvable.extraspecial]
+p_elt_constt [in mathcomp.solvable.pgroup]
+p_eltNK [in mathcomp.solvable.pgroup]
+p_eltJ [in mathcomp.solvable.pgroup]
+p_eltX [in mathcomp.solvable.pgroup]
+p_eltV [in mathcomp.solvable.pgroup]
+p_elt1 [in mathcomp.solvable.pgroup]
+p_eltM [in mathcomp.solvable.pgroup]
+p_eltM_norm [in mathcomp.solvable.pgroup]
+p_elt_exp [in mathcomp.solvable.pgroup]
+p_group1 [in mathcomp.solvable.pgroup]
+p_Sylow [in mathcomp.solvable.pgroup]
+p_groupJ [in mathcomp.solvable.pgroup]
+p_groupP [in mathcomp.solvable.pgroup]
+p_natP [in mathcomp.ssreflect.prime]
+p_part_gt1 [in mathcomp.ssreflect.prime]
+p_part_eq1 [in mathcomp.ssreflect.prime]
+p_part [in mathcomp.ssreflect.prime]
+p_rank_abelian [in mathcomp.solvable.abelian]
+p_rank_Ohm1 [in mathcomp.solvable.abelian]
+p_rank_p'quotient [in mathcomp.solvable.abelian]
+p_rank_dprod [in mathcomp.solvable.abelian]
+p_rank_quotient [in mathcomp.solvable.abelian]
+p_rank_le_rank [in mathcomp.solvable.abelian]
+p_rank_pmaxElem_exists [in mathcomp.solvable.abelian]
+p_rank_Hall [in mathcomp.solvable.abelian]
+p_rank_Sylow [in mathcomp.solvable.abelian]
+p_rankJ [in mathcomp.solvable.abelian]
+p_rankElem_max [in mathcomp.solvable.abelian]
+p_rankS [in mathcomp.solvable.abelian]
+p_rank_abelem [in mathcomp.solvable.abelian]
+p_rank_le_logn [in mathcomp.solvable.abelian]
+p_rank1 [in mathcomp.solvable.abelian]
+p_rank_gt0 [in mathcomp.solvable.abelian]
+p_rank_geP [in mathcomp.solvable.abelian]
+p_rank_witness [in mathcomp.solvable.abelian]
+p_abelem_split1 [in mathcomp.solvable.maximal]
+p_core_Fitting [in mathcomp.solvable.maximal]
+p_index_maximal [in mathcomp.solvable.maximal]
+p_maximal_index [in mathcomp.solvable.maximal]
+p_maximal_normal [in mathcomp.solvable.maximal]
+p'groupEpi [in mathcomp.solvable.pgroup]
+p'group_quotient_cent_prime [in mathcomp.solvable.pgroup]
+p'natE [in mathcomp.ssreflect.prime]
+p'natEpi [in mathcomp.ssreflect.prime]
+p'nat_coprime [in mathcomp.ssreflect.prime]
+p'_elt_constt [in mathcomp.solvable.pgroup]
+p1ElemE [in mathcomp.solvable.abelian]
+p2Elem_dprodP [in mathcomp.solvable.abelian]
+p2group_abelian [in mathcomp.solvable.sylow]
+p3group_extraspecial [in mathcomp.solvable.maximal]
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(23233 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1373 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(213 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3475 entries)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(89 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(11853 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(359 entries)
Axiom IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(47 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(103 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(266 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1118 entries)
Abbreviation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(691 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3461 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(185 entries)
+
+ + + +
+ + + \ No newline at end of file -- cgit v1.2.3