mathcomp.ssreflect.tuple

From ed05182cece6bb3706e09b2ce14af4a41a2e8141 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Apr 2018 10:54:22 +0200 Subject: generate the documentation for 1.7 --- docs/htmldoc/index_global_P.html | 2699 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 2699 insertions(+) create mode 100644 docs/htmldoc/index_global_P.html (limited to 'docs/htmldoc/index_global_P.html') diff --git a/docs/htmldoc/index_global_P.html b/docs/htmldoc/index_global_P.html new file mode 100644 index 0000000..7dd5cb8 --- /dev/null +++ b/docs/htmldoc/index_global_P.html @@ -0,0 +1,2699 @@ + + + + + +mathcomp.ssreflect.tuple + + + + +

+ + + +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

Global Index

Y

_

(23233 entries)

Notation Index

H

J

O

T

W

X

Y

_

(1373 entries)

Module Index

D

H

J

K

L

O

T

W

X

Y

Z

_

other

(213 entries)

Variable Index

J

W

X

Y

_

other

(3475 entries)

Library Index

K

L

O

U

W

X

Y

_

other

(89 entries)

Lemma Index

Y

_

other

(11853 entries)

Constructor Index

J

K

W

Y

_

other

(359 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(47 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(103 entries)

Projection Index

D

H

J

K

L

O

W

X

Y

_

other

(266 entries)

Section Index

J

W

X

Y

_

other

(1118 entries)

Abbreviation Index

Y

_

other

(691 entries)

Definition Index

Y

_

other

(3461 entries)

Record Index

B

D

H

J

K

L

O

W

X

Y

_

other

(185 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]
+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]
+PermSeq [section, in mathcomp.ssreflect.seq]
+PermSeq.T [variable, in mathcomp.ssreflect.seq]
+PermutationParity [section, in mathcomp.fingroup.perm]
+PermutationParity.T [variable, in mathcomp.fingroup.perm]
+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 [lemma, in mathcomp.ssreflect.seq]
+perm_eq_iotaP [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_eq_uniq [lemma, in mathcomp.ssreflect.seq]
+perm_uniq [lemma, in mathcomp.ssreflect.seq]
+perm_eq_small [lemma, in mathcomp.ssreflect.seq]
+perm_eq_size [lemma, in mathcomp.ssreflect.seq]
+perm_eq_all [lemma, in mathcomp.ssreflect.seq]
+perm_eq_mem [lemma, in mathcomp.ssreflect.seq]
+perm_filterC [lemma, in mathcomp.ssreflect.seq]
+perm_filter [lemma, in mathcomp.ssreflect.seq]
+perm_eq_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_cat2r [lemma, in mathcomp.ssreflect.seq]
+perm_cons [lemma, in mathcomp.ssreflect.seq]
+perm_cat2l [lemma, in mathcomp.ssreflect.seq]
+perm_catC [lemma, in mathcomp.ssreflect.seq]
+perm_eqrP [lemma, in mathcomp.ssreflect.seq]
+perm_eqlP [lemma, in mathcomp.ssreflect.seq]
+perm_eqlE [lemma, in mathcomp.ssreflect.seq]
+perm_eqr [abbreviation, in mathcomp.ssreflect.seq]
+perm_eql [abbreviation, in mathcomp.ssreflect.seq]
+perm_eq_trans [lemma, in mathcomp.ssreflect.seq]
+perm_eq_sym [lemma, in mathcomp.ssreflect.seq]
+perm_eq_refl [lemma, in mathcomp.ssreflect.seq]
+perm_eqP [lemma, in mathcomp.ssreflect.seq]
+perm_eq [definition, in mathcomp.ssreflect.seq]
+perm_eq_abelian_type [lemma, in mathcomp.solvable.abelian]
+perm_faithful [lemma, in mathcomp.fingroup.action]
+perm_act1P [lemma, in mathcomp.fingroup.action]
+perm_mact [lemma, in mathcomp.fingroup.action]
+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_wrapped_arg [definition, in mathcomp.ssreflect.prime]
+pi_unwrapped_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]
+PlainTheory [section, in mathcomp.ssreflect.finfun]
+PlainTheory.aT [variable, in mathcomp.ssreflect.finfun]
+PlainTheory.rT [variable, in mathcomp.ssreflect.finfun]
+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_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]
+polyF [definition, in mathcomp.field.closed_field]
+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.PolyOverSemiring [section, 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_countMixin [definition, in mathcomp.field.countalg]
+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_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]
+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]
+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_eqMixin [definition, in mathcomp.ssreflect.eqtype]
+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

Y

_

(23233 entries)

Notation Index

H

J

O

T

W

X

Y

_

(1373 entries)

Module Index

D

H

J

K

L

O

T

W

X

Y

Z

_

other

(213 entries)

Variable Index

J

W

X

Y

_

other

(3475 entries)

Library Index

K

L

O

U

W

X

Y

_

other

(89 entries)

Lemma Index

Y

_

other

(11853 entries)

Constructor Index

J

K

W

Y

_

other

(359 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(47 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(103 entries)

Projection Index

D

H

J

K

L

O

W

X

Y

_

other

(266 entries)

Section Index

J

W

X

Y

_

other

(1118 entries)

Abbreviation Index

Y

_

other

(691 entries)

Definition Index

Y

_

other

(3461 entries)

Record Index

B

D

H

J

K

L

O

W

X

Y

_

other

(185 entries)

+

+ + + +

+ + + \ No newline at end of file -- cgit v1.2.3