| 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
-p [abbreviation, in mathcomp.algebra.zmodp]-p [abbreviation, in mathcomp.algebra.zmodp]
-P [abbreviation, in mathcomp.ssreflect.finset]
-PackSocle [constructor, in mathcomp.character.mxrepresentation]
-PackSocleK [lemma, in mathcomp.character.mxrepresentation]
-pack_subCountType [definition, in mathcomp.ssreflect.choice]
-pack_subFinType [definition, in mathcomp.ssreflect.fintype]
-PairAlg [section, in mathcomp.algebra.ssralg]
-PairAlg.A1 [variable, in mathcomp.algebra.ssralg]
-PairAlg.A2 [variable, in mathcomp.algebra.ssralg]
-PairAlg.R [variable, in mathcomp.algebra.ssralg]
-PairComRing [section, in mathcomp.algebra.ssralg]
-PairComRing.R1 [variable, in mathcomp.algebra.ssralg]
-PairComRing.R2 [variable, in mathcomp.algebra.ssralg]
-pairg1 [definition, in mathcomp.fingroup.gproduct]
-pairg1_morphM [lemma, in mathcomp.fingroup.gproduct]
-PairLalg [section, in mathcomp.algebra.ssralg]
-PairLalg.A1 [variable, in mathcomp.algebra.ssralg]
-PairLalg.A2 [variable, in mathcomp.algebra.ssralg]
-PairLalg.R [variable, in mathcomp.algebra.ssralg]
-PairLmod [section, in mathcomp.algebra.ssralg]
-PairLmod.R [variable, in mathcomp.algebra.ssralg]
-PairLmod.V1 [variable, in mathcomp.algebra.ssralg]
-PairLmod.V2 [variable, in mathcomp.algebra.ssralg]
-pairmap [definition, in mathcomp.ssreflect.seq]
-pairmapK [lemma, in mathcomp.ssreflect.seq]
-pairmap_tupleP [lemma, in mathcomp.ssreflect.tuple]
-pairmap_cat [lemma, in mathcomp.ssreflect.seq]
-PairRing [section, in mathcomp.algebra.ssralg]
-PairRing.R1 [variable, in mathcomp.algebra.ssralg]
-PairRing.R2 [variable, in mathcomp.algebra.ssralg]
-PairUnitRing [section, in mathcomp.algebra.ssralg]
-PairUnitRing.R1 [variable, in mathcomp.algebra.ssralg]
-PairUnitRing.R2 [variable, in mathcomp.algebra.ssralg]
-pairwise_orthogonal_cat [lemma, in mathcomp.character.classfun]
-pairwise_orthogonalP [lemma, in mathcomp.character.classfun]
-pairwise_orthogonal [definition, in mathcomp.character.classfun]
-PairZmod [section, in mathcomp.algebra.ssralg]
-PairZmod.M1 [variable, in mathcomp.algebra.ssralg]
-PairZmod.M2 [variable, in mathcomp.algebra.ssralg]
-pair_unitRingMixin [definition, in mathcomp.algebra.ssralg]
-pair_invr_out [lemma, in mathcomp.algebra.ssralg]
-pair_unitP [lemma, in mathcomp.algebra.ssralg]
-pair_mulVr [lemma, in mathcomp.algebra.ssralg]
-pair_mulVl [lemma, in mathcomp.algebra.ssralg]
-pair_invr [definition, in mathcomp.algebra.ssralg]
-pair_unitr [definition, in mathcomp.algebra.ssralg]
-pair_scaleAr [lemma, in mathcomp.algebra.ssralg]
-pair_scaleAl [lemma, in mathcomp.algebra.ssralg]
-pair_lmodMixin [definition, in mathcomp.algebra.ssralg]
-pair_scaleDl [lemma, in mathcomp.algebra.ssralg]
-pair_scaleDr [lemma, in mathcomp.algebra.ssralg]
-pair_scale1 [lemma, in mathcomp.algebra.ssralg]
-pair_scaleA [lemma, in mathcomp.algebra.ssralg]
-pair_mulC [lemma, in mathcomp.algebra.ssralg]
-pair_ringMixin [definition, in mathcomp.algebra.ssralg]
-pair_one_neq0 [lemma, in mathcomp.algebra.ssralg]
-pair_mulDr [lemma, in mathcomp.algebra.ssralg]
-pair_mulDl [lemma, in mathcomp.algebra.ssralg]
-pair_mul1r [lemma, in mathcomp.algebra.ssralg]
-pair_mul1l [lemma, in mathcomp.algebra.ssralg]
-pair_mulA [lemma, in mathcomp.algebra.ssralg]
-pair_zmodMixin [definition, in mathcomp.algebra.ssralg]
-pair_addN [lemma, in mathcomp.algebra.ssralg]
-pair_add0 [lemma, in mathcomp.algebra.ssralg]
-pair_addC [lemma, in mathcomp.algebra.ssralg]
-pair_addA [lemma, in mathcomp.algebra.ssralg]
-pair_vectMixin [definition, in mathcomp.algebra.vector]
-pair_vect_iso [lemma, in mathcomp.algebra.vector]
-pair_of_tagK [lemma, in mathcomp.ssreflect.choice]
-pair_of_tag [definition, in mathcomp.ssreflect.choice]
-pair_ortho_rec [definition, in mathcomp.character.classfun]
-pair_bigA [lemma, in mathcomp.ssreflect.bigop]
-pair_big [lemma, in mathcomp.ssreflect.bigop]
-pair_big_dep [lemma, in mathcomp.ssreflect.bigop]
-pair_eq2 [lemma, in mathcomp.ssreflect.eqtype]
-pair_eq1 [lemma, in mathcomp.ssreflect.eqtype]
-pair_eqE [lemma, in mathcomp.ssreflect.eqtype]
-pair_eqP [lemma, in mathcomp.ssreflect.eqtype]
-pair_eq [definition, in mathcomp.ssreflect.eqtype]
-pair1g [definition, in mathcomp.fingroup.gproduct]
-pair1g_morphM [lemma, in mathcomp.fingroup.gproduct]
-partG_eq1 [lemma, in mathcomp.solvable.pgroup]
-PartialAction [section, in mathcomp.fingroup.action]
-PartialAction.aT [variable, in mathcomp.fingroup.action]
-PartialAction.D [variable, in mathcomp.fingroup.action]
-PartialAction.OrbitStabilizer [section, in mathcomp.fingroup.action]
-PartialAction.OrbitStabilizer.G [variable, in mathcomp.fingroup.action]
-PartialAction.OrbitStabilizer.sGD [variable, in mathcomp.fingroup.action]
-PartialAction.OrbitStabilizer.ssGD [variable, in mathcomp.fingroup.action]
-PartialAction.OrbitStabilizer.x [variable, in mathcomp.fingroup.action]
-PartialAction.rT [variable, in mathcomp.fingroup.action]
-PartialAction.to [variable, in mathcomp.fingroup.action]
-PartialFunctorTheory [section, in mathcomp.solvable.gfunctor]
-PartialFunctorTheory.BasicTheory [section, in mathcomp.solvable.gfunctor]
-PartialFunctorTheory.BasicTheory.F [variable, in mathcomp.solvable.gfunctor]
-PartialFunctorTheory.F1 [variable, in mathcomp.solvable.gfunctor]
-PartialFunctorTheory.F2 [variable, in mathcomp.solvable.gfunctor]
-PartialFunctorTheory.Modulo [section, in mathcomp.solvable.gfunctor]
-PartialFunctorTheory.Modulo.F1 [variable, in mathcomp.solvable.gfunctor]
-PartialFunctorTheory.Modulo.F2 [variable, in mathcomp.solvable.gfunctor]
-partial_product [definition, in mathcomp.fingroup.gproduct]
-partition [definition, in mathcomp.ssreflect.finset]
-Partitions [section, in mathcomp.ssreflect.finset]
-Partitions.BigOps [section, in mathcomp.ssreflect.finset]
-Partitions.BigOps.idx [variable, in mathcomp.ssreflect.finset]
-Partitions.BigOps.op [variable, in mathcomp.ssreflect.finset]
-Partitions.BigOps.R [variable, in mathcomp.ssreflect.finset]
-Partitions.BigOps.rhs [variable, in mathcomp.ssreflect.finset]
-Partitions.BigOps.rhs_cond [variable, in mathcomp.ssreflect.finset]
-Partitions.Equivalence [section, in mathcomp.ssreflect.finset]
-Partitions.Equivalence.D [variable, in mathcomp.ssreflect.finset]
-Partitions.Equivalence.eqiR [variable, in mathcomp.ssreflect.finset]
-Partitions.Equivalence.PPx [variable, in mathcomp.ssreflect.finset]
-Partitions.Equivalence.Px [variable, in mathcomp.ssreflect.finset]
-Partitions.Equivalence.Pxx [variable, in mathcomp.ssreflect.finset]
-Partitions.Equivalence.R [variable, in mathcomp.ssreflect.finset]
-Partitions.I [variable, in mathcomp.ssreflect.finset]
-Partitions.Preim [section, in mathcomp.ssreflect.finset]
-Partitions.Preim.f [variable, in mathcomp.ssreflect.finset]
-Partitions.Preim.rT [variable, in mathcomp.ssreflect.finset]
-Partitions.T [variable, in mathcomp.ssreflect.finset]
-Partitions.Transversals [section, in mathcomp.ssreflect.finset]
-Partitions.Transversals.D [variable, in mathcomp.ssreflect.finset]
-Partitions.Transversals.P [variable, in mathcomp.ssreflect.finset]
-Partitions.Transversals.sXP [variable, in mathcomp.ssreflect.finset]
-Partitions.Transversals.tiP [variable, in mathcomp.ssreflect.finset]
-Partitions.Transversals.trPX [variable, in mathcomp.ssreflect.finset]
-Partitions.Transversals.trX [variable, in mathcomp.ssreflect.finset]
-Partitions.Transversals.X [variable, in mathcomp.ssreflect.finset]
-partition_normedTI [lemma, in mathcomp.solvable.frobenius]
-partition_class_support [lemma, in mathcomp.solvable.frobenius]
-partition_big [lemma, in mathcomp.ssreflect.bigop]
-partition_partition [lemma, in mathcomp.ssreflect.finset]
-partition_disjoint_bigcup [lemma, in mathcomp.ssreflect.finset]
-partition_big_imset [lemma, in mathcomp.ssreflect.finset]
-partn [definition, in mathcomp.ssreflect.prime]
-partnC [lemma, in mathcomp.ssreflect.prime]
-partnI [lemma, in mathcomp.ssreflect.prime]
-partnM [lemma, in mathcomp.ssreflect.prime]
-partnNK [lemma, in mathcomp.ssreflect.prime]
-partnT [lemma, in mathcomp.ssreflect.prime]
-partnX [lemma, in mathcomp.ssreflect.prime]
-partn_part [lemma, in mathcomp.ssreflect.prime]
-partn_eq1 [lemma, in mathcomp.ssreflect.prime]
-partn_biggcd [lemma, in mathcomp.ssreflect.prime]
-partn_biglcm [lemma, in mathcomp.ssreflect.prime]
-partn_gcd [lemma, in mathcomp.ssreflect.prime]
-partn_lcm [lemma, in mathcomp.ssreflect.prime]
-partn_pi [lemma, in mathcomp.ssreflect.prime]
-partn_dvd [lemma, in mathcomp.ssreflect.prime]
-partn_exponentS [lemma, in mathcomp.solvable.abelian]
-partn0 [lemma, in mathcomp.ssreflect.prime]
-partn1 [lemma, in mathcomp.ssreflect.prime]
-part_p'nat [lemma, in mathcomp.ssreflect.prime]
-part_pnat_id [lemma, in mathcomp.ssreflect.prime]
-part_pnat [lemma, in mathcomp.ssreflect.prime]
-part_gt0 [lemma, in mathcomp.ssreflect.prime]
-Pascal [lemma, in mathcomp.ssreflect.binomial]
-path [definition, in mathcomp.ssreflect.path]
-path [library]
-pathP [lemma, in mathcomp.ssreflect.path]
-Paths [section, in mathcomp.ssreflect.path]
-Paths.n0 [variable, in mathcomp.ssreflect.path]
-Paths.Path [section, in mathcomp.ssreflect.path]
-Paths.Path.e [variable, in mathcomp.ssreflect.path]
-Paths.Path.x0_cycle [variable, in mathcomp.ssreflect.path]
-Paths.T [variable, in mathcomp.ssreflect.path]
-path_min_sorted [lemma, in mathcomp.ssreflect.path]
-path_sorted [lemma, in mathcomp.ssreflect.path]
-path_connect [lemma, in mathcomp.ssreflect.fingraph]
-pblock [definition, in mathcomp.ssreflect.finset]
-pblockK [lemma, in mathcomp.ssreflect.finset]
-pblock_transversal [lemma, in mathcomp.ssreflect.finset]
-pblock_inj [lemma, in mathcomp.ssreflect.finset]
-pblock_equivalence [lemma, in mathcomp.ssreflect.finset]
-pblock_equivalence_partition [lemma, in mathcomp.ssreflect.finset]
-pblock_mem [lemma, in mathcomp.ssreflect.finset]
-PcanChoiceMixin [lemma, in mathcomp.ssreflect.choice]
-PcanCountMixin [definition, in mathcomp.ssreflect.choice]
-PcanEqMixin [definition, in mathcomp.ssreflect.eqtype]
-PcanFinMixin [definition, in mathcomp.ssreflect.fintype]
-pcan_pickleK [lemma, in mathcomp.ssreflect.choice]
-pcan_enumP [lemma, in mathcomp.ssreflect.fintype]
-pcore [definition, in mathcomp.solvable.pgroup]
-PcoreDef [section, in mathcomp.solvable.pgroup]
-PcoreDef.A [variable, in mathcomp.solvable.pgroup]
-PcoreDef.gT [variable, in mathcomp.solvable.pgroup]
-PcoreDef.pi [variable, in mathcomp.solvable.pgroup]
-pcoreI [lemma, in mathcomp.solvable.pgroup]
-pcoreJ [lemma, in mathcomp.solvable.pgroup]
-pcoreNK [lemma, in mathcomp.solvable.pgroup]
-PCoreProps [section, in mathcomp.solvable.pgroup]
-PCoreProps.gT [variable, in mathcomp.solvable.pgroup]
-PCoreProps.pi [variable, in mathcomp.solvable.pgroup]
-pcoreS [lemma, in mathcomp.solvable.pgroup]
-pcore_setI_normal [lemma, in mathcomp.solvable.pgroup]
-pcore_modp [lemma, in mathcomp.solvable.pgroup]
-pcore_mod1 [lemma, in mathcomp.solvable.pgroup]
-pcore_mod_res [lemma, in mathcomp.solvable.pgroup]
-pcore_mod_sub [lemma, in mathcomp.solvable.pgroup]
-pcore_char [lemma, in mathcomp.solvable.pgroup]
-pcore_normal [lemma, in mathcomp.solvable.pgroup]
-pcore_pgroup_id [lemma, in mathcomp.solvable.pgroup]
-pcore_max [lemma, in mathcomp.solvable.pgroup]
-pcore_sub_Hall [lemma, in mathcomp.solvable.pgroup]
-pcore_sub [lemma, in mathcomp.solvable.pgroup]
-pcore_pgroup [lemma, in mathcomp.solvable.pgroup]
-pcore_psubgroup [lemma, in mathcomp.solvable.pgroup]
-pcore_mod [definition, in mathcomp.solvable.pgroup]
-pcore_Fitting [lemma, in mathcomp.solvable.maximal]
-pcore_faithful_mx_irr [lemma, in mathcomp.character.mxabelem]
-pcore_sub_rker_mx_irr [lemma, in mathcomp.character.mxabelem]
-pcore_sub_rstab_mxsimple [lemma, in mathcomp.character.mxabelem]
-pcore_faithful_irr_act [lemma, in mathcomp.solvable.sylow]
-pcore_sub_astab_irr [lemma, in mathcomp.solvable.sylow]
-pcycle [definition, in mathcomp.fingroup.perm]
-pcycleE [lemma, in mathcomp.fingroup.action]
-pcycles [definition, in mathcomp.fingroup.perm]
-pcycle_perm [lemma, in mathcomp.fingroup.perm]
-pcycle_sym [lemma, in mathcomp.fingroup.perm]
-pcycle_traject [lemma, in mathcomp.fingroup.perm]
-pcycle_id [lemma, in mathcomp.fingroup.perm]
-pcycle_actperm [lemma, in mathcomp.fingroup.action]
-pdiv [definition, in mathcomp.ssreflect.prime]
-Pdiv [module, in mathcomp.algebra.polydiv]
-pdivP [lemma, in mathcomp.ssreflect.prime]
-pdiv_pfactor [lemma, in mathcomp.ssreflect.prime]
-pdiv_id [lemma, in mathcomp.ssreflect.prime]
-pdiv_min_dvd [lemma, in mathcomp.ssreflect.prime]
-pdiv_gt0 [lemma, in mathcomp.ssreflect.prime]
-pdiv_leq [lemma, in mathcomp.ssreflect.prime]
-pdiv_dvd [lemma, in mathcomp.ssreflect.prime]
-pdiv_prime [lemma, in mathcomp.ssreflect.prime]
-pdiv_p_elt [lemma, in mathcomp.solvable.abelian]
-Pdiv.ClosedField [module, in mathcomp.algebra.polydiv]
-Pdiv.ClosedField.closed [section, in mathcomp.algebra.polydiv]
-Pdiv.ClosedField.closed.F [variable, in mathcomp.algebra.polydiv]
-Pdiv.ClosedField.coprimepP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.ClosedField.root_coprimep [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain [module, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.apply_irredp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.Bezoutp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.Bezout_coprimepPn [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.Bezout_coprimepP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimepP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimepp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimepPn [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimepX [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_XsubC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_addl_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_comp_poly [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_gdco [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_div_gcd [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_expr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_expl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_pexpr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_pexpl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_mulr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_root [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_modr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_modl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_dvdr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_dvdl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_sym [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_scaler [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_scalel [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_def [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep_size_gcd [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprimep1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprime0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.coprime1p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.divpN0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.divp_eq0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.divp_dvd [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.divp_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.divp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.divp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.div0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdpN0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_prod_XsubC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mul_XsubC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_comp_poly [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_gdco [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_pexp2r [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_div_eq0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_gcd_idr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_gcd_idl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_gcd [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_gcdr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_gcdl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_gcdlr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_size_eqp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_opp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_scalel [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_scaler [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_eqp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_XsubCl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_exp_sub [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_exp2r [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_Pexp2l [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_exp2l [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_exp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mul2l [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mul2r [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mulIr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mulIl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_trans [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mod [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_sub [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_subl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_subr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_add_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_add [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_addl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_addr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mulr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp_leq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvdUp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvd_eqp_divl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvd0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvd0pP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.dvd1p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.egcdp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.egcdpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.egcdpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.egcdp_recP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.egcdp_rec [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.egcdp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqpxx [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_monic [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_coprimepl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_coprimepr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_rgcd_gcd [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_gcd [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_gcdl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_gcdr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_rdiv_div [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_rmod_mod [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_root [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_exp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_mulr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_mul2l [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_mul2r [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_dvdl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_dvdr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_size [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_scale [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_rtrans [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_ltrans [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_trans [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_sym [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp_div_XsubC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eqp01 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.eq_dvdp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.Gauss_gcdpl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.Gauss_gcdpr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.Gauss_dvdp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.Gauss_dvdpr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.Gauss_dvdpl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdpC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_comp_poly [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_mul2r [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_mul2l [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_eqp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_def [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_modl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_modr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_eq0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_exp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_scaler [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_scalel [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_mulr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_addr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_addl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_addl_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp_rec [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcdp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcd0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gcd1p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gdcop [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gdcopP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.GdcopSpec [constructor, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gdcop_recP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gdcop_spec [inductive, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gdcop_rec [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gdcop0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.gtNdvdp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.IDomainPseudoDivision [section, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.IDomainPseudoDivision.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.irredp_XsubCP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.irredp_XsubC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.irredp_neq0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.irreducible_poly [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.leq_gcdpr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.leq_gcdpl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.leq_divpl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.leq_modp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.leq_divpr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.leq_divp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.ltn_divpr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.ltn_modpN0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.ltn_divpl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.ltn_modp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modpC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp_XsubC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp_coprime [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp_eq0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp_eq0P [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp_mod [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp_mulr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.modp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.mod0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.mulp_gcdl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.mulp_gcdr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.polyC_eqp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.polyXsubCP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.polyXsubC_eqp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.rcoprimep_coprimep [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.root_gdco [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.root_biggcd [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.root_gcd [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.root_bigmul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.root_factor_theorem [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.scalp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.size_gcdp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.size_gcd1p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.size_poly_eq1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.size_divp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.size2_dvdp_gdco [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonIdomain.uniq_roots_dvdp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing [module, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.ComEdivnSpec [constructor, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.comm_redivpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.comm_redivp_spec [inductive, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.leq_rmodp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.leq_rdivp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.ltn_rmodpN0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.ltn_rmodp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.Nrdvdp_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rcoprimep [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdivp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdivp_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdivp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdiv0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvdp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvdpN0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvdp_leq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvdp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvdp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvd0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvd0pP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rdvd1p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.redivp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.redivp_def [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.redivp_key [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.redivp_expanded_def [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.redivp_rec [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgcdp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgcdpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgcdp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgcd0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgdcop [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgdcop_rec [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rgdcop0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.RingPseudoDivision [section, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.RingPseudoDivision.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodpC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodp_eq0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodp_eq0P [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodp_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodp0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmodp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rmod0p [lemma, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rscalp [definition, in mathcomp.algebra.polydiv]
-Pdiv.CommonRing.rscalp_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.ComRing [module, in mathcomp.algebra.polydiv]
-Pdiv.ComRing.CommutativeRingPseudoDivision [section, in mathcomp.algebra.polydiv]
-Pdiv.ComRing.CommutativeRingPseudoDivision.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.ComRing.EdivnSpec [constructor, in mathcomp.algebra.polydiv]
-Pdiv.ComRing.rdivp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.ComRing.rdvdp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.ComRing.rdvdp_eqP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.ComRing.redivpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.ComRing.redivp_spec [inductive, in mathcomp.algebra.polydiv]
-Pdiv.Field [module, in mathcomp.algebra.polydiv]
-Pdiv.Field.Bezout_eq1_coprimepP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.coprimep_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.cubic_irreducible [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divpAC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divpKC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_divl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_pmul2r [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_pmul2l [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_mulCA [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_mulAC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_mulA [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_addl_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_addl_mul_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_add [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_opp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_scaler [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_scalel [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_modpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.divp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.dvdpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.dvdpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.dvdp_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.dvdp_gdcor [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.dvdp_eq_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.dvdp_eq_div [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.dvdp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.edivpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.EdivpSpec [constructor, in mathcomp.algebra.polydiv]
-Pdiv.Field.edivp_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.edivp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.edivp_spec [inductive, in mathcomp.algebra.polydiv]
-Pdiv.Field.edivp_def [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.egcdp_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqpfP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqpf_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_rgdco_gdco [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_gdcol [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_gdcor [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_div [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_divr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_mod [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_modpr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_divl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.eqp_modpl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.expp_sub [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.FieldDivision [section, in mathcomp.algebra.polydiv]
-Pdiv.Field.FieldDivision.F [variable, in mathcomp.algebra.polydiv]
-Pdiv.Field.FieldDivision.FieldMap [section, in mathcomp.algebra.polydiv]
-Pdiv.Field.FieldDivision.FieldMap.f [variable, in mathcomp.algebra.polydiv]
-Pdiv.Field.FieldDivision.FieldMap.rR [variable, in mathcomp.algebra.polydiv]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.polydiv]
-Pdiv.Field.FieldDivision.FieldRingMap [section, in mathcomp.algebra.polydiv]
-Pdiv.Field.FieldDivision.FieldRingMap.f [variable, in mathcomp.algebra.polydiv]
-Pdiv.Field.FieldDivision.FieldRingMap.rR [variable, in mathcomp.algebra.polydiv]
-_ ^f (ring_scope) [notation, in mathcomp.algebra.polydiv]
-Pdiv.Field.gcdp_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.gdcop_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.gdcop_rec_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.leq_trunc_divp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.map_modp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.map_divp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modNp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modp_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modp_addl_mul_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modp_add [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modp_opp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modp_scaler [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.modp_scalel [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.mulKp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.mulpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.redivp_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.reducible_cubic_root [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.scalpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Field.scalp_map [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Idomain [module, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs [module, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.divp [definition, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.dvdp [definition, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.edivp [definition, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.edivp_key [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.edivp_expanded_def [definition, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.eqp [definition, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.IDomainPseudoDivisionDefs [section, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.IDomainPseudoDivisionDefs.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.modp [definition, in mathcomp.algebra.polydiv]
-Pdiv.IdomainDefs.scalp [definition, in mathcomp.algebra.polydiv]
-_ %= _ (ring_scope) [notation, in mathcomp.algebra.polydiv]
-_ %| _ (ring_scope) [notation, in mathcomp.algebra.polydiv]
-_ %% _ (ring_scope) [notation, in mathcomp.algebra.polydiv]
-_ %/ _ (ring_scope) [notation, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic [module, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.divpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.divpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.divp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.dvdpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.dvdp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.modpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.MonicDivisor [section, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.MonicDivisor.monq [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.MonicDivisor.q [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.MonicDivisor.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.mulKp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.mulpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainMonic.scalpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit [module, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divpAC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divpKC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_scaler [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_divl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_pmul2r [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_pmul2l [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_mulCA [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_mulAC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_mulA [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_addl_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_addl_mul_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_add [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_opp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_scalel [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.divp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.dvdpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.dvdp_eq_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.dvdp_eq_div [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.dvdp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.edivpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.eqp_divl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.eqp_modpl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.expp_sub [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.leq_trunc_divp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.modpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.modp_scaler [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.modp_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.modp_addl_mul_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.modp_add [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.modp_opp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.modp_scalel [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.MoreUnitDivisor [section, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.MoreUnitDivisor.d [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.MoreUnitDivisor.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.MoreUnitDivisor.ulcd [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.mulKp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.mulpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.ucl_eqp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.ulc_eqpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.UnitDivisor [section, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.UnitDivisor.d [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.UnitDivisor.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.IdomainUnit.UnitDivisor.ulcd [variable, in mathcomp.algebra.polydiv]
-Pdiv.Ring [module, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg [module, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.ComRegDivisor [section, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.ComRegDivisor.Cdl [variable, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.ComRegDivisor.d [variable, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.ComRegDivisor.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.ComRegDivisor.Rreg [variable, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.eq_rdvdp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rdivpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rdivpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rdivp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.Rdvdp [constructor, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.RdvdpN [constructor, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rdvdpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rdvdp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rdvdp_eqP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rdvdp_spec [inductive, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.redivp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rmodpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingComRreg.rmodp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic [module, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.eq_rdvdp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.MonicDivisor [section, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.MonicDivisor.d [variable, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.MonicDivisor.mond [variable, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.MonicDivisor.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdivpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdivpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdivp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdivp_addr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdivp_addl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdivp_addl_mul [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdivp_addl_mul_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdivp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdvdpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdvdpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rdvdp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.redivp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rmodpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rmodp_mulmr [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rmodp_add [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rmodp_addl_mul_small [lemma, in mathcomp.algebra.polydiv]
-Pdiv.RingMonic.rmodp_mull [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Ring.ExtraMonicDivisor [section, in mathcomp.algebra.polydiv]
-Pdiv.Ring.ExtraMonicDivisor.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.Ring.polyXsubCP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Ring.rdivp1 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Ring.rdvdp_XsubCl [lemma, in mathcomp.algebra.polydiv]
-Pdiv.Ring.root_factor_theorem [lemma, in mathcomp.algebra.polydiv]
-Pdiv.UnitRing [module, in mathcomp.algebra.polydiv]
-Pdiv.UnitRing.uniq_roots_rdvdp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.UnitRing.UnitRingPseudoDivision [section, in mathcomp.algebra.polydiv]
-Pdiv.UnitRing.UnitRingPseudoDivision.R [variable, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain [module, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.divpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.divpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.divpKC [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.divpp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.divp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.dvdpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.dvdpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.dvdp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.edivpP [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.edivp_eq [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.edivp_spec [inductive, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.edivp_redivp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.edivp_def [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.Fedivp_spec [constructor, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.lc_expn_scalp_neq0 [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.modpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.mulKp [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.mulpK [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.Redivp_spec [constructor, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.scalpE [lemma, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.WeakTheoryForIDomainPseudoDivision [section, in mathcomp.algebra.polydiv]
-Pdiv.WeakIdomain.WeakTheoryForIDomainPseudoDivision.R [variable, in mathcomp.algebra.polydiv]
-pElem [definition, in mathcomp.solvable.abelian]
-pElemI [lemma, in mathcomp.solvable.abelian]
-pElemJ [lemma, in mathcomp.solvable.abelian]
-pElemP [lemma, in mathcomp.solvable.abelian]
-pElemS [lemma, in mathcomp.solvable.abelian]
-perm [abbreviation, in mathcomp.fingroup.perm]
-Perm [constructor, in mathcomp.fingroup.perm]
-perm [library]
-PermAction [section, in mathcomp.fingroup.action]
-PermAction.rT [variable, in mathcomp.fingroup.action]
-PermDef [module, in mathcomp.fingroup.perm]
-PermDefSection [section, in mathcomp.fingroup.perm]
-PermDefSection.T [variable, in mathcomp.fingroup.perm]
-PermDefSig [module, in mathcomp.fingroup.perm]
-PermDefSig.fun_of_permE [axiom, in mathcomp.fingroup.perm]
-PermDefSig.fun_of_perm [axiom, in mathcomp.fingroup.perm]
-PermDefSig.perm [axiom, in mathcomp.fingroup.perm]
-PermDefSig.permE [axiom, in mathcomp.fingroup.perm]
-PermDef.fun_of_permE [lemma, in mathcomp.fingroup.perm]
-PermDef.fun_of_perm [definition, in mathcomp.fingroup.perm]
-PermDef.perm [definition, in mathcomp.fingroup.perm]
-PermDef.permE [lemma, in mathcomp.fingroup.perm]
-permE [lemma, in mathcomp.fingroup.perm]
-permEl [lemma, in mathcomp.ssreflect.seq]
-PermIn [section, in mathcomp.fingroup.automorphism]
-PermIn.A [variable, in mathcomp.fingroup.automorphism]
-PermIn.f [variable, in mathcomp.fingroup.automorphism]
-PermIn.injf [variable, in mathcomp.fingroup.automorphism]
-PermIn.sBf [variable, in mathcomp.fingroup.automorphism]
-PermIn.T [variable, in mathcomp.fingroup.automorphism]
-permJ [lemma, in mathcomp.fingroup.perm]
-permK [lemma, in mathcomp.fingroup.perm]
-permKV [lemma, in mathcomp.fingroup.perm]
-permM [lemma, in mathcomp.fingroup.perm]
-permP [lemma, in mathcomp.fingroup.perm]
-permP [lemma, in mathcomp.ssreflect.seq]
-permPl [lemma, in mathcomp.ssreflect.seq]
-permPr [lemma, in mathcomp.ssreflect.seq]
-perms [abbreviation, in mathcomp.ssreflect.seq]
-PermSeq [section, in mathcomp.ssreflect.seq]
-PermSeq.T [variable, in mathcomp.ssreflect.seq]
-perms_rec [definition, in mathcomp.ssreflect.seq]
-PermutationParity [section, in mathcomp.fingroup.perm]
-PermutationParity.T [variable, in mathcomp.fingroup.perm]
-permutations [definition, in mathcomp.ssreflect.seq]
-Permutations [section, in mathcomp.ssreflect.seq]
-permutationsE [lemma, in mathcomp.ssreflect.seq]
-permutationsErot [lemma, in mathcomp.ssreflect.seq]
-permutations_all_uniq [lemma, in mathcomp.ssreflect.seq]
-permutations_uniq [lemma, in mathcomp.ssreflect.seq]
-Permutations.cons_permsE [variable, in mathcomp.ssreflect.seq]
-Permutations.permsP [variable, in mathcomp.ssreflect.seq]
-Permutations.T [variable, in mathcomp.ssreflect.seq]
-permX [lemma, in mathcomp.fingroup.perm]
-perm_sortP [lemma, in mathcomp.ssreflect.path]
-perm_sort [lemma, in mathcomp.ssreflect.path]
-perm_merge [lemma, in mathcomp.ssreflect.path]
-perm_onM [lemma, in mathcomp.fingroup.perm]
-perm_on1 [lemma, in mathcomp.fingroup.perm]
-perm_closed [lemma, in mathcomp.fingroup.perm]
-perm_on [definition, in mathcomp.fingroup.perm]
-perm_of_baseFinGroupMixin [definition, in mathcomp.fingroup.perm]
-perm_mulP [lemma, in mathcomp.fingroup.perm]
-perm_invP [lemma, in mathcomp.fingroup.perm]
-perm_oneP [lemma, in mathcomp.fingroup.perm]
-perm_mul [definition, in mathcomp.fingroup.perm]
-perm_inv [definition, in mathcomp.fingroup.perm]
-perm_invK [lemma, in mathcomp.fingroup.perm]
-perm_one [definition, in mathcomp.fingroup.perm]
-perm_onto [lemma, in mathcomp.fingroup.perm]
-perm_inj [lemma, in mathcomp.fingroup.perm]
-perm_def [abbreviation, in mathcomp.fingroup.perm]
-perm_proof [lemma, in mathcomp.fingroup.perm]
-perm_finMixin [definition, in mathcomp.fingroup.perm]
-perm_countMixin [definition, in mathcomp.fingroup.perm]
-perm_choiceMixin [definition, in mathcomp.fingroup.perm]
-perm_eqMixin [definition, in mathcomp.fingroup.perm]
-perm_of [definition, in mathcomp.fingroup.perm]
-perm_type [inductive, in mathcomp.fingroup.perm]
-perm_bigcprod [lemma, in mathcomp.fingroup.gproduct]
-perm_basis [lemma, in mathcomp.algebra.vector]
-perm_free [lemma, in mathcomp.algebra.vector]
-perm_mxV [lemma, in mathcomp.algebra.matrix]
-perm_mx_is_perm [lemma, in mathcomp.algebra.matrix]
-perm_mxM [lemma, in mathcomp.algebra.matrix]
-perm_mx1 [lemma, in mathcomp.algebra.matrix]
-perm_mx [definition, in mathcomp.algebra.matrix]
-perm_inE [lemma, in mathcomp.fingroup.automorphism]
-perm_in_on [lemma, in mathcomp.fingroup.automorphism]
-perm_in [definition, in mathcomp.fingroup.automorphism]
-perm_in_inj [lemma, in mathcomp.fingroup.automorphism]
-perm_undup_count [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_iotaP [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_consP [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_nilP [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_small [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_all [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_flatten [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_rev [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_uniq [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_mem [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_size [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_trans [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_sym [abbreviation, in mathcomp.ssreflect.seq]
-perm_eq_refl [abbreviation, in mathcomp.ssreflect.seq]
-perm_eqlE [abbreviation, in mathcomp.ssreflect.seq]
-perm_eqrP [abbreviation, in mathcomp.ssreflect.seq]
-perm_eqlP [abbreviation, in mathcomp.ssreflect.seq]
-perm_eqP [abbreviation, in mathcomp.ssreflect.seq]
-perm_permutations [lemma, in mathcomp.ssreflect.seq]
-perm_count_undup [lemma, in mathcomp.ssreflect.seq]
-perm_tseq [abbreviation, in mathcomp.ssreflect.seq]
-perm_tally_seq [lemma, in mathcomp.ssreflect.seq]
-perm_tally [lemma, in mathcomp.ssreflect.seq]
-perm_flatten [lemma, in mathcomp.ssreflect.seq]
-perm_sumn [lemma, in mathcomp.ssreflect.seq]
-perm_iotaP [lemma, in mathcomp.ssreflect.seq]
-perm_pmap [lemma, in mathcomp.ssreflect.seq]
-perm_map_inj [lemma, in mathcomp.ssreflect.seq]
-perm_map [lemma, in mathcomp.ssreflect.seq]
-perm_to_subseq [lemma, in mathcomp.ssreflect.seq]
-perm_to_rem [lemma, in mathcomp.ssreflect.seq]
-perm_eqr [abbreviation, in mathcomp.ssreflect.seq]
-perm_eql [abbreviation, in mathcomp.ssreflect.seq]
-perm_undup [lemma, in mathcomp.ssreflect.seq]
-perm_uniq [lemma, in mathcomp.ssreflect.seq]
-perm_small_eq [lemma, in mathcomp.ssreflect.seq]
-perm_all [lemma, in mathcomp.ssreflect.seq]
-perm_has [lemma, in mathcomp.ssreflect.seq]
-perm_consP [lemma, in mathcomp.ssreflect.seq]
-perm_nilP [lemma, in mathcomp.ssreflect.seq]
-perm_mem [lemma, in mathcomp.ssreflect.seq]
-perm_size [lemma, in mathcomp.ssreflect.seq]
-perm_filterC [lemma, in mathcomp.ssreflect.seq]
-perm_filter [lemma, in mathcomp.ssreflect.seq]
-perm_rev [lemma, in mathcomp.ssreflect.seq]
-perm_rotr [lemma, in mathcomp.ssreflect.seq]
-perm_rot [lemma, in mathcomp.ssreflect.seq]
-perm_rcons [lemma, in mathcomp.ssreflect.seq]
-perm_catCA [lemma, in mathcomp.ssreflect.seq]
-perm_catAC [lemma, in mathcomp.ssreflect.seq]
-perm_cat [lemma, in mathcomp.ssreflect.seq]
-perm_catr [lemma, in mathcomp.ssreflect.seq]
-perm_cat2r [lemma, in mathcomp.ssreflect.seq]
-perm_cons [lemma, in mathcomp.ssreflect.seq]
-perm_catl [lemma, in mathcomp.ssreflect.seq]
-perm_cat2l [lemma, in mathcomp.ssreflect.seq]
-perm_catC [lemma, in mathcomp.ssreflect.seq]
-perm_eqr [abbreviation, in mathcomp.ssreflect.seq]
-perm_eql [abbreviation, in mathcomp.ssreflect.seq]
-perm_trans [lemma, in mathcomp.ssreflect.seq]
-perm_sym [lemma, in mathcomp.ssreflect.seq]
-perm_refl [lemma, in mathcomp.ssreflect.seq]
-perm_eq [definition, in mathcomp.ssreflect.seq]
-perm_faithful [lemma, in mathcomp.fingroup.action]
-perm_act1P [lemma, in mathcomp.fingroup.action]
-perm_mact [lemma, in mathcomp.fingroup.action]
-perm_big [lemma, in mathcomp.ssreflect.bigop]
-perm1 [lemma, in mathcomp.fingroup.perm]
-PervasiveMonoids [section, in mathcomp.ssreflect.bigop]
-pexpIrz [lemma, in mathcomp.algebra.ssrint]
-pexprz_eq1 [lemma, in mathcomp.algebra.ssrint]
-Pextraspecial [module, in mathcomp.solvable.extraspecial]
-Pextraspecial.act [definition, in mathcomp.solvable.extraspecial]
-Pextraspecial.actP [lemma, in mathcomp.solvable.extraspecial]
-Pextraspecial.Construction [section, in mathcomp.solvable.extraspecial]
-Pextraspecial.Construction.p [variable, in mathcomp.solvable.extraspecial]
-Pextraspecial.gactP [lemma, in mathcomp.solvable.extraspecial]
-Pextraspecial.groupAction [definition, in mathcomp.solvable.extraspecial]
-Pextraspecial.gtype [definition, in mathcomp.solvable.extraspecial]
-Pextraspecial.gtype_key [lemma, in mathcomp.solvable.extraspecial]
-Pextraspecial.ngtype [definition, in mathcomp.solvable.extraspecial]
-Pextraspecial.ngtypeQ [definition, in mathcomp.solvable.extraspecial]
-pfactor [definition, in mathcomp.ssreflect.prime]
-pfactorK [lemma, in mathcomp.ssreflect.prime]
-pfactorKpdiv [lemma, in mathcomp.ssreflect.prime]
-pfactor_coprime [lemma, in mathcomp.ssreflect.prime]
-pfactor_dvdnn [lemma, in mathcomp.ssreflect.prime]
-pfactor_dvdn [lemma, in mathcomp.ssreflect.prime]
-pfactor_gt0 [lemma, in mathcomp.ssreflect.prime]
-pfamily [abbreviation, in mathcomp.ssreflect.finfun]
-pfamilyP [lemma, in mathcomp.ssreflect.finfun]
-pfamily_mem [definition, in mathcomp.ssreflect.finfun]
-pffun_on [abbreviation, in mathcomp.ssreflect.finfun]
-pffun_onP [lemma, in mathcomp.ssreflect.finfun]
-pffun_on_mem [definition, in mathcomp.ssreflect.finfun]
-pFtoE [abbreviation, in mathcomp.algebra.polyXY]
-pgroup [definition, in mathcomp.solvable.pgroup]
-pgroup [library]
-PgroupDefs [section, in mathcomp.solvable.pgroup]
-PgroupDefs.gT [variable, in mathcomp.solvable.pgroup]
-pgroupE [lemma, in mathcomp.solvable.pgroup]
-pgroupJ [lemma, in mathcomp.solvable.pgroup]
-pgroupM [lemma, in mathcomp.solvable.pgroup]
-pgroupNK [lemma, in mathcomp.solvable.pgroup]
-pgroupP [lemma, in mathcomp.solvable.pgroup]
-PgroupProps [section, in mathcomp.solvable.pgroup]
-PgroupProps.gT [variable, in mathcomp.solvable.pgroup]
-pgroupS [lemma, in mathcomp.solvable.pgroup]
-pgroup_pdiv [lemma, in mathcomp.solvable.pgroup]
-pgroup_p [lemma, in mathcomp.solvable.pgroup]
-pgroup_pi [lemma, in mathcomp.solvable.pgroup]
-pgroup_cyclic_faithful [lemma, in mathcomp.character.character]
-pgroup_sol [lemma, in mathcomp.solvable.sylow]
-pgroup_nil [lemma, in mathcomp.solvable.sylow]
-pgroup_fix_mod [lemma, in mathcomp.solvable.sylow]
-pgroup1 [lemma, in mathcomp.solvable.pgroup]
-pHall [definition, in mathcomp.solvable.pgroup]
-pHallE [lemma, in mathcomp.solvable.pgroup]
-pHallJ [lemma, in mathcomp.solvable.pgroup]
-pHallJnorm [lemma, in mathcomp.solvable.pgroup]
-pHallJ2 [lemma, in mathcomp.solvable.pgroup]
-pHallNK [lemma, in mathcomp.solvable.pgroup]
-pHallP [lemma, in mathcomp.solvable.pgroup]
-pHall_id [lemma, in mathcomp.solvable.pgroup]
-pHall_subl [lemma, in mathcomp.solvable.pgroup]
-pHall_Hall [lemma, in mathcomp.solvable.pgroup]
-pHall_pgroup [lemma, in mathcomp.solvable.pgroup]
-pHall_sub [lemma, in mathcomp.solvable.pgroup]
-PhiJ [lemma, in mathcomp.solvable.maximal]
-PhiS [lemma, in mathcomp.solvable.maximal]
-Phi_mulg [lemma, in mathcomp.solvable.maximal]
-Phi_cprod [lemma, in mathcomp.solvable.maximal]
-Phi_min [lemma, in mathcomp.solvable.maximal]
-Phi_Mho [lemma, in mathcomp.solvable.maximal]
-Phi_joing [lemma, in mathcomp.solvable.maximal]
-Phi_quotient_abelem [lemma, in mathcomp.solvable.maximal]
-Phi_quotient_cyclic [lemma, in mathcomp.solvable.maximal]
-Phi_quotient_id [lemma, in mathcomp.solvable.maximal]
-Phi_normal [lemma, in mathcomp.solvable.maximal]
-Phi_char [lemma, in mathcomp.solvable.maximal]
-Phi_nongen [lemma, in mathcomp.solvable.maximal]
-Phi_proper [lemma, in mathcomp.solvable.maximal]
-Phi_sub_max [lemma, in mathcomp.solvable.maximal]
-Phi_sub [lemma, in mathcomp.solvable.maximal]
-Pi [module, in mathcomp.ssreflect.generic_quotient]
-PiAdditive [section, in mathcomp.algebra.ring_quotient]
-PiAdditive.equivV [variable, in mathcomp.algebra.ring_quotient]
-PiAdditive.Q [variable, in mathcomp.algebra.ring_quotient]
-PiAdditive.V [variable, in mathcomp.algebra.ring_quotient]
-PiAdditive.zeroV [variable, in mathcomp.algebra.ring_quotient]
-Pick [constructor, in mathcomp.ssreflect.fintype]
-pick [definition, in mathcomp.ssreflect.fintype]
-pickle [definition, in mathcomp.ssreflect.choice]
-pickleK [lemma, in mathcomp.ssreflect.choice]
-pickleK_inv [lemma, in mathcomp.ssreflect.choice]
-pickle_taggedK [lemma, in mathcomp.ssreflect.choice]
-pickle_tagged [definition, in mathcomp.ssreflect.choice]
-pickle_seqK [lemma, in mathcomp.ssreflect.choice]
-pickle_seq [definition, in mathcomp.ssreflect.choice]
-pickle_invK [lemma, in mathcomp.ssreflect.choice]
-pickle_inv [definition, in mathcomp.ssreflect.choice]
-pickP [lemma, in mathcomp.ssreflect.fintype]
-pick_spec [inductive, in mathcomp.ssreflect.fintype]
-pick_true [definition, in mathcomp.ssreflect.fintype]
-PiConst [abbreviation, in mathcomp.ssreflect.generic_quotient]
-pid_mx_id [lemma, in mathcomp.algebra.matrix]
-pid_mx_minh [lemma, in mathcomp.algebra.matrix]
-pid_mx_minv [lemma, in mathcomp.algebra.matrix]
-pid_mx_block [lemma, in mathcomp.algebra.matrix]
-pid_mx_col [lemma, in mathcomp.algebra.matrix]
-pid_mx_row [lemma, in mathcomp.algebra.matrix]
-pid_mx_1 [lemma, in mathcomp.algebra.matrix]
-pid_mx_0 [lemma, in mathcomp.algebra.matrix]
-pid_mx [definition, in mathcomp.algebra.matrix]
-pid_mx_key [lemma, in mathcomp.algebra.matrix]
-piE [abbreviation, in mathcomp.ssreflect.generic_quotient]
-PiEmbed [abbreviation, in mathcomp.ssreflect.generic_quotient]
-PiMono1 [abbreviation, in mathcomp.ssreflect.generic_quotient]
-PiMono2 [abbreviation, in mathcomp.ssreflect.generic_quotient]
-PiMorph [abbreviation, in mathcomp.ssreflect.generic_quotient]
-PiMorph1 [abbreviation, in mathcomp.ssreflect.generic_quotient]
-PiMorph11 [abbreviation, in mathcomp.ssreflect.generic_quotient]
-PiMorph2 [abbreviation, in mathcomp.ssreflect.generic_quotient]
-pinvmx [definition, in mathcomp.algebra.mxalgebra]
-piOhm1 [lemma, in mathcomp.solvable.abelian]
-piP [lemma, in mathcomp.ssreflect.generic_quotient]
-PiRMorphism [section, in mathcomp.algebra.ring_quotient]
-PiRMorphism.equivR [variable, in mathcomp.algebra.ring_quotient]
-PiRMorphism.Q [variable, in mathcomp.algebra.ring_quotient]
-PiRMorphism.R [variable, in mathcomp.algebra.ring_quotient]
-PiRMorphism.zeroR [variable, in mathcomp.algebra.ring_quotient]
-piSg [lemma, in mathcomp.fingroup.fingroup]
-PiSig [module, in mathcomp.ssreflect.generic_quotient]
-PiSig.E [axiom, in mathcomp.ssreflect.generic_quotient]
-PiSig.f [axiom, in mathcomp.ssreflect.generic_quotient]
-PiSpec [constructor, in mathcomp.ssreflect.generic_quotient]
-pi_p'group [lemma, in mathcomp.solvable.pgroup]
-pi_pgroup [lemma, in mathcomp.solvable.pgroup]
-pi_subfext_inv [lemma, in mathcomp.field.fieldext]
-pi_subfext_mul [lemma, in mathcomp.field.fieldext]
-pi_subfext_opp [lemma, in mathcomp.field.fieldext]
-pi_subfext_add [lemma, in mathcomp.field.fieldext]
-pi_subfx_inj [lemma, in mathcomp.field.fieldext]
-pi_p'nat [lemma, in mathcomp.ssreflect.prime]
-pi_pnat [lemma, in mathcomp.ssreflect.prime]
-pi_of_prime [lemma, in mathcomp.ssreflect.prime]
-pi_of_exp [lemma, in mathcomp.ssreflect.prime]
-pi_of_part [lemma, in mathcomp.ssreflect.prime]
-pi_ofM [lemma, in mathcomp.ssreflect.prime]
-pi_of_dvd [lemma, in mathcomp.ssreflect.prime]
-pi_max_pdiv [lemma, in mathcomp.ssreflect.prime]
-pi_pdiv [lemma, in mathcomp.ssreflect.prime]
-pi_of [definition, in mathcomp.ssreflect.prime]
-pi_arg [definition, in mathcomp.ssreflect.prime]
-pi_invr [lemma, in mathcomp.algebra.ring_quotient]
-pi_unitr [lemma, in mathcomp.algebra.ring_quotient]
-pi_is_multiplicative [lemma, in mathcomp.algebra.ring_quotient]
-pi_mulr [lemma, in mathcomp.algebra.ring_quotient]
-pi_oner [lemma, in mathcomp.algebra.ring_quotient]
-pi_is_additive [lemma, in mathcomp.algebra.ring_quotient]
-pi_addr [lemma, in mathcomp.algebra.ring_quotient]
-pi_oppr [lemma, in mathcomp.algebra.ring_quotient]
-pi_zeror [lemma, in mathcomp.algebra.ring_quotient]
-pi_eq_quot [lemma, in mathcomp.ssreflect.generic_quotient]
-pi_eq_quot_mixin [projection, in mathcomp.ssreflect.generic_quotient]
-pi_morph11 [lemma, in mathcomp.ssreflect.generic_quotient]
-pi_mono2 [lemma, in mathcomp.ssreflect.generic_quotient]
-pi_mono1 [lemma, in mathcomp.ssreflect.generic_quotient]
-pi_morph2 [lemma, in mathcomp.ssreflect.generic_quotient]
-pi_morph1 [lemma, in mathcomp.ssreflect.generic_quotient]
-pi_spec [inductive, in mathcomp.ssreflect.generic_quotient]
-pi_phant [definition, in mathcomp.ssreflect.generic_quotient]
-pi_of_exponent [lemma, in mathcomp.solvable.abelian]
-pi_center_nilpotent [lemma, in mathcomp.solvable.sylow]
-pi'_p'group [lemma, in mathcomp.solvable.pgroup]
-pi'_p'nat [lemma, in mathcomp.ssreflect.prime]
-Pi.E [definition, in mathcomp.ssreflect.generic_quotient]
-Pi.f [definition, in mathcomp.ssreflect.generic_quotient]
-plusE [lemma, in mathcomp.ssreflect.ssrnat]
-pmap [definition, in mathcomp.ssreflect.seq]
-Pmap [section, in mathcomp.ssreflect.seq]
-PmapSub [section, in mathcomp.ssreflect.seq]
-PmapSub.p [variable, in mathcomp.ssreflect.seq]
-PmapSub.sT [variable, in mathcomp.ssreflect.seq]
-PmapSub.T [variable, in mathcomp.ssreflect.seq]
-pmapS_filter [lemma, in mathcomp.ssreflect.seq]
-pmap_sub_uniq [lemma, in mathcomp.ssreflect.seq]
-pmap_uniq [lemma, in mathcomp.ssreflect.seq]
-pmap_cat [lemma, in mathcomp.ssreflect.seq]
-pmap_filter [lemma, in mathcomp.ssreflect.seq]
-Pmap.aT [variable, in mathcomp.ssreflect.seq]
-Pmap.f [variable, in mathcomp.ssreflect.seq]
-Pmap.fK [variable, in mathcomp.ssreflect.seq]
-Pmap.g [variable, in mathcomp.ssreflect.seq]
-Pmap.rT [variable, in mathcomp.ssreflect.seq]
-PMax [section, in mathcomp.solvable.maximal]
-pmaxElem [definition, in mathcomp.solvable.abelian]
-pmaxElemJ [lemma, in mathcomp.solvable.abelian]
-pmaxElemP [lemma, in mathcomp.solvable.abelian]
-pmaxElemS [lemma, in mathcomp.solvable.abelian]
-pmaxElem_LdivP [lemma, in mathcomp.solvable.abelian]
-pmaxElem_exists [lemma, in mathcomp.solvable.abelian]
-pmaxElem_extraspecial [lemma, in mathcomp.solvable.maximal]
-PMax.gT [variable, in mathcomp.solvable.maximal]
-PMax.M [variable, in mathcomp.solvable.maximal]
-PMax.P [variable, in mathcomp.solvable.maximal]
-PMax.p [variable, in mathcomp.solvable.maximal]
-PMax.pP [variable, in mathcomp.solvable.maximal]
-pmorphimF [lemma, in mathcomp.solvable.gfunctor]
-pmorphim_pHall [lemma, in mathcomp.solvable.pgroup]
-pmorphim_pgroup [lemma, in mathcomp.solvable.pgroup]
-pmulrn [lemma, in mathcomp.algebra.ssrint]
-pmulrz_rle0 [lemma, in mathcomp.algebra.ssrint]
-pmulrz_rge0 [lemma, in mathcomp.algebra.ssrint]
-pmulrz_rlt0 [lemma, in mathcomp.algebra.ssrint]
-pmulrz_rgt0 [lemma, in mathcomp.algebra.ssrint]
-pmulrz_lle0 [lemma, in mathcomp.algebra.ssrint]
-pmulrz_lge0 [lemma, in mathcomp.algebra.ssrint]
-pmulrz_llt0 [lemma, in mathcomp.algebra.ssrint]
-pmulrz_lgt0 [lemma, in mathcomp.algebra.ssrint]
-pnat [definition, in mathcomp.ssreflect.prime]
-pnatE [lemma, in mathcomp.ssreflect.prime]
-pnatI [lemma, in mathcomp.ssreflect.prime]
-pnatNK [lemma, in mathcomp.ssreflect.prime]
-pnatP [lemma, in mathcomp.ssreflect.prime]
-pnatPpi [lemma, in mathcomp.ssreflect.prime]
-PnatTheory [section, in mathcomp.ssreflect.prime]
-pnat_1 [lemma, in mathcomp.ssreflect.prime]
-pnat_coprime [lemma, in mathcomp.ssreflect.prime]
-pnat_div [lemma, in mathcomp.ssreflect.prime]
-pnat_dvd [lemma, in mathcomp.ssreflect.prime]
-pnat_pi [lemma, in mathcomp.ssreflect.prime]
-pnat_id [lemma, in mathcomp.ssreflect.prime]
-pnat_exp [lemma, in mathcomp.ssreflect.prime]
-pnat_mul [lemma, in mathcomp.ssreflect.prime]
-pnat_exponent [lemma, in mathcomp.solvable.abelian]
-pnElem [definition, in mathcomp.solvable.abelian]
-pnElemE [lemma, in mathcomp.solvable.abelian]
-pnElemI [lemma, in mathcomp.solvable.abelian]
-pnElemJ [lemma, in mathcomp.solvable.abelian]
-pnElemP [lemma, in mathcomp.solvable.abelian]
-pnElemPcard [lemma, in mathcomp.solvable.abelian]
-pnElemS [lemma, in mathcomp.solvable.abelian]
-pnElem_prime [lemma, in mathcomp.solvable.abelian]
-pnElem0 [lemma, in mathcomp.solvable.abelian]
-poly [definition, in mathcomp.algebra.poly]
-Poly [definition, in mathcomp.algebra.poly]
-poly [library]
-polyC [definition, in mathcomp.algebra.poly]
-polyCK [lemma, in mathcomp.algebra.poly]
-PolyCompose [section, in mathcomp.algebra.poly]
-PolyCompose.R [variable, in mathcomp.algebra.poly]
-_ \Po _ (ring_scope) [notation, in mathcomp.algebra.poly]
-polyC_inv [lemma, in mathcomp.algebra.poly]
-polyC_exp [lemma, in mathcomp.algebra.poly]
-polyC_multiplicative [lemma, in mathcomp.algebra.poly]
-polyC_mul [lemma, in mathcomp.algebra.poly]
-polyC_muln [lemma, in mathcomp.algebra.poly]
-polyC_sub [lemma, in mathcomp.algebra.poly]
-polyC_opp [lemma, in mathcomp.algebra.poly]
-polyC_add [lemma, in mathcomp.algebra.poly]
-polyC_eq0 [lemma, in mathcomp.algebra.poly]
-polyC_inj [lemma, in mathcomp.algebra.poly]
-polyC_mulrz [lemma, in mathcomp.algebra.ssrint]
-polyC0 [lemma, in mathcomp.algebra.poly]
-polyC1 [lemma, in mathcomp.algebra.poly]
-polydiv [library]
-PolyK [lemma, in mathcomp.algebra.poly]
-polynomial [record, in mathcomp.algebra.poly]
-Polynomial [constructor, in mathcomp.algebra.poly]
-Polynomial [section, in mathcomp.algebra.poly]
-PolynomialComRing [section, in mathcomp.algebra.poly]
-PolynomialComRing.R [variable, in mathcomp.algebra.poly]
-PolynomialIdomain [section, in mathcomp.algebra.poly]
-PolynomialIdomain.R [variable, in mathcomp.algebra.poly]
-PolynomialTheory [section, in mathcomp.algebra.poly]
-PolynomialTheory.OnePrimitive [section, in mathcomp.algebra.poly]
-PolynomialTheory.OnePrimitive.n [variable, in mathcomp.algebra.poly]
-PolynomialTheory.OnePrimitive.n_gt0 [variable, in mathcomp.algebra.poly]
-PolynomialTheory.OnePrimitive.prim_z [variable, in mathcomp.algebra.poly]
-PolynomialTheory.OnePrimitive.z [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverAdd [section, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverAdd.addS [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverAdd.kS [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverAdd.S [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverRing [section, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverRing.kS [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverRing.ringS [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverRing.S [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverSemiring [section, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverSemiring.kS [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverSemiring.ringS [variable, in mathcomp.algebra.poly]
-PolynomialTheory.PolyOverSemiring.S [variable, in mathcomp.algebra.poly]
-PolynomialTheory.R [variable, in mathcomp.algebra.poly]
-_ ^`N ( _ ) (ring_scope) [notation, in mathcomp.algebra.poly]
-_ ^` ( _ ) (ring_scope) [notation, in mathcomp.algebra.poly]
-_ .-primitive_root (ring_scope) [notation, in mathcomp.algebra.poly]
-_ .-unity_root (ring_scope) [notation, in mathcomp.algebra.poly]
-_ .[ _ ] (ring_scope) [notation, in mathcomp.algebra.poly]
-_ ^` [notation, in mathcomp.algebra.poly]
-_ %:P [notation, in mathcomp.algebra.poly]
-'X [notation, in mathcomp.algebra.poly]
-'X^ _ [notation, in mathcomp.algebra.poly]
-\poly_ ( _ < _ ) _ [notation, in mathcomp.algebra.poly]
-polynomial_choiceMixin [definition, in mathcomp.algebra.poly]
-polynomial_eqMixin [definition, in mathcomp.algebra.poly]
-Polynomial.R [variable, in mathcomp.algebra.poly]
-polyOver [definition, in mathcomp.algebra.poly]
-polyOverC [lemma, in mathcomp.algebra.poly]
-polyOverNr [lemma, in mathcomp.algebra.poly]
-polyOverP [lemma, in mathcomp.algebra.poly]
-polyOverS [lemma, in mathcomp.algebra.poly]
-polyOverSv [lemma, in mathcomp.field.fieldext]
-polyOverX [lemma, in mathcomp.algebra.poly]
-polyOverXsubC [lemma, in mathcomp.algebra.poly]
-polyOverZ [lemma, in mathcomp.algebra.poly]
-polyOver_subvs [lemma, in mathcomp.field.fieldext]
-polyOver_dvdzP [lemma, in mathcomp.algebra.intdiv]
-polyOver_comp [lemma, in mathcomp.algebra.poly]
-polyOver_nderivn [lemma, in mathcomp.algebra.poly]
-polyOver_derivn [lemma, in mathcomp.algebra.poly]
-polyOver_deriv [lemma, in mathcomp.algebra.poly]
-polyOver_mulr_closed [lemma, in mathcomp.algebra.poly]
-polyOver_addr_closed [lemma, in mathcomp.algebra.poly]
-polyOver_poly [lemma, in mathcomp.algebra.poly]
-polyOver_key [lemma, in mathcomp.algebra.poly]
-polyOver0 [lemma, in mathcomp.algebra.poly]
-polyOver1P [lemma, in mathcomp.field.falgebra]
-polyP [lemma, in mathcomp.algebra.poly]
-polyseq [projection, in mathcomp.algebra.poly]
-polyseqC [lemma, in mathcomp.algebra.poly]
-polyseqK [lemma, in mathcomp.algebra.poly]
-polyseqMX [lemma, in mathcomp.algebra.poly]
-polyseqMXn [lemma, in mathcomp.algebra.poly]
-polyseqX [lemma, in mathcomp.algebra.poly]
-polyseqXn [lemma, in mathcomp.algebra.poly]
-polyseqXsubC [lemma, in mathcomp.algebra.poly]
-polyseq_poly [lemma, in mathcomp.algebra.poly]
-polyseq_cons [lemma, in mathcomp.algebra.poly]
-polyseq0 [lemma, in mathcomp.algebra.poly]
-polyseq1 [lemma, in mathcomp.algebra.poly]
-polySpred [lemma, in mathcomp.algebra.poly]
-polyX [definition, in mathcomp.algebra.poly]
-polyXsubC_eq0 [lemma, in mathcomp.algebra.poly]
-polyXY [library]
-PolyXY_Field.FtoE [variable, in mathcomp.algebra.polyXY]
-PolyXY_Field.E [variable, in mathcomp.algebra.polyXY]
-PolyXY_Field.F [variable, in mathcomp.algebra.polyXY]
-PolyXY_Field [section, in mathcomp.algebra.polyXY]
-PolyXY_Idomain.R [variable, in mathcomp.algebra.polyXY]
-PolyXY_Idomain [section, in mathcomp.algebra.polyXY]
-PolyXY_ComRing.R [variable, in mathcomp.algebra.polyXY]
-PolyXY_ComRing [section, in mathcomp.algebra.polyXY]
-PolyXY_Ring.R [variable, in mathcomp.algebra.polyXY]
-PolyXY_Ring [section, in mathcomp.algebra.polyXY]
-polyX_eq0 [lemma, in mathcomp.algebra.poly]
-polyX_key [lemma, in mathcomp.algebra.poly]
-polyX_def [definition, in mathcomp.algebra.poly]
-PolyZintOIdom [section, in mathcomp.algebra.ssrint]
-PolyZintOIdom.R [variable, in mathcomp.algebra.ssrint]
-PolyZintRing [section, in mathcomp.algebra.ssrint]
-PolyZintRing.R [variable, in mathcomp.algebra.ssrint]
-poly_square_freeP [lemma, in mathcomp.field.separable]
-poly_rV_is_linear [lemma, in mathcomp.algebra.mxpoly]
-poly_rV_K [lemma, in mathcomp.algebra.mxpoly]
-poly_rV [definition, in mathcomp.algebra.mxpoly]
-poly_XmY_eq0 [lemma, in mathcomp.algebra.polyXY]
-poly_XaY_eq0 [lemma, in mathcomp.algebra.polyXY]
-poly_XmY0 [lemma, in mathcomp.algebra.polyXY]
-poly_XaY0 [lemma, in mathcomp.algebra.polyXY]
-poly_XmY [definition, in mathcomp.algebra.polyXY]
-poly_XaY [definition, in mathcomp.algebra.polyXY]
-poly_invE [lemma, in mathcomp.algebra.poly]
-poly_unitE [lemma, in mathcomp.algebra.poly]
-poly_comUnitMixin [definition, in mathcomp.algebra.poly]
-poly_inv_out [lemma, in mathcomp.algebra.poly]
-poly_intro_unit [lemma, in mathcomp.algebra.poly]
-poly_mulVp [lemma, in mathcomp.algebra.poly]
-poly_inv [definition, in mathcomp.algebra.poly]
-poly_unit [definition, in mathcomp.algebra.poly]
-poly_idomainAxiom [lemma, in mathcomp.algebra.poly]
-poly_mul_comm [lemma, in mathcomp.algebra.poly]
-poly_initial [lemma, in mathcomp.algebra.poly]
-poly_morphX_comm [lemma, in mathcomp.algebra.poly]
-poly_def [lemma, in mathcomp.algebra.poly]
-poly_ind [lemma, in mathcomp.algebra.poly]
-poly_lmodMixin [definition, in mathcomp.algebra.poly]
-poly_ringMixin [definition, in mathcomp.algebra.poly]
-poly_zmodMixin [definition, in mathcomp.algebra.poly]
-poly_key [lemma, in mathcomp.algebra.poly]
-poly_expanded_def [definition, in mathcomp.algebra.poly]
-poly_nil [definition, in mathcomp.algebra.poly]
-poly_countMixin [definition, in mathcomp.algebra.poly]
-poly_of [definition, in mathcomp.algebra.poly]
-poly_inj [lemma, in mathcomp.algebra.poly]
-poly0Vpos [lemma, in mathcomp.algebra.poly]
-poly1_neq0 [lemma, in mathcomp.algebra.poly]
-poly2_root [lemma, in mathcomp.algebra.poly]
-pop_succn [definition, in mathcomp.ssreflect.ssrnat]
-PosNotEq0 [constructor, in mathcomp.ssreflect.ssrnat]
-posnP [lemma, in mathcomp.ssreflect.ssrnat]
-Posz [constructor, in mathcomp.algebra.ssrint]
-PoszD [lemma, in mathcomp.algebra.ssrint]
-PoszM [lemma, in mathcomp.algebra.ssrint]
-pos_of_nat [definition, in mathcomp.ssreflect.ssrnat]
-powerset [definition, in mathcomp.ssreflect.finset]
-powersetCE [lemma, in mathcomp.ssreflect.finset]
-powersetE [lemma, in mathcomp.ssreflect.finset]
-powersetI [lemma, in mathcomp.ssreflect.finset]
-powersetS [lemma, in mathcomp.ssreflect.finset]
-powersetT [lemma, in mathcomp.ssreflect.finset]
-powerset0 [lemma, in mathcomp.ssreflect.finset]
-powerset1 [lemma, in mathcomp.ssreflect.finset]
-powers_mx [definition, in mathcomp.algebra.mxpoly]
-pprod [abbreviation, in mathcomp.fingroup.gproduct]
-pprod [abbreviation, in mathcomp.fingroup.gproduct]
-pprodE [lemma, in mathcomp.fingroup.gproduct]
-pprodEY [lemma, in mathcomp.fingroup.gproduct]
-pprodg1 [lemma, in mathcomp.fingroup.gproduct]
-pprodJ [lemma, in mathcomp.fingroup.gproduct]
-pprodm [definition, in mathcomp.fingroup.gproduct]
-pprodmE [lemma, in mathcomp.fingroup.gproduct]
-pprodmEl [lemma, in mathcomp.fingroup.gproduct]
-pprodmEr [lemma, in mathcomp.fingroup.gproduct]
-pprodmM [lemma, in mathcomp.fingroup.gproduct]
-pprodP [lemma, in mathcomp.fingroup.gproduct]
-pprodW [lemma, in mathcomp.fingroup.gproduct]
-pprodWC [lemma, in mathcomp.fingroup.gproduct]
-pprodWY [lemma, in mathcomp.fingroup.gproduct]
-pprod1g [lemma, in mathcomp.fingroup.gproduct]
-pQtoC [abbreviation, in mathcomp.field.algC]
-pQtoC [abbreviation, in mathcomp.field.cyclotomic]
-pQtoC [abbreviation, in mathcomp.field.algnum]
-Pquotient [section, in mathcomp.solvable.pgroup]
-pquotient_pcore [lemma, in mathcomp.solvable.pgroup]
-pquotient_pHall [lemma, in mathcomp.solvable.pgroup]
-pquotient_pgroup [lemma, in mathcomp.solvable.pgroup]
-Pquotient.G [variable, in mathcomp.solvable.pgroup]
-Pquotient.gT [variable, in mathcomp.solvable.pgroup]
-Pquotient.H [variable, in mathcomp.solvable.pgroup]
-Pquotient.K [variable, in mathcomp.solvable.pgroup]
-Pquotient.p [variable, in mathcomp.solvable.pgroup]
-Pquotient.pi [variable, in mathcomp.solvable.pgroup]
-Pquotient.piK [variable, in mathcomp.solvable.pgroup]
-PreClosedField [module, in mathcomp.algebra.poly]
-PreClosedField.closed_nonrootP [lemma, in mathcomp.algebra.poly]
-PreClosedField.closed_rootP [lemma, in mathcomp.algebra.poly]
-PreClosedField.UseAxiom [section, in mathcomp.algebra.poly]
-PreClosedField.UseAxiom.closedF [variable, in mathcomp.algebra.poly]
-PreClosedField.UseAxiom.F [variable, in mathcomp.algebra.poly]
-predC_closed [lemma, in mathcomp.ssreflect.fingraph]
-predC1 [definition, in mathcomp.ssreflect.eqtype]
-predD1 [definition, in mathcomp.ssreflect.eqtype]
-predD1P [lemma, in mathcomp.ssreflect.eqtype]
-Predicates [section, in mathcomp.character.classfun]
-Predicates.D [variable, in mathcomp.character.classfun]
-Predicates.gT [variable, in mathcomp.character.classfun]
-Predicates.R [variable, in mathcomp.character.classfun]
-Predicates.rT [variable, in mathcomp.character.classfun]
-predn [abbreviation, in mathcomp.ssreflect.ssrnat]
-prednK [lemma, in mathcomp.ssreflect.ssrnat]
-predn_exp [lemma, in mathcomp.ssreflect.binomial]
-predn_int [lemma, in mathcomp.algebra.ssrint]
-predOfType [abbreviation, in mathcomp.ssreflect.finset]
-PredType [definition, in mathcomp.ssreflect.ssrbool]
-predT_subset [lemma, in mathcomp.ssreflect.fintype]
-predU1 [definition, in mathcomp.ssreflect.eqtype]
-predU1l [lemma, in mathcomp.ssreflect.eqtype]
-predU1P [lemma, in mathcomp.ssreflect.eqtype]
-predU1r [lemma, in mathcomp.ssreflect.eqtype]
-predX [definition, in mathcomp.ssreflect.eqtype]
-predX_prod_enum [lemma, in mathcomp.ssreflect.fintype]
-pred_of_vspace [definition, in mathcomp.algebra.vector]
-pred_of_itv [definition, in mathcomp.algebra.interval]
-pred_Nirr [definition, in mathcomp.character.character]
-pred_of_set [abbreviation, in mathcomp.ssreflect.finset]
-pred_of_set_def [abbreviation, in mathcomp.ssreflect.finset]
-pred0b [definition, in mathcomp.ssreflect.fintype]
-pred0P [lemma, in mathcomp.ssreflect.fintype]
-pred0Pn [lemma, in mathcomp.ssreflect.fintype]
-pred1 [definition, in mathcomp.ssreflect.eqtype]
-pred1E [lemma, in mathcomp.ssreflect.eqtype]
-pred2 [definition, in mathcomp.ssreflect.eqtype]
-pred2P [lemma, in mathcomp.ssreflect.eqtype]
-pred3 [definition, in mathcomp.ssreflect.eqtype]
-pred4 [definition, in mathcomp.ssreflect.eqtype]
-prefix_subseq [lemma, in mathcomp.ssreflect.seq]
-PreGroupIdentities [section, in mathcomp.fingroup.fingroup]
-PreGroupIdentities.T [variable, in mathcomp.fingroup.fingroup]
-preimset [definition, in mathcomp.ssreflect.finset]
-preimsetC [lemma, in mathcomp.ssreflect.finset]
-preimsetD [lemma, in mathcomp.ssreflect.finset]
-preimsetI [lemma, in mathcomp.ssreflect.finset]
-preimsetS [lemma, in mathcomp.ssreflect.finset]
-preimsetT [lemma, in mathcomp.ssreflect.finset]
-preimsetU [lemma, in mathcomp.ssreflect.finset]
-preimset_proper [lemma, in mathcomp.ssreflect.finset]
-preimset0 [lemma, in mathcomp.ssreflect.finset]
-preim_permV [lemma, in mathcomp.fingroup.perm]
-preim_autE [lemma, in mathcomp.fingroup.automorphism]
-preim_seq [definition, in mathcomp.ssreflect.fintype]
-preim_iinv [lemma, in mathcomp.ssreflect.fintype]
-preim_partition_pblock [lemma, in mathcomp.ssreflect.finset]
-preim_partitionP [lemma, in mathcomp.ssreflect.finset]
-preim_partition [definition, in mathcomp.ssreflect.finset]
-Presentation [module, in mathcomp.fingroup.presentation]
-presentation [library]
-PresentationTheory [section, in mathcomp.fingroup.presentation]
-Presentation.And [constructor, in mathcomp.fingroup.presentation]
-Presentation.and_rel [definition, in mathcomp.fingroup.presentation]
-Presentation.bool_of_rel [definition, in mathcomp.fingroup.presentation]
-Presentation.Cast [definition, in mathcomp.fingroup.presentation]
-Presentation.Comm [constructor, in mathcomp.fingroup.presentation]
-Presentation.Conj [constructor, in mathcomp.fingroup.presentation]
-Presentation.Cst [constructor, in mathcomp.fingroup.presentation]
-Presentation.Env [constructor, in mathcomp.fingroup.presentation]
-Presentation.env [inductive, in mathcomp.fingroup.presentation]
-Presentation.env1 [definition, in mathcomp.fingroup.presentation]
-Presentation.Eq1 [definition, in mathcomp.fingroup.presentation]
-Presentation.Eq2 [constructor, in mathcomp.fingroup.presentation]
-Presentation.Eq3 [definition, in mathcomp.fingroup.presentation]
-Presentation.eval [definition, in mathcomp.fingroup.presentation]
-Presentation.Exp [constructor, in mathcomp.fingroup.presentation]
-Presentation.Formula [constructor, in mathcomp.fingroup.presentation]
-Presentation.formula [inductive, in mathcomp.fingroup.presentation]
-Presentation.Generator [constructor, in mathcomp.fingroup.presentation]
-Presentation.hom [definition, in mathcomp.fingroup.presentation]
-Presentation.Idx [constructor, in mathcomp.fingroup.presentation]
-Presentation.Inv [constructor, in mathcomp.fingroup.presentation]
-Presentation.iso [definition, in mathcomp.fingroup.presentation]
-Presentation.Mul [constructor, in mathcomp.fingroup.presentation]
-Presentation.NoRel [constructor, in mathcomp.fingroup.presentation]
-Presentation.Presentation [section, in mathcomp.fingroup.presentation]
-Presentation.rel [definition, in mathcomp.fingroup.presentation]
-Presentation.Rel [constructor, in mathcomp.fingroup.presentation]
-Presentation.rel_type [inductive, in mathcomp.fingroup.presentation]
-Presentation.sat [definition, in mathcomp.fingroup.presentation]
-Presentation.term [inductive, in mathcomp.fingroup.presentation]
-Presentation.type [inductive, in mathcomp.fingroup.presentation]
-prev [definition, in mathcomp.ssreflect.path]
-prev_map [lemma, in mathcomp.ssreflect.path]
-prev_rev [lemma, in mathcomp.ssreflect.path]
-prev_rotr [lemma, in mathcomp.ssreflect.path]
-prev_rot [lemma, in mathcomp.ssreflect.path]
-prev_next [lemma, in mathcomp.ssreflect.path]
-prev_cycle [lemma, in mathcomp.ssreflect.path]
-prev_nth [lemma, in mathcomp.ssreflect.path]
-prev_at [definition, in mathcomp.ssreflect.path]
-pre_image [lemma, in mathcomp.ssreflect.fintype]
-prime [definition, in mathcomp.ssreflect.prime]
-prime [library]
-PrimeChar [section, in mathcomp.field.finfield]
-PrimeCharType [definition, in mathcomp.field.finfield]
-primeChar_dimf [lemma, in mathcomp.field.finfield]
-primeChar_vectMixin [definition, in mathcomp.field.finfield]
-primeChar_vectAxiom [lemma, in mathcomp.field.finfield]
-primeChar_pgroup [lemma, in mathcomp.field.finfield]
-primeChar_abelem [lemma, in mathcomp.field.finfield]
-primeChar_scaleAr [lemma, in mathcomp.field.finfield]
-primeChar_scaleAl [lemma, in mathcomp.field.finfield]
-primeChar_lmodMixin [definition, in mathcomp.field.finfield]
-primeChar_scaleDl [lemma, in mathcomp.field.finfield]
-primeChar_scaleDr [lemma, in mathcomp.field.finfield]
-primeChar_scale1 [lemma, in mathcomp.field.finfield]
-primeChar_scaleA [lemma, in mathcomp.field.finfield]
-primeChar_scale [definition, in mathcomp.field.finfield]
-PrimeChar.FinField [section, in mathcomp.field.finfield]
-PrimeChar.FinField.charFp [variable, in mathcomp.field.finfield]
-PrimeChar.FinField.F0 [variable, in mathcomp.field.finfield]
-PrimeChar.FinRing [section, in mathcomp.field.finfield]
-PrimeChar.FinRing.charRp [variable, in mathcomp.field.finfield]
-PrimeChar.FinRing.n [variable, in mathcomp.field.finfield]
-PrimeChar.FinRing.pr_p [variable, in mathcomp.field.finfield]
-PrimeChar.FinRing.R0 [variable, in mathcomp.field.finfield]
-PrimeChar.p [variable, in mathcomp.field.finfield]
-PrimeChar.PrimeCharRing [section, in mathcomp.field.finfield]
-PrimeChar.PrimeCharRing.charRp [variable, in mathcomp.field.finfield]
-PrimeChar.PrimeCharRing.natrFp [variable, in mathcomp.field.finfield]
-PrimeChar.PrimeCharRing.R0 [variable, in mathcomp.field.finfield]
-_ *p: _ [notation, in mathcomp.field.finfield]
-PrimeDecompAux [module, in mathcomp.ssreflect.prime]
-PrimeDecompAux.add_totient_factor [definition, in mathcomp.ssreflect.prime]
-PrimeDecompAux.add_divisors [definition, in mathcomp.ssreflect.prime]
-PrimeDecompAux.cons_pfactor [definition, in mathcomp.ssreflect.prime]
-PrimeDecompAux.edivn2 [definition, in mathcomp.ssreflect.prime]
-PrimeDecompAux.edivn2P [lemma, in mathcomp.ssreflect.prime]
-PrimeDecompAux.elogn2 [definition, in mathcomp.ssreflect.prime]
-PrimeDecompAux.elogn2P [lemma, in mathcomp.ssreflect.prime]
-PrimeDecompAux.Elogn2Spec [constructor, in mathcomp.ssreflect.prime]
-PrimeDecompAux.elogn2_spec [inductive, in mathcomp.ssreflect.prime]
-PrimeDecompAux.ifnz [definition, in mathcomp.ssreflect.prime]
-PrimeDecompAux.ifnzP [lemma, in mathcomp.ssreflect.prime]
-PrimeDecompAux.IfnzPos [constructor, in mathcomp.ssreflect.prime]
-PrimeDecompAux.IfnzZero [constructor, in mathcomp.ssreflect.prime]
-PrimeDecompAux.ifnz_spec [inductive, in mathcomp.ssreflect.prime]
-_ ^? _ :: _ (nat_scope) [notation, in mathcomp.ssreflect.prime]
-PrimeField [section, in mathcomp.algebra.zmodp]
-PrimeField.F_prime.p_pr [variable, in mathcomp.algebra.zmodp]
-PrimeField.F_prime [section, in mathcomp.algebra.zmodp]
-PrimeField.p [variable, in mathcomp.algebra.zmodp]
-primeP [lemma, in mathcomp.ssreflect.prime]
-primePn [lemma, in mathcomp.ssreflect.prime]
-primePns [lemma, in mathcomp.ssreflect.prime]
-PrimePowerField [lemma, in mathcomp.field.finfield]
-primes [definition, in mathcomp.ssreflect.prime]
-primes_class_simple_gt1 [lemma, in mathcomp.character.integral_char]
-primes_part [lemma, in mathcomp.ssreflect.prime]
-primes_prime [lemma, in mathcomp.ssreflect.prime]
-primes_exp [lemma, in mathcomp.ssreflect.prime]
-primes_mul [lemma, in mathcomp.ssreflect.prime]
-primes_uniq [lemma, in mathcomp.ssreflect.prime]
-primes_exponent [lemma, in mathcomp.solvable.abelian]
-prime_subgroupVti [lemma, in mathcomp.solvable.pgroup]
-prime_dvd_bin [lemma, in mathcomp.ssreflect.binomial]
-prime_FrobeniusP [lemma, in mathcomp.solvable.frobenius]
-prime_decompE [lemma, in mathcomp.ssreflect.prime]
-prime_above [lemma, in mathcomp.ssreflect.prime]
-prime_coprime [lemma, in mathcomp.ssreflect.prime]
-prime_oddPn [lemma, in mathcomp.ssreflect.prime]
-prime_gt0 [lemma, in mathcomp.ssreflect.prime]
-prime_gt1 [lemma, in mathcomp.ssreflect.prime]
-prime_nt_dvdP [lemma, in mathcomp.ssreflect.prime]
-prime_decomp_correct [lemma, in mathcomp.ssreflect.prime]
-prime_decomp [definition, in mathcomp.ssreflect.prime]
-[ rec _ , _ , _ , _ , _ , _ ] [notation, in mathcomp.ssreflect.prime]
-prime_decomp_rec [definition, in mathcomp.ssreflect.prime]
-prime_decomp [section, in mathcomp.ssreflect.prime]
-prime_idealrM [lemma, in mathcomp.algebra.ring_quotient]
-prime_idealr_zmod [projection, in mathcomp.algebra.ring_quotient]
-prime_idealr [record, in mathcomp.algebra.ring_quotient]
-prime_idealr_closed [definition, in mathcomp.algebra.ring_quotient]
-prime_Ohm1P [lemma, in mathcomp.solvable.extremal]
-prime_invariant_irr_extendible [lemma, in mathcomp.character.inertia]
-prime_abelem [lemma, in mathcomp.solvable.abelian]
-prime_meetG [lemma, in mathcomp.fingroup.fingroup]
-prime_TIg [lemma, in mathcomp.fingroup.fingroup]
-prime_cyclic [lemma, in mathcomp.solvable.cyclic]
-Primitive [section, in mathcomp.solvable.primitive_action]
-primitive [definition, in mathcomp.solvable.primitive_action]
-PrimitiveDef [section, in mathcomp.solvable.primitive_action]
-PrimitiveDef.A [variable, in mathcomp.solvable.primitive_action]
-PrimitiveDef.aT [variable, in mathcomp.solvable.primitive_action]
-PrimitiveDef.S [variable, in mathcomp.solvable.primitive_action]
-PrimitiveDef.sT [variable, in mathcomp.solvable.primitive_action]
-PrimitiveDef.to [variable, in mathcomp.solvable.primitive_action]
-PrimitiveRoots [section, in mathcomp.solvable.cyclic]
-primitive_root_splitting_abelian [lemma, in mathcomp.character.mxrepresentation]
-Primitive_Element_Theorem [lemma, in mathcomp.field.separable]
-primitive_root_of_unity [definition, in mathcomp.algebra.poly]
-primitive_action [library]
-Primitive.aT [variable, in mathcomp.solvable.primitive_action]
-Primitive.G [variable, in mathcomp.solvable.primitive_action]
-Primitive.S [variable, in mathcomp.solvable.primitive_action]
-Primitive.sT [variable, in mathcomp.solvable.primitive_action]
-Primitive.to [variable, in mathcomp.solvable.primitive_action]
-prim_trans_norm [lemma, in mathcomp.solvable.primitive_action]
-prim_rootP [lemma, in mathcomp.algebra.poly]
-prim_root_exp_coprime [lemma, in mathcomp.algebra.poly]
-prim_order_dvd [lemma, in mathcomp.algebra.poly]
-prim_expr_mod [lemma, in mathcomp.algebra.poly]
-prim_expr_order [lemma, in mathcomp.algebra.poly]
-prim_order_gt0 [lemma, in mathcomp.algebra.poly]
-prim_order_exists [lemma, in mathcomp.algebra.poly]
-principal_comp [definition, in mathcomp.character.mxrepresentation]
-principal_comp_def [definition, in mathcomp.character.mxrepresentation]
-principal_comp_key [lemma, in mathcomp.character.mxrepresentation]
-principal_comp_subproof [lemma, in mathcomp.character.mxrepresentation]
-ProdEqType [section, in mathcomp.ssreflect.eqtype]
-ProdEqType.T1 [variable, in mathcomp.ssreflect.eqtype]
-ProdEqType.T2 [variable, in mathcomp.ssreflect.eqtype]
-ProdFinType [section, in mathcomp.ssreflect.fintype]
-ProdFinType.T1 [variable, in mathcomp.ssreflect.fintype]
-ProdFinType.T2 [variable, in mathcomp.ssreflect.fintype]
-ProdMorph [section, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm [section, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm.cfHK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm.eqfHK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm.eqHK_G [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm.fH [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm.fK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm.G [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm.H [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Cprodm.K [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.defs [section, in mathcomp.fingroup.gproduct]
-ProdMorph.defs.A [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.defs.B [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.defs.fA [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.defs.fB [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Dprodm [section, in mathcomp.fingroup.gproduct]
-ProdMorph.Dprodm.cfHK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Dprodm.eqHK_G [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Dprodm.fH [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Dprodm.fK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Dprodm.G [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Dprodm.H [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Dprodm.K [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.gT [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Props [section, in mathcomp.fingroup.gproduct]
-ProdMorph.Props.actf [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Props.eqfHK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Props.fH [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Props.fK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Props.H [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Props.K [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Props.nHK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.rT [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Sdprodm [section, in mathcomp.fingroup.gproduct]
-ProdMorph.Sdprodm.actf [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Sdprodm.eqHK_G [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Sdprodm.fH [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Sdprodm.fK [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Sdprodm.G [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Sdprodm.H [variable, in mathcomp.fingroup.gproduct]
-ProdMorph.Sdprodm.K [variable, in mathcomp.fingroup.gproduct]
-prodMz [lemma, in mathcomp.algebra.ssrint]
-prodn_gt0 [lemma, in mathcomp.ssreflect.bigop]
-prodn_cond_gt0 [lemma, in mathcomp.ssreflect.bigop]
-prodsgP [lemma, in mathcomp.fingroup.fingroup]
-Product [section, in mathcomp.character.classfun]
-Product [section, in mathcomp.solvable.center]
-Product.G [variable, in mathcomp.character.classfun]
-Product.gT [variable, in mathcomp.character.classfun]
-Product.gT [variable, in mathcomp.solvable.center]
-prodv [definition, in mathcomp.field.falgebra]
-prodvA [lemma, in mathcomp.field.falgebra]
-prodvAC [lemma, in mathcomp.field.fieldext]
-prodvC [lemma, in mathcomp.field.fieldext]
-prodvCA [lemma, in mathcomp.field.fieldext]
-prodvDl [lemma, in mathcomp.field.falgebra]
-prodvDr [lemma, in mathcomp.field.falgebra]
-ProdVector [section, in mathcomp.algebra.vector]
-ProdVector.R [variable, in mathcomp.algebra.vector]
-ProdVector.vT1 [variable, in mathcomp.algebra.vector]
-ProdVector.vT2 [variable, in mathcomp.algebra.vector]
-prodvP [lemma, in mathcomp.field.falgebra]
-prodvS [lemma, in mathcomp.field.falgebra]
-prodvSl [lemma, in mathcomp.field.falgebra]
-prodvSr [lemma, in mathcomp.field.falgebra]
-prodv_is_aspace [lemma, in mathcomp.field.fieldext]
-prodv_sub [lemma, in mathcomp.field.falgebra]
-prodv_id [lemma, in mathcomp.field.falgebra]
-prodv_line [lemma, in mathcomp.field.falgebra]
-prodv_key [lemma, in mathcomp.field.falgebra]
-prodv0 [lemma, in mathcomp.field.falgebra]
-prodv1 [lemma, in mathcomp.field.falgebra]
-prod_constt [lemma, in mathcomp.solvable.pgroup]
-prod_tpermP [lemma, in mathcomp.fingroup.perm]
-prod_prime_decomp [lemma, in mathcomp.ssreflect.prime]
-prod_Cyclotomic [lemma, in mathcomp.field.cyclotomic]
-prod_cyclotomic [lemma, in mathcomp.field.cyclotomic]
-prod_repr_lin [lemma, in mathcomp.character.character]
-prod_repr [definition, in mathcomp.character.character]
-prod_mx_repr [lemma, in mathcomp.character.character]
-prod_countMixin [definition, in mathcomp.ssreflect.choice]
-prod_choiceMixin [definition, in mathcomp.ssreflect.choice]
-prod_finMixin [definition, in mathcomp.ssreflect.fintype]
-prod_enumP [lemma, in mathcomp.ssreflect.fintype]
-prod_enum [definition, in mathcomp.ssreflect.fintype]
-prod_cfunE [lemma, in mathcomp.character.classfun]
-prod_nat_const_nat [lemma, in mathcomp.ssreflect.bigop]
-prod_nat_const [lemma, in mathcomp.ssreflect.bigop]
-prod_t_correct [lemma, in mathcomp.solvable.burnside_app]
-prod_tuple [definition, in mathcomp.solvable.burnside_app]
-prod0v [lemma, in mathcomp.field.falgebra]
-prod1v [lemma, in mathcomp.field.falgebra]
-Projection [section, in mathcomp.algebra.vector]
-Projection.K [variable, in mathcomp.algebra.vector]
-Projection.Sumv_Pi.defV [variable, in mathcomp.algebra.vector]
-Projection.Sumv_Pi.V [variable, in mathcomp.algebra.vector]
-Projection.Sumv_Pi.sumv_pi_rec [variable, in mathcomp.algebra.vector]
-Projection.Sumv_Pi.Vs [variable, in mathcomp.algebra.vector]
-Projection.Sumv_Pi.P [variable, in mathcomp.algebra.vector]
-Projection.Sumv_Pi.r0 [variable, in mathcomp.algebra.vector]
-Projection.Sumv_Pi.I [variable, in mathcomp.algebra.vector]
-Projection.Sumv_Pi [section, in mathcomp.algebra.vector]
-Projection.vT [variable, in mathcomp.algebra.vector]
-projv [definition, in mathcomp.algebra.vector]
-projv_proj [lemma, in mathcomp.algebra.vector]
-projv_id [lemma, in mathcomp.algebra.vector]
-proj_mx_hom [lemma, in mathcomp.character.mxrepresentation]
-proj_factmodS [lemma, in mathcomp.character.mxrepresentation]
-proj_mx_proj [lemma, in mathcomp.algebra.mxalgebra]
-proj_mx_0 [lemma, in mathcomp.algebra.mxalgebra]
-proj_mx_id [lemma, in mathcomp.algebra.mxalgebra]
-proj_mx_compl_sub [lemma, in mathcomp.algebra.mxalgebra]
-proj_mx_sub [lemma, in mathcomp.algebra.mxalgebra]
-proj_mx [definition, in mathcomp.algebra.mxalgebra]
-proper [definition, in mathcomp.ssreflect.fintype]
-Proper [section, in mathcomp.field.falgebra]
-properD [lemma, in mathcomp.ssreflect.finset]
-properD1 [lemma, in mathcomp.ssreflect.finset]
-properE [lemma, in mathcomp.ssreflect.fintype]
-properEcard [lemma, in mathcomp.ssreflect.finset]
-properEneq [lemma, in mathcomp.ssreflect.finset]
-properG_ltn_log [lemma, in mathcomp.solvable.pgroup]
-properI [lemma, in mathcomp.ssreflect.finset]
-properIl [lemma, in mathcomp.ssreflect.finset]
-properIr [lemma, in mathcomp.ssreflect.finset]
-properIset [lemma, in mathcomp.ssreflect.finset]
-properJ [lemma, in mathcomp.fingroup.fingroup]
-ProperMxsum [constructor, in mathcomp.algebra.mxalgebra]
-ProperMxsumExpr [constructor, in mathcomp.algebra.mxalgebra]
-properP [lemma, in mathcomp.ssreflect.fintype]
-ProperSumvExpr [constructor, in mathcomp.algebra.vector]
-properT [lemma, in mathcomp.ssreflect.finset]
-PropertiesDefs [section, in mathcomp.solvable.nilpotent]
-PropertiesDefs.A [variable, in mathcomp.solvable.nilpotent]
-PropertiesDefs.gT [variable, in mathcomp.solvable.nilpotent]
-properU [lemma, in mathcomp.ssreflect.finset]
-properUl [lemma, in mathcomp.ssreflect.finset]
-properUr [lemma, in mathcomp.ssreflect.finset]
-properxx [lemma, in mathcomp.ssreflect.fintype]
-proper_addvP [definition, in mathcomp.algebra.vector]
-proper_addv_dim [projection, in mathcomp.algebra.vector]
-proper_addv_val [projection, in mathcomp.algebra.vector]
-proper_addv_expr [record, in mathcomp.algebra.vector]
-proper_ideal [definition, in mathcomp.algebra.ring_quotient]
-proper_irrefl [lemma, in mathcomp.ssreflect.fintype]
-proper_card [lemma, in mathcomp.ssreflect.fintype]
-proper_sub_trans [lemma, in mathcomp.ssreflect.fintype]
-proper_trans [lemma, in mathcomp.ssreflect.fintype]
-proper_subn [lemma, in mathcomp.ssreflect.fintype]
-proper_sub [lemma, in mathcomp.ssreflect.fintype]
-proper_mxsumP [definition, in mathcomp.algebra.mxalgebra]
-proper_mxsum_rank [projection, in mathcomp.algebra.mxalgebra]
-proper_mxsum_val [projection, in mathcomp.algebra.mxalgebra]
-proper_mxsum_expr [record, in mathcomp.algebra.mxalgebra]
-proper_neq [lemma, in mathcomp.ssreflect.finset]
-Proper.aT [variable, in mathcomp.field.falgebra]
-Proper.R [variable, in mathcomp.field.falgebra]
-proper0 [lemma, in mathcomp.ssreflect.finset]
-proper1G [lemma, in mathcomp.fingroup.fingroup]
-proper1set [lemma, in mathcomp.ssreflect.finset]
-pseries [definition, in mathcomp.solvable.pgroup]
-PseriesDefs [section, in mathcomp.solvable.pgroup]
-PseriesDefs.A [variable, in mathcomp.solvable.pgroup]
-PseriesDefs.gT [variable, in mathcomp.solvable.pgroup]
-PseriesDefs.pis [variable, in mathcomp.solvable.pgroup]
-pseriesJ [lemma, in mathcomp.solvable.pgroup]
-pseriesS [lemma, in mathcomp.solvable.pgroup]
-pseries_rcons_id [lemma, in mathcomp.solvable.pgroup]
-pseries_char_catr [lemma, in mathcomp.solvable.pgroup]
-pseries_catr_id [lemma, in mathcomp.solvable.pgroup]
-pseries_char_catl [lemma, in mathcomp.solvable.pgroup]
-pseries_catl_id [lemma, in mathcomp.solvable.pgroup]
-pseries_sub_catr [lemma, in mathcomp.solvable.pgroup]
-pseries_norm2 [lemma, in mathcomp.solvable.pgroup]
-pseries_sub_catl [lemma, in mathcomp.solvable.pgroup]
-pseries_pop2 [lemma, in mathcomp.solvable.pgroup]
-pseries_pop [lemma, in mathcomp.solvable.pgroup]
-pseries_normal [lemma, in mathcomp.solvable.pgroup]
-pseries_char [lemma, in mathcomp.solvable.pgroup]
-pseries_sub [lemma, in mathcomp.solvable.pgroup]
-pseries_subfun [lemma, in mathcomp.solvable.pgroup]
-pseries_rcons [lemma, in mathcomp.solvable.pgroup]
-pseries_group_set [lemma, in mathcomp.solvable.pgroup]
-pseries1 [lemma, in mathcomp.solvable.pgroup]
-psubgroup [definition, in mathcomp.solvable.pgroup]
-psubgroupJ [lemma, in mathcomp.solvable.pgroup]
-psubgroup1 [lemma, in mathcomp.solvable.pgroup]
-pT [abbreviation, in mathcomp.fingroup.perm]
-purely_inseparable_trans [lemma, in mathcomp.field.separable]
-purely_inseparable_refl [lemma, in mathcomp.field.separable]
-purely_inseparableP [lemma, in mathcomp.field.separable]
-purely_inseparable [definition, in mathcomp.field.separable]
-purely_inseparable_elementP [lemma, in mathcomp.field.separable]
-purely_inseparable_element [definition, in mathcomp.field.separable]
-pval [definition, in mathcomp.fingroup.perm]
-pvalE [lemma, in mathcomp.fingroup.perm]
-Px [abbreviation, in mathcomp.field.galois]
-pX1p2id [lemma, in mathcomp.solvable.extraspecial]
-pX1p2n_extraspecial [lemma, in mathcomp.solvable.extraspecial]
-pX1p2n_pgroup [lemma, in mathcomp.solvable.extraspecial]
-pX1p2S [lemma, in mathcomp.solvable.extraspecial]
-pX1p2_extraspecial [lemma, in mathcomp.solvable.extraspecial]
-pX1p2_pgroup [lemma, in mathcomp.solvable.extraspecial]
-pZtoC [abbreviation, in mathcomp.field.algC]
-pZtoC [abbreviation, in mathcomp.field.cyclotomic]
-pZtoC [abbreviation, in mathcomp.field.algnum]
-pZtoQ [abbreviation, in mathcomp.field.algC]
-pZtoQ [abbreviation, in mathcomp.algebra.intdiv]
-pZtoQ [abbreviation, in mathcomp.field.cyclotomic]
-pZtoQ [abbreviation, in mathcomp.field.algnum]
-p_elt_constt [lemma, in mathcomp.solvable.pgroup]
-p_eltNK [lemma, in mathcomp.solvable.pgroup]
-p_eltJ [lemma, in mathcomp.solvable.pgroup]
-p_eltX [lemma, in mathcomp.solvable.pgroup]
-p_eltV [lemma, in mathcomp.solvable.pgroup]
-p_elt1 [lemma, in mathcomp.solvable.pgroup]
-p_eltM [lemma, in mathcomp.solvable.pgroup]
-p_eltM_norm [lemma, in mathcomp.solvable.pgroup]
-p_elt_exp [lemma, in mathcomp.solvable.pgroup]
-p_group1 [lemma, in mathcomp.solvable.pgroup]
-p_Sylow [lemma, in mathcomp.solvable.pgroup]
-p_groupJ [lemma, in mathcomp.solvable.pgroup]
-p_groupP [lemma, in mathcomp.solvable.pgroup]
-p_elt [definition, in mathcomp.solvable.pgroup]
-p_group [definition, in mathcomp.solvable.pgroup]
-p_natP [lemma, in mathcomp.ssreflect.prime]
-p_part_gt1 [lemma, in mathcomp.ssreflect.prime]
-p_part_eq1 [lemma, in mathcomp.ssreflect.prime]
-p_part [lemma, in mathcomp.ssreflect.prime]
-p_A [abbreviation, in mathcomp.algebra.mxpoly]
-p_rank_abelian [lemma, in mathcomp.solvable.abelian]
-p_rank_Ohm1 [lemma, in mathcomp.solvable.abelian]
-p_rank_p'quotient [lemma, in mathcomp.solvable.abelian]
-p_rank_dprod [lemma, in mathcomp.solvable.abelian]
-p_rank_quotient [lemma, in mathcomp.solvable.abelian]
-p_rank_le_rank [lemma, in mathcomp.solvable.abelian]
-p_rank_pmaxElem_exists [lemma, in mathcomp.solvable.abelian]
-p_rank_Hall [lemma, in mathcomp.solvable.abelian]
-p_rank_Sylow [lemma, in mathcomp.solvable.abelian]
-p_rankJ [lemma, in mathcomp.solvable.abelian]
-p_rankElem_max [lemma, in mathcomp.solvable.abelian]
-p_rankS [lemma, in mathcomp.solvable.abelian]
-p_rank_abelem [lemma, in mathcomp.solvable.abelian]
-p_rank_le_logn [lemma, in mathcomp.solvable.abelian]
-p_rank1 [lemma, in mathcomp.solvable.abelian]
-p_rank_gt0 [lemma, in mathcomp.solvable.abelian]
-p_rank_geP [lemma, in mathcomp.solvable.abelian]
-p_rank_witness [lemma, in mathcomp.solvable.abelian]
-p_rank [definition, in mathcomp.solvable.abelian]
-p_abelem_split1 [lemma, in mathcomp.solvable.maximal]
-p_core_Fitting [lemma, in mathcomp.solvable.maximal]
-p_index_maximal [lemma, in mathcomp.solvable.maximal]
-p_maximal_index [lemma, in mathcomp.solvable.maximal]
-p_maximal_normal [lemma, in mathcomp.solvable.maximal]
-p'groupEpi [lemma, in mathcomp.solvable.pgroup]
-p'group_quotient_cent_prime [lemma, in mathcomp.solvable.pgroup]
-p'natE [lemma, in mathcomp.ssreflect.prime]
-p'natEpi [lemma, in mathcomp.ssreflect.prime]
-p'nat_coprime [lemma, in mathcomp.ssreflect.prime]
-p'_elt_constt [lemma, in mathcomp.solvable.pgroup]
-p1ElemE [lemma, in mathcomp.solvable.abelian]
-p2Elem_dprodP [lemma, in mathcomp.solvable.abelian]
-p2group_abelian [lemma, in mathcomp.solvable.sylow]
-p3group_extraspecial [lemma, 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) | -