| Global Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(23836 entries) | -
| Notation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1409 entries) | -
| Module Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(221 entries) | -
| Variable Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3574 entries) | -
| Library Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(90 entries) | -
| Lemma Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(12096 entries) | -
| Constructor Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(368 entries) | -
| Axiom Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(45 entries) | -
| Inductive Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(107 entries) | -
| Projection Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(273 entries) | -
| Section Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1140 entries) | -
| Abbreviation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(728 entries) | -
| Definition Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3596 entries) | -
| Record Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(189 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]
-permEl [in mathcomp.ssreflect.seq]
-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]
-permP [in mathcomp.ssreflect.seq]
-permPl [in mathcomp.ssreflect.seq]
-permPr [in mathcomp.ssreflect.seq]
-permutationsE [in mathcomp.ssreflect.seq]
-permutationsErot [in mathcomp.ssreflect.seq]
-permutations_all_uniq [in mathcomp.ssreflect.seq]
-permutations_uniq [in mathcomp.ssreflect.seq]
-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_permutations [in mathcomp.ssreflect.seq]
-perm_count_undup [in mathcomp.ssreflect.seq]
-perm_tally_seq [in mathcomp.ssreflect.seq]
-perm_tally [in mathcomp.ssreflect.seq]
-perm_flatten [in mathcomp.ssreflect.seq]
-perm_sumn [in mathcomp.ssreflect.seq]
-perm_iotaP [in mathcomp.ssreflect.seq]
-perm_pmap [in mathcomp.ssreflect.seq]
-perm_map_inj [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_undup [in mathcomp.ssreflect.seq]
-perm_uniq [in mathcomp.ssreflect.seq]
-perm_small_eq [in mathcomp.ssreflect.seq]
-perm_all [in mathcomp.ssreflect.seq]
-perm_has [in mathcomp.ssreflect.seq]
-perm_consP [in mathcomp.ssreflect.seq]
-perm_nilP [in mathcomp.ssreflect.seq]
-perm_mem [in mathcomp.ssreflect.seq]
-perm_size [in mathcomp.ssreflect.seq]
-perm_filterC [in mathcomp.ssreflect.seq]
-perm_filter [in mathcomp.ssreflect.seq]
-perm_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_cat [in mathcomp.ssreflect.seq]
-perm_catr [in mathcomp.ssreflect.seq]
-perm_cat2r [in mathcomp.ssreflect.seq]
-perm_cons [in mathcomp.ssreflect.seq]
-perm_catl [in mathcomp.ssreflect.seq]
-perm_cat2l [in mathcomp.ssreflect.seq]
-perm_catC [in mathcomp.ssreflect.seq]
-perm_trans [in mathcomp.ssreflect.seq]
-perm_sym [in mathcomp.ssreflect.seq]
-perm_refl [in mathcomp.ssreflect.seq]
-perm_faithful [in mathcomp.fingroup.action]
-perm_act1P [in mathcomp.fingroup.action]
-perm_mact [in mathcomp.fingroup.action]
-perm_big [in mathcomp.ssreflect.bigop]
-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_cat [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]
-PrimeDecompAux.edivn2P [in mathcomp.ssreflect.prime]
-PrimeDecompAux.elogn2P [in mathcomp.ssreflect.prime]
-PrimeDecompAux.ifnzP [in mathcomp.ssreflect.prime]
-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 Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(23836 entries) | -
| Notation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1409 entries) | -
| Module Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(221 entries) | -
| Variable Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3574 entries) | -
| Library Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(90 entries) | -
| Lemma Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(12096 entries) | -
| Constructor Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(368 entries) | -
| Axiom Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(45 entries) | -
| Inductive Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(107 entries) | -
| Projection Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(273 entries) | -
| Section Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1140 entries) | -
| Abbreviation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(728 entries) | -
| Definition Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3596 entries) | -
| Record Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(189 entries) | -