| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (54001 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1931 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1658 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7199 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15214 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (224 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (132 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2371 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2266 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (732 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21455 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (647 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]
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]
PairComSemiRing [section, in mathcomp.algebra.ssralg]
PairComSemiRing.R1 [variable, in mathcomp.algebra.ssralg]
PairComSemiRing.R2 [variable, in mathcomp.algebra.ssralg]
pairg1 [definition, in mathcomp.fingroup.gproduct]
pairg1_morphism [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_bseq [definition, in mathcomp.ssreflect.tuple]
pairmap_bseqP [lemma, in mathcomp.ssreflect.tuple]
pairmap_tuple [definition, in mathcomp.ssreflect.tuple]
pairmap_tupleP [lemma, in mathcomp.ssreflect.tuple]
pairmap_cat [lemma, in mathcomp.ssreflect.seq]
pairMnE [lemma, in mathcomp.algebra.ssralg]
PairNmod [section, in mathcomp.algebra.ssralg]
PairNmod.U [variable, in mathcomp.algebra.ssralg]
PairNmod.V [variable, in mathcomp.algebra.ssralg]
PairSemiRing [section, in mathcomp.algebra.ssralg]
PairSemiRing.R1 [variable, in mathcomp.algebra.ssralg]
PairSemiRing.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 [definition, in mathcomp.ssreflect.seq]
Pairwise [section, in mathcomp.ssreflect.seq]
pairwiseP [lemma, in mathcomp.ssreflect.seq]
pairwise_trans [lemma, in mathcomp.ssreflect.seq]
pairwise_eq [lemma, in mathcomp.ssreflect.seq]
pairwise_uniq [lemma, in mathcomp.ssreflect.seq]
pairwise_relI [lemma, in mathcomp.ssreflect.seq]
pairwise_map [lemma, in mathcomp.ssreflect.seq]
pairwise_all2rel [lemma, in mathcomp.ssreflect.seq]
pairwise_filter [lemma, in mathcomp.ssreflect.seq]
pairwise_mask [lemma, in mathcomp.ssreflect.seq]
pairwise_rcons [lemma, in mathcomp.ssreflect.seq]
pairwise_cat [lemma, in mathcomp.ssreflect.seq]
pairwise_cons [lemma, in mathcomp.ssreflect.seq]
pairwise_orthogonal_cat [lemma, in mathcomp.character.classfun]
pairwise_orthogonalP [lemma, in mathcomp.character.classfun]
pairwise_orthogonal [definition, in mathcomp.character.classfun]
pairwise_sort [lemma, in mathcomp.ssreflect.path]
pairwise_sorted [lemma, in mathcomp.ssreflect.path]
pairwise_orthogonal_cat [lemma, in mathcomp.algebra.sesquilinear]
pairwise_orthogonalP [lemma, in mathcomp.algebra.sesquilinear]
pairwise_orthogonal [definition, in mathcomp.algebra.sesquilinear]
Pairwise.r [variable, in mathcomp.ssreflect.seq]
Pairwise.T [variable, in mathcomp.ssreflect.seq]
pairwise2 [lemma, in mathcomp.ssreflect.seq]
PairZmod [section, in mathcomp.algebra.ssralg]
PairZmod.U [variable, in mathcomp.algebra.ssralg]
PairZmod.V [variable, in mathcomp.algebra.ssralg]
pair_of_interval [definition, in mathcomp.algebra.interval]
pair_of_tagK [lemma, in mathcomp.ssreflect.choice]
pair_of_tag [definition, in mathcomp.ssreflect.choice]
pair_of_mxvec_index [definition, in mathcomp.algebra.matrix]
pair_of_section [definition, in mathcomp.solvable.jordanholder]
pair_ortho_rec [definition, in mathcomp.character.classfun]
pair_of_sd [definition, in mathcomp.fingroup.gproduct]
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_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_one_neq0 [lemma, in mathcomp.algebra.ssralg]
pair_mulr0 [lemma, in mathcomp.algebra.ssralg]
pair_mul0r [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_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_vect_iso [lemma, in mathcomp.algebra.vector]
pair_ortho_rec [definition, in mathcomp.algebra.sesquilinear]
pair_bigA [lemma, in mathcomp.ssreflect.bigop]
pair_big [lemma, in mathcomp.ssreflect.bigop]
pair_big_dep [lemma, in mathcomp.ssreflect.bigop]
pair_bigA_idem [lemma, in mathcomp.ssreflect.bigop]
pair_big_idem [lemma, in mathcomp.ssreflect.bigop]
pair_big_dep_idem [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_morphism [definition, in mathcomp.fingroup.gproduct]
pair1g_morphM [lemma, in mathcomp.fingroup.gproduct]
parse [definition, in mathcomp.algebra.rat]
parse [definition, in mathcomp.algebra.ssralg]
parse_int [definition, in mathcomp.algebra.ssrint]
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]
partitionD1 [lemma, in mathcomp.ssreflect.finset]
PartitionImage [section, in mathcomp.ssreflect.finset]
PartitionImage.D [variable, in mathcomp.ssreflect.finset]
PartitionImage.f [variable, in mathcomp.ssreflect.finset]
PartitionImage.fP [variable, in mathcomp.ssreflect.finset]
PartitionImage.inj_f [variable, in mathcomp.ssreflect.finset]
PartitionImage.P [variable, in mathcomp.ssreflect.finset]
PartitionImage.T [variable, in mathcomp.ssreflect.finset]
PartitionImage.T' [variable, in mathcomp.ssreflect.finset]
partitionS [lemma, 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]
partitionU1 [lemma, in mathcomp.ssreflect.finset]
partition_partition [lemma, in mathcomp.ssreflect.finset]
partition_disjoint_bigcup [lemma, in mathcomp.ssreflect.finset]
partition_pigeonhole [lemma, in mathcomp.ssreflect.finset]
partition_set0 [lemma, in mathcomp.ssreflect.finset]
partition_trivIset [lemma, in mathcomp.ssreflect.finset]
partition_neq0 [lemma, in mathcomp.ssreflect.finset]
partition_big_imset [lemma, 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_big_idem [lemma, in mathcomp.ssreflect.bigop]
partition0 [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 [definition, in mathcomp.ssreflect.binomial]
passmx [module, in mathcomp.algebra.vector]
passmx.coord_vecof [lemma, in mathcomp.algebra.vector]
passmx.coord_rVof [lemma, in mathcomp.algebra.vector]
passmx.funmx [definition, in mathcomp.algebra.vector]
passmx.funmx_linear [lemma, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isSemiAdditive__164 [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isScalable__162 [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isSemiAdditive__156 [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isScalable__154 [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isSemiAdditive__148 [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isScalable__146 [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isSemiAdditive__141 [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isScalable__139 [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isSemiAdditive [definition, in mathcomp.algebra.vector]
passmx.GRing_isLinear__to__GRing_isScalable [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_166 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_165 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_factory_160 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_158 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_157 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_factory_152 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_150 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_149 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_factory_144 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_143 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_142 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_factory_137 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_136 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_mixin_135 [definition, in mathcomp.algebra.vector]
passmx.HB_unnamed_factory_132 [definition, in mathcomp.algebra.vector]
passmx.hommx [definition, in mathcomp.algebra.vector]
passmx.hommxE [lemma, in mathcomp.algebra.vector]
passmx.hommxK [lemma, in mathcomp.algebra.vector]
passmx.hommx_mul [lemma, in mathcomp.algebra.vector]
passmx.hommx_eq0 [lemma, in mathcomp.algebra.vector]
passmx.hommx_linear [lemma, in mathcomp.algebra.vector]
passmx.hommx1 [lemma, in mathcomp.algebra.vector]
passmx.hom_vecof [lemma, in mathcomp.algebra.vector]
passmx.leigenspace [definition, in mathcomp.algebra.vector]
passmx.leigenspaceE [lemma, in mathcomp.algebra.vector]
passmx.leigenvalue [definition, in mathcomp.algebra.vector]
passmx.limgE [lemma, in mathcomp.algebra.vector]
passmx.lker_ker [lemma, in mathcomp.algebra.vector]
passmx.m [abbreviation, in mathcomp.algebra.vector]
passmx.m [abbreviation, in mathcomp.algebra.vector]
passmx.m [abbreviation, in mathcomp.algebra.vector]
passmx.mem_vecof [lemma, in mathcomp.algebra.vector]
passmx.msof [definition, in mathcomp.algebra.vector]
passmx.msofK [lemma, in mathcomp.algebra.vector]
passmx.msof_eq0 [lemma, in mathcomp.algebra.vector]
passmx.msof_sub [lemma, in mathcomp.algebra.vector]
passmx.msof0 [lemma, in mathcomp.algebra.vector]
passmx.mul_mxof [lemma, in mathcomp.algebra.vector]
passmx.mxof [definition, in mathcomp.algebra.vector]
passmx.mxofK [lemma, in mathcomp.algebra.vector]
passmx.mxof_comp [lemma, in mathcomp.algebra.vector]
passmx.mxof_eq0 [lemma, in mathcomp.algebra.vector]
passmx.mxof_linear [lemma, in mathcomp.algebra.vector]
passmx.mxof1 [lemma, in mathcomp.algebra.vector]
passmx.n [abbreviation, in mathcomp.algebra.vector]
passmx.n [abbreviation, in mathcomp.algebra.vector]
passmx.n [abbreviation, in mathcomp.algebra.vector]
passmx.n [abbreviation, in mathcomp.algebra.vector]
passmx.p [abbreviation, in mathcomp.algebra.vector]
passmx.passmx [section, in mathcomp.algebra.vector]
passmx.passmx_hommx__canonical__GRing_Linear [definition, in mathcomp.algebra.vector]
passmx.passmx_hommx__canonical__GRing_Additive [definition, in mathcomp.algebra.vector]
passmx.passmx_funmx__canonical__GRing_Linear [definition, in mathcomp.algebra.vector]
passmx.passmx_funmx__canonical__GRing_Additive [definition, in mathcomp.algebra.vector]
passmx.passmx_mxof__canonical__GRing_Linear [definition, in mathcomp.algebra.vector]
passmx.passmx_mxof__canonical__GRing_Additive [definition, in mathcomp.algebra.vector]
passmx.passmx_vecof__canonical__GRing_Linear [definition, in mathcomp.algebra.vector]
passmx.passmx_vecof__canonical__GRing_Additive [definition, in mathcomp.algebra.vector]
passmx.passmx_rVof__canonical__GRing_Linear [definition, in mathcomp.algebra.vector]
passmx.passmx_rVof__canonical__GRing_Additive [definition, in mathcomp.algebra.vector]
passmx.passmx.eigen [section, in mathcomp.algebra.vector]
passmx.passmx.eigen.e [variable, in mathcomp.algebra.vector]
passmx.passmx.eigen.e_free [variable, in mathcomp.algebra.vector]
passmx.passmx.eigen.e_basis [variable, in mathcomp.algebra.vector]
passmx.passmx.F [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx [section, in mathcomp.algebra.vector]
passmx.passmx.hommx_comp.g_basis [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx_comp.f_basis [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx_comp.e_basis [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx_comp.g [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx_comp.f [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx_comp.e [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx_comp [section, in mathcomp.algebra.vector]
passmx.passmx.hommx.e [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx.e_basis [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx.e' [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx.f_basis [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx.hb_instance_159.M [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx.hb_instance_159.hb_instance_159 [section, in mathcomp.algebra.vector]
passmx.passmx.hommx.hb_instance_151.M [variable, in mathcomp.algebra.vector]
passmx.passmx.hommx.hb_instance_151.hb_instance_151 [section, in mathcomp.algebra.vector]
passmx.passmx.vecmx [section, in mathcomp.algebra.vector]
passmx.passmx.vecmx.e [variable, in mathcomp.algebra.vector]
passmx.passmx.vecmx.e_basis [variable, in mathcomp.algebra.vector]
passmx.passmx.vsms [section, in mathcomp.algebra.vector]
passmx.passmx.vsms.e [variable, in mathcomp.algebra.vector]
passmx.passmx.vsms.e_basis [variable, in mathcomp.algebra.vector]
passmx.rVof [definition, in mathcomp.algebra.vector]
passmx.rVofE [lemma, in mathcomp.algebra.vector]
passmx.rVofK [lemma, in mathcomp.algebra.vector]
passmx.rVof_sub [lemma, in mathcomp.algebra.vector]
passmx.rVof_app [lemma, in mathcomp.algebra.vector]
passmx.rVof_mul [lemma, in mathcomp.algebra.vector]
passmx.rVof_eq0 [lemma, in mathcomp.algebra.vector]
passmx.rVof_linear [lemma, in mathcomp.algebra.vector]
passmx.sub_vsof [lemma, in mathcomp.algebra.vector]
passmx.sub_msof [lemma, in mathcomp.algebra.vector]
passmx.vecof [definition, in mathcomp.algebra.vector]
passmx.vecofK [lemma, in mathcomp.algebra.vector]
passmx.vecof_mul [lemma, in mathcomp.algebra.vector]
passmx.vecof_eq0 [lemma, in mathcomp.algebra.vector]
passmx.vecof_linear [lemma, in mathcomp.algebra.vector]
passmx.vecof_delta [lemma, in mathcomp.algebra.vector]
passmx.vsof [definition, in mathcomp.algebra.vector]
passmx.vsofK [lemma, in mathcomp.algebra.vector]
passmx.vsof_eq0 [lemma, in mathcomp.algebra.vector]
passmx.vsof_sub [lemma, in mathcomp.algebra.vector]
passmx.vsof0 [lemma, in mathcomp.algebra.vector]
path [abbreviation, in mathcomp.ssreflect.path]
path [abbreviation, in mathcomp.ssreflect.path]
path [definition, in mathcomp.ssreflect.path]
path [library]
pathP [lemma, in mathcomp.ssreflect.path]
Paths [section, in mathcomp.ssreflect.path]
Paths.EqPath_in.e'_e [variable, in mathcomp.ssreflect.path]
Paths.EqPath_in.e_e' [variable, in mathcomp.ssreflect.path]
Paths.EqPath_in.ee' [variable, in mathcomp.ssreflect.path]
Paths.EqPath_in.e' [variable, in mathcomp.ssreflect.path]
Paths.EqPath_in.e [variable, in mathcomp.ssreflect.path]
Paths.EqPath_in.P [variable, in mathcomp.ssreflect.path]
Paths.EqPath_in [section, in mathcomp.ssreflect.path]
Paths.n0 [variable, in mathcomp.ssreflect.path]
Paths.Path [section, in mathcomp.ssreflect.path]
Paths.PathEq [section, in mathcomp.ssreflect.path]
Paths.PathEq.e [variable, in mathcomp.ssreflect.path]
Paths.PathEq.e' [variable, in mathcomp.ssreflect.path]
Paths.Path.e [variable, in mathcomp.ssreflect.path]
Paths.Path.x0_cycle [variable, in mathcomp.ssreflect.path]
Paths.SubPath [section, in mathcomp.ssreflect.path]
Paths.SubPath_in.ee' [variable, in mathcomp.ssreflect.path]
Paths.SubPath_in.e' [variable, in mathcomp.ssreflect.path]
Paths.SubPath_in.e [variable, in mathcomp.ssreflect.path]
Paths.SubPath_in.P [variable, in mathcomp.ssreflect.path]
Paths.SubPath_in [section, in mathcomp.ssreflect.path]
Paths.SubPath.e [variable, in mathcomp.ssreflect.path]
Paths.SubPath.e' [variable, in mathcomp.ssreflect.path]
Paths.T [variable, in mathcomp.ssreflect.path]
Paths.Transitive [section, in mathcomp.ssreflect.path]
Paths.Transitive_in.leT_refl [variable, in mathcomp.ssreflect.path]
Paths.Transitive_in.leT_tr [variable, in mathcomp.ssreflect.path]
Paths.Transitive_in.leT [variable, in mathcomp.ssreflect.path]
Paths.Transitive_in.P [variable, in mathcomp.ssreflect.path]
Paths.Transitive_in [section, in mathcomp.ssreflect.path]
Paths.Transitive.leT [variable, in mathcomp.ssreflect.path]
Paths.Transitive.leT_refl [variable, in mathcomp.ssreflect.path]
Paths.Transitive.leT_tr' [variable, in mathcomp.ssreflect.path]
Paths.Transitive.leT_tr [variable, in mathcomp.ssreflect.path]
path_map [lemma, in mathcomp.ssreflect.path]
path_filter [lemma, in mathcomp.ssreflect.path]
path_mask [lemma, in mathcomp.ssreflect.path]
path_pairwise [lemma, in mathcomp.ssreflect.path]
path_sortedE [lemma, in mathcomp.ssreflect.path]
path_le [lemma, in mathcomp.ssreflect.path]
path_filter_in [lemma, in mathcomp.ssreflect.path]
path_mask_in [lemma, in mathcomp.ssreflect.path]
path_pairwise_in [lemma, in mathcomp.ssreflect.path]
path_sorted_inE [lemma, in mathcomp.ssreflect.path]
path_relI [lemma, 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]
PCanHasChoice [lemma, in mathcomp.ssreflect.choice]
PCanIsCountable [definition, in mathcomp.ssreflect.choice]
PCanIsFinite [definition, in mathcomp.ssreflect.fintype]
pcan_pickleK [lemma, in mathcomp.ssreflect.choice]
pcan_enumP [lemma, in mathcomp.ssreflect.fintype]
pcan_type [definition, in mathcomp.ssreflect.eqtype]
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_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]
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_pgFun [definition, in mathcomp.solvable.pgroup]
pcore_gFun [definition, in mathcomp.solvable.pgroup]
pcore_igFun [definition, 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_group [definition, in mathcomp.solvable.pgroup]
pcore_mod [definition, in mathcomp.solvable.pgroup]
pcore_group [definition, in mathcomp.solvable.pgroup]
pcore_Fitting [lemma, in mathcomp.solvable.maximal]
Pdeg2 [module, in mathcomp.algebra.poly]
Pdeg2.Field [module, in mathcomp.algebra.poly]
Pdeg2.FieldMonic [module, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_root2 [lemma, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_root1 [lemma, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_factor [lemma, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.deg2_poly_canonical [lemma, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic [section, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.a [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.a1 [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.b [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.c [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.degp [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.delta [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.F [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.monicp [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.nz2 [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.p [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.r [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.r_sqrt_delta [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.r1 [variable, in mathcomp.algebra.poly]
Pdeg2.FieldMonic.Pdeg2FieldMonic.r2 [variable, in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_root2 [lemma, in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_root1 [lemma, in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_factor [lemma, in mathcomp.algebra.poly]
Pdeg2.Field.deg2_poly_canonical [lemma, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field [section, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.a [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.aa4 [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.aneq0 [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.a2neq0 [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.b [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.c [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.degp [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.delta [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.F [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.nz2 [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.p [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.pE [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.pneq0 [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.r [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.r_sqrt_delta [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.r1 [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.r2 [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.splitr [variable, in mathcomp.algebra.poly]
Pdeg2.Field.Pdeg2Field.sqa2neq0 [variable, in mathcomp.algebra.poly]
Pdiv [module, in mathcomp.algebra.polydiv]
pdiv [definition, in mathcomp.ssreflect.prime]
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.coprimepMl [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepMr [lemma, 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.coprimepZl [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimepZr [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep_XsubC2 [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_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_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.dvdpNl [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpNr [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpN0 [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpp [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpZl [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdpZr [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.dvdp_exp_XsubCP [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_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.eqpW [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_modr [lemma, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp_modl [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.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_XaddC [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_id [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.root_dvdp [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_unlockable [definition, 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.divpD [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.divpN [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.divpp [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.divpP [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.divpZl [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.divpZr [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_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.FieldDivision.Multiplicity [section, 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.horner_mod [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.modpD [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.modpE [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.modpN [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.modpP [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.modpZl [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.modpZr [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.mulKp [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mulpK [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mup [definition, in mathcomp.algebra.polydiv]
Pdiv.Field.mupM [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mupMl [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mupMr [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mupNroot [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mup_XsubCX [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mup_ltn [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mup_leq [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mup_geq [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.mu_prod_XsubC [lemma, in mathcomp.algebra.polydiv]
Pdiv.Field.prod_XsubC_eq [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.Field.XsubC_dvd [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_unlockable [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.drop_poly_divp [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.dvdpP [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.dvdp_eq [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.IdomainMonic [section, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.IdomainMonic.MonicDivisor [section, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.IdomainMonic.MonicDivisor.monq [variable, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.IdomainMonic.MonicDivisor.q [variable, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.IdomainMonic.R [variable, in mathcomp.algebra.polydiv]
Pdiv.IdomainMonic.modpE [lemma, 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.IdomainMonic.take_poly_modp [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit [module, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpAC [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpD [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpK [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpKC [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpN [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpp [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpP [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpZl [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.divpZr [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_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.modpD [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpN [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpP [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpZl [lemma, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.modpZr [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.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.ComRingMonic [section, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.ComRingMonic.d [variable, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.ComRingMonic.mond [variable, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.ComRingMonic.R [variable, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.drop_poly_rdivp [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.eq_rdvdp [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpDl [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rdivpDr [lemma, 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_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.RingMonic [section, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.RingMonic.MonicDivisor [section, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.RingMonic.MonicDivisor.d [variable, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.RingMonic.MonicDivisor.mond [variable, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.RingMonic.R [variable, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpB [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpD [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpN [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpp [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpX [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodpZ [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_compr [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_mulml [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_mulmr [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_sum [lemma, in mathcomp.algebra.polydiv]
Pdiv.RingMonic.rmodp_id [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.RingMonic.take_poly_rmodp [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 [module, 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]
PermDefSection [section, in mathcomp.fingroup.perm]
PermDefSection.T [variable, in mathcomp.fingroup.perm]
permE [lemma, in mathcomp.fingroup.perm]
permEl [lemma, in mathcomp.ssreflect.seq]
PermIn [section, in mathcomp.fingroup.automorphism]
PermIn.A [variable, in mathcomp.fingroup.automorphism]
PermIn.f [variable, in mathcomp.fingroup.automorphism]
PermIn.injf [variable, in mathcomp.fingroup.automorphism]
PermIn.sBf [variable, in mathcomp.fingroup.automorphism]
PermIn.T [variable, in mathcomp.fingroup.automorphism]
permJ [lemma, in mathcomp.fingroup.perm]
permK [lemma, in mathcomp.fingroup.perm]
permKV [lemma, in mathcomp.fingroup.perm]
permM [lemma, in mathcomp.fingroup.perm]
permP [lemma, in mathcomp.fingroup.perm]
permP [lemma, in mathcomp.ssreflect.seq]
permPl [lemma, in mathcomp.ssreflect.seq]
permPr [lemma, in mathcomp.ssreflect.seq]
perms [abbreviation, in mathcomp.ssreflect.seq]
PermSeq [section, in mathcomp.ssreflect.seq]
PermSeq.T [variable, in mathcomp.ssreflect.seq]
perms_rec [definition, in mathcomp.ssreflect.seq]
permS0 [lemma, in mathcomp.fingroup.perm]
permS01 [lemma, in mathcomp.fingroup.perm]
permS1 [lemma, in mathcomp.fingroup.perm]
PermutationParity [section, in mathcomp.fingroup.perm]
PermutationParity.T [variable, in mathcomp.fingroup.perm]
permutations [definition, in mathcomp.ssreflect.seq]
Permutations [section, in mathcomp.ssreflect.seq]
permutationsE [lemma, in mathcomp.ssreflect.seq]
permutationsErot [lemma, in mathcomp.ssreflect.seq]
permutations_all_uniq [lemma, in mathcomp.ssreflect.seq]
permutations_uniq [lemma, in mathcomp.ssreflect.seq]
Permutations.cons_permsE [variable, in mathcomp.ssreflect.seq]
Permutations.permsP [variable, in mathcomp.ssreflect.seq]
Permutations.T [variable, in mathcomp.ssreflect.seq]
permX [lemma, in mathcomp.fingroup.perm]
permX_fix [lemma, in mathcomp.fingroup.perm]
perm_onC [lemma, in mathcomp.fingroup.perm]
perm_on_id [lemma, in mathcomp.fingroup.perm]
perm_onV [lemma, in mathcomp.fingroup.perm]
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_perm_type__canonical__fingroup_FinGroup [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__fingroup_BaseFinGroup [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_unlock [definition, in mathcomp.fingroup.perm]
perm_unlock_subterm [definition, in mathcomp.fingroup.perm]
perm_Locked.unlock [axiom, in mathcomp.fingroup.perm]
perm_Locked.body [axiom, in mathcomp.fingroup.perm]
perm_Locked [module, in mathcomp.fingroup.perm]
perm_proof [lemma, in mathcomp.fingroup.perm]
perm_perm_type__canonical__fintype_SubFinite [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__fintype_Finite [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__choice_SubCountable [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__choice_SubChoice [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__eqtype_SubEquality [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__choice_Countable [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__choice_Choice [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__eqtype_Equality [definition, in mathcomp.fingroup.perm]
perm_perm_type__canonical__eqtype_SubType [definition, in mathcomp.fingroup.perm]
perm_of [definition, in mathcomp.fingroup.perm]
perm_type_sind [definition, in mathcomp.fingroup.perm]
perm_type_rec [definition, in mathcomp.fingroup.perm]
perm_type_ind [definition, in mathcomp.fingroup.perm]
perm_type_rect [definition, in mathcomp.fingroup.perm]
perm_type [inductive, in mathcomp.fingroup.perm]
perm_permutations [lemma, in mathcomp.ssreflect.seq]
perm_count_undup [lemma, in mathcomp.ssreflect.seq]
perm_tseq [abbreviation, in mathcomp.ssreflect.seq]
perm_tally_seq [lemma, in mathcomp.ssreflect.seq]
perm_tally [lemma, in mathcomp.ssreflect.seq]
perm_allpairs [lemma, in mathcomp.ssreflect.seq]
perm_allpairs_consr [lemma, in mathcomp.ssreflect.seq]
perm_allpairs_catr [lemma, in mathcomp.ssreflect.seq]
perm_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
perm_flatten [lemma, in mathcomp.ssreflect.seq]
perm_zip2 [lemma, in mathcomp.ssreflect.seq]
perm_zip1 [lemma, in mathcomp.ssreflect.seq]
perm_zip_sym [lemma, in mathcomp.ssreflect.seq]
perm_sumn [lemma, in mathcomp.ssreflect.seq]
perm_iotaP [lemma, in mathcomp.ssreflect.seq]
perm_pmap [lemma, in mathcomp.ssreflect.seq]
perm_map_inj [lemma, in mathcomp.ssreflect.seq]
perm_map [lemma, in mathcomp.ssreflect.seq]
perm_to_subseq [lemma, in mathcomp.ssreflect.seq]
perm_to_rem [lemma, in mathcomp.ssreflect.seq]
perm_eqr [abbreviation, in mathcomp.ssreflect.seq]
perm_eql [abbreviation, in mathcomp.ssreflect.seq]
perm_undup [lemma, in mathcomp.ssreflect.seq]
perm_uniq [lemma, in mathcomp.ssreflect.seq]
perm_small_eq [lemma, in mathcomp.ssreflect.seq]
perm_all [lemma, in mathcomp.ssreflect.seq]
perm_has [lemma, in mathcomp.ssreflect.seq]
perm_consP [lemma, in mathcomp.ssreflect.seq]
perm_nilP [lemma, in mathcomp.ssreflect.seq]
perm_mem [lemma, in mathcomp.ssreflect.seq]
perm_size [lemma, in mathcomp.ssreflect.seq]
perm_filterC [lemma, in mathcomp.ssreflect.seq]
perm_filter [lemma, in mathcomp.ssreflect.seq]
perm_rev [lemma, in mathcomp.ssreflect.seq]
perm_rotr [lemma, in mathcomp.ssreflect.seq]
perm_rot [lemma, in mathcomp.ssreflect.seq]
perm_rcons [lemma, in mathcomp.ssreflect.seq]
perm_catACA [lemma, in mathcomp.ssreflect.seq]
perm_catCA [lemma, in mathcomp.ssreflect.seq]
perm_catAC [lemma, in mathcomp.ssreflect.seq]
perm_cat [lemma, in mathcomp.ssreflect.seq]
perm_catr [lemma, in mathcomp.ssreflect.seq]
perm_cat2r [lemma, in mathcomp.ssreflect.seq]
perm_cons [lemma, in mathcomp.ssreflect.seq]
perm_catl [lemma, in mathcomp.ssreflect.seq]
perm_cat2l [lemma, in mathcomp.ssreflect.seq]
perm_catC [lemma, in mathcomp.ssreflect.seq]
perm_eqr [abbreviation, in mathcomp.ssreflect.seq]
perm_eql [abbreviation, in mathcomp.ssreflect.seq]
perm_trans [lemma, in mathcomp.ssreflect.seq]
perm_sym [lemma, in mathcomp.ssreflect.seq]
perm_refl [lemma, in mathcomp.ssreflect.seq]
perm_eq [definition, in mathcomp.ssreflect.seq]
perm_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_mxEsub [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_prime_astab [lemma, in mathcomp.fingroup.action]
perm_prime_orbit [lemma, in mathcomp.fingroup.action]
perm_prime_atrans [lemma, in mathcomp.fingroup.action]
perm_faithful [lemma, in mathcomp.fingroup.action]
perm_act1P [lemma, in mathcomp.fingroup.action]
perm_action [definition, in mathcomp.fingroup.action]
perm_mact [lemma, in mathcomp.fingroup.action]
perm_sort_inP [lemma, in mathcomp.ssreflect.path]
perm_sortP [lemma, in mathcomp.ssreflect.path]
perm_iota_sort [lemma, in mathcomp.ssreflect.path]
perm_sort [lemma, in mathcomp.ssreflect.path]
perm_merge [lemma, in mathcomp.ssreflect.path]
perm_bigcprod [lemma, in mathcomp.fingroup.gproduct]
perm_basis [lemma, in mathcomp.algebra.vector]
perm_free [lemma, in mathcomp.algebra.vector]
perm_big_supp [lemma, in mathcomp.ssreflect.bigop]
perm_big_supp_cond [lemma, in mathcomp.ssreflect.bigop]
perm_big [lemma, in mathcomp.ssreflect.bigop]
perm.body [definition, in mathcomp.fingroup.perm]
perm.unlock [definition, in mathcomp.fingroup.perm]
perm1 [lemma, in mathcomp.fingroup.perm]
PervasiveMonoids [section, in mathcomp.ssreflect.bigop]
PervasiveMonoids.hb_instance_120.T [variable, in mathcomp.ssreflect.bigop]
PervasiveMonoids.hb_instance_120.hb_instance_120 [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.action [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_sol [lemma, in mathcomp.solvable.sylow]
pgroup_nil [lemma, in mathcomp.solvable.sylow]
pgroup_fix_mod [lemma, in mathcomp.solvable.sylow]
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]
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 [definition, 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_mxEcol [lemma, in mathcomp.algebra.matrix]
pid_mxErow [lemma, in mathcomp.algebra.matrix]
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]
pinvmxE [lemma, in mathcomp.algebra.mxalgebra]
pinvmx_unitary [lemma, in mathcomp.algebra.spectral]
pinvmx_full [lemma, in mathcomp.algebra.mxalgebra]
pinvmx_free [lemma, 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]
PiSpec [constructor, in mathcomp.ssreflect.generic_quotient]
pi_eq_quot_mono [definition, in mathcomp.ssreflect.generic_quotient]
pi_eq_quot [definition, 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_unlock [definition, in mathcomp.ssreflect.generic_quotient]
pi_unlock_subterm [definition, in mathcomp.ssreflect.generic_quotient]
pi_Locked.unlock [axiom, in mathcomp.ssreflect.generic_quotient]
pi_Locked.body [axiom, in mathcomp.ssreflect.generic_quotient]
pi_Locked [module, in mathcomp.ssreflect.generic_quotient]
pi_subdef [definition, in mathcomp.ssreflect.generic_quotient]
pi_subfext_inv_morph [definition, in mathcomp.field.fieldext]
pi_subfext_inv [lemma, in mathcomp.field.fieldext]
pi_subfext_mul_morph [definition, in mathcomp.field.fieldext]
pi_subfext_mul [lemma, in mathcomp.field.fieldext]
pi_subfext_opp_morph [definition, in mathcomp.field.fieldext]
pi_subfext_opp [lemma, in mathcomp.field.fieldext]
pi_subfx_add_morph [definition, in mathcomp.field.fieldext]
pi_subfext_add [lemma, in mathcomp.field.fieldext]
pi_subfx_inj_morph [definition, in mathcomp.field.fieldext]
pi_subfx_inj [lemma, in mathcomp.field.fieldext]
pi_inv_quot_morph [definition, in mathcomp.algebra.ring_quotient]
pi_unit_quot_morph [definition, in mathcomp.algebra.ring_quotient]
pi_invr [definition, in mathcomp.algebra.ring_quotient]
pi_unitr [definition, in mathcomp.algebra.ring_quotient]
pi_body__canonical__GRing_RMorphism [definition, in mathcomp.algebra.ring_quotient]
pi_is_multiplicative [lemma, in mathcomp.algebra.ring_quotient]
pi_mul_quot_morph [definition, in mathcomp.algebra.ring_quotient]
pi_one_quot_morph [definition, in mathcomp.algebra.ring_quotient]
pi_mulr [definition, in mathcomp.algebra.ring_quotient]
pi_oner [definition, in mathcomp.algebra.ring_quotient]
pi_body__canonical__GRing_Additive [definition, in mathcomp.algebra.ring_quotient]
pi_is_additive [lemma, in mathcomp.algebra.ring_quotient]
pi_add_quot_morph [definition, in mathcomp.algebra.ring_quotient]
pi_opp_quot_morph [definition, in mathcomp.algebra.ring_quotient]
pi_zero_quot_morph [definition, in mathcomp.algebra.ring_quotient]
pi_addr [definition, in mathcomp.algebra.ring_quotient]
pi_oppr [definition, in mathcomp.algebra.ring_quotient]
pi_zeror [definition, in mathcomp.algebra.ring_quotient]
pi_center_nilpotent [lemma, in mathcomp.solvable.sylow]
pi_p'group [lemma, in mathcomp.solvable.pgroup]
pi_pgroup [lemma, in mathcomp.solvable.pgroup]
pi_p'nat [lemma, in mathcomp.ssreflect.prime]
pi_pnat [lemma, in mathcomp.ssreflect.prime]
pi_of_prime [lemma, in mathcomp.ssreflect.prime]
pi_of_exp [lemma, in mathcomp.ssreflect.prime]
pi_of_part [lemma, in mathcomp.ssreflect.prime]
pi_ofM [lemma, in mathcomp.ssreflect.prime]
pi_of_dvd [lemma, in mathcomp.ssreflect.prime]
pi_max_pdiv [lemma, in mathcomp.ssreflect.prime]
pi_pdiv [lemma, in mathcomp.ssreflect.prime]
pi_of [definition, in mathcomp.ssreflect.prime]
pi_arg_of_fin_pred [definition, in mathcomp.ssreflect.prime]
pi_arg_of_nat [definition, in mathcomp.ssreflect.prime]
pi_arg [definition, in mathcomp.ssreflect.prime]
pi_of_exponent [lemma, in mathcomp.solvable.abelian]
pi'_p'group [lemma, in mathcomp.solvable.pgroup]
pi'_p'nat [lemma, in mathcomp.ssreflect.prime]
pi.body [definition, in mathcomp.ssreflect.generic_quotient]
pi.unlock [definition, in mathcomp.ssreflect.generic_quotient]
Plain [section, in mathcomp.ssreflect.bigop]
Plain.op [variable, in mathcomp.ssreflect.bigop]
Plain.R [variable, in mathcomp.ssreflect.bigop]
Plain.x [variable, in mathcomp.ssreflect.bigop]
plogp [definition, in mathcomp.field.qfpoly]
Plogp [section, in mathcomp.field.qfpoly]
plogpD [lemma, in mathcomp.field.qfpoly]
plogp_div_eq0 [lemma, in mathcomp.field.qfpoly]
plogp_X [lemma, in mathcomp.field.qfpoly]
plogp_lt [lemma, in mathcomp.field.qfpoly]
Plogp.F [variable, in mathcomp.field.qfpoly]
plogp0 [lemma, in mathcomp.field.qfpoly]
plogp1 [lemma, in mathcomp.field.qfpoly]
plusE [lemma, in mathcomp.ssreflect.ssrnat]
pmap [definition, in mathcomp.ssreflect.seq]
Pmap [section, in mathcomp.ssreflect.seq]
PmapSub [section, in mathcomp.ssreflect.seq]
PmapSub.p [variable, in mathcomp.ssreflect.seq]
PmapSub.sT [variable, in mathcomp.ssreflect.seq]
PmapSub.T [variable, in mathcomp.ssreflect.seq]
pmapS_filter [lemma, in mathcomp.ssreflect.seq]
pmap_sub_uniq [lemma, in mathcomp.ssreflect.seq]
pmap_uniq [lemma, in mathcomp.ssreflect.seq]
pmap_cat [lemma, in mathcomp.ssreflect.seq]
pmap_filter [lemma, in mathcomp.ssreflect.seq]
Pmap.aT [variable, in mathcomp.ssreflect.seq]
Pmap.f [variable, in mathcomp.ssreflect.seq]
Pmap.fK [variable, in mathcomp.ssreflect.seq]
Pmap.g [variable, in mathcomp.ssreflect.seq]
Pmap.rT [variable, in mathcomp.ssreflect.seq]
PMax [section, in mathcomp.solvable.maximal]
pmaxElem [definition, in mathcomp.solvable.abelian]
pmaxElemJ [lemma, in mathcomp.solvable.abelian]
pmaxElemP [lemma, in mathcomp.solvable.abelian]
pmaxElemS [lemma, in mathcomp.solvable.abelian]
pmaxElem_LdivP [lemma, in mathcomp.solvable.abelian]
pmaxElem_exists [lemma, in mathcomp.solvable.abelian]
pmaxElem_extraspecial [lemma, in mathcomp.solvable.maximal]
PMax.gT [variable, in mathcomp.solvable.maximal]
PMax.M [variable, in mathcomp.solvable.maximal]
PMax.P [variable, in mathcomp.solvable.maximal]
PMax.p [variable, in mathcomp.solvable.maximal]
PMax.pP [variable, in mathcomp.solvable.maximal]
pmorphimF [lemma, in mathcomp.solvable.gfunctor]
pmorphim_pHall [lemma, in mathcomp.solvable.pgroup]
pmorphim_pgroup [lemma, in mathcomp.solvable.pgroup]
pmulrn [lemma, in mathcomp.algebra.ssrint]
pmulrz_rle0 [lemma, in mathcomp.algebra.ssrint]
pmulrz_rge0 [lemma, in mathcomp.algebra.ssrint]
pmulrz_rlt0 [lemma, in mathcomp.algebra.ssrint]
pmulrz_rgt0 [lemma, in mathcomp.algebra.ssrint]
pmulrz_lle0 [lemma, in mathcomp.algebra.ssrint]
pmulrz_lge0 [lemma, in mathcomp.algebra.ssrint]
pmulrz_llt0 [lemma, in mathcomp.algebra.ssrint]
pmulrz_lgt0 [lemma, in mathcomp.algebra.ssrint]
pnat [definition, in mathcomp.ssreflect.prime]
pnatE [lemma, in mathcomp.ssreflect.prime]
pnatI [lemma, in mathcomp.ssreflect.prime]
pnatM [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]
pnatX [lemma, 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_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]
polyCB [lemma, in mathcomp.algebra.poly]
polyCD [lemma, in mathcomp.algebra.poly]
polyCK [lemma, in mathcomp.algebra.poly]
polyCM [lemma, in mathcomp.algebra.poly]
polyCMn [lemma, in mathcomp.algebra.poly]
polyCMz [lemma, in mathcomp.algebra.ssrint]
polyCN [lemma, in mathcomp.algebra.poly]
PolyCompose [section, in mathcomp.algebra.poly]
PolyCompose.hb_instance_91.p [variable, in mathcomp.algebra.poly]
PolyCompose.hb_instance_91.hb_instance_91 [section, in mathcomp.algebra.poly]
PolyCompose.R [variable, in mathcomp.algebra.poly]
_ \Po _ (ring_scope) [notation, in mathcomp.algebra.poly]
polyCV [lemma, in mathcomp.algebra.poly]
polyC_natr [lemma, in mathcomp.algebra.poly]
polyC_exp [lemma, in mathcomp.algebra.poly]
polyC_multiplicative [lemma, in mathcomp.algebra.poly]
polyC_eq0 [lemma, in mathcomp.algebra.poly]
polyC_inj [lemma, in mathcomp.algebra.poly]
polyC0 [lemma, in mathcomp.algebra.poly]
polyC1 [lemma, in mathcomp.algebra.poly]
polydiv [library]
PolyK [lemma, in mathcomp.algebra.poly]
polyn [projection, in mathcomp.algebra.qpoly]
polynomial [record, in mathcomp.algebra.poly]
Polynomial [section, in mathcomp.algebra.poly]
PolynomialComRing [section, in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_153.q [variable, in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_153.hb_instance_153 [section, in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_143.x [variable, in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_143.hb_instance_143 [section, in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_135.x [variable, in mathcomp.algebra.poly]
PolynomialComRing.hb_instance_135.hb_instance_135 [section, in mathcomp.algebra.poly]
PolynomialComRing.HornerAlg [section, in mathcomp.algebra.poly]
PolynomialComRing.HornerAlg.A [variable, in mathcomp.algebra.poly]
PolynomialComRing.HornerAlg.Defs [section, in mathcomp.algebra.poly]
PolynomialComRing.HornerAlg.Defs.a [variable, in mathcomp.algebra.poly]
PolynomialComRing.HornerAlg.pf [variable, 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.hb_instance_66.n [variable, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_66.hb_instance_66 [section, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_58.n [variable, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_58.hb_instance_58 [section, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_45.zmodS [variable, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_45.hb_instance_45 [section, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_30.i [variable, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_30.hb_instance_30 [section, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_14.i [variable, in mathcomp.algebra.poly]
PolynomialTheory.hb_instance_14.hb_instance_14 [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.S [variable, in mathcomp.algebra.poly]
PolynomialTheory.PolyOverRing [section, in mathcomp.algebra.poly]
PolynomialTheory.PolyOverRing.S [variable, in mathcomp.algebra.poly]
PolynomialTheory.PolyOverSemiring [section, in mathcomp.algebra.poly]
PolynomialTheory.PolyOverSemiring.S [variable, in mathcomp.algebra.poly]
PolynomialTheory.PolyOverSemiRing2 [section, in mathcomp.algebra.poly]
PolynomialTheory.PolyOverSemiRing2.S [variable, in mathcomp.algebra.poly]
PolynomialTheory.R [variable, in mathcomp.algebra.poly]
_ ^`N ( _ ) (ring_scope) [notation, in mathcomp.algebra.poly]
_ ^` ( _ ) (ring_scope) [notation, in mathcomp.algebra.poly]
_ .-primitive_root (ring_scope) [notation, in mathcomp.algebra.poly]
_ .-unity_root (ring_scope) [notation, in mathcomp.algebra.poly]
_ .[ _ ] (ring_scope) [notation, in mathcomp.algebra.poly]
_ ^` () [notation, in mathcomp.algebra.poly]
_ %:P [notation, in mathcomp.algebra.poly]
'X [notation, in mathcomp.algebra.poly]
'X^ _ [notation, in mathcomp.algebra.poly]
\poly_ ( _ < _ ) _ [notation, in mathcomp.algebra.poly]
Polynomial.R [variable, in mathcomp.algebra.poly]
polyn_is_linear [lemma, in mathcomp.algebra.qpoly]
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]
polyOverXaddC [lemma, in mathcomp.algebra.poly]
polyOverXn [lemma, in mathcomp.algebra.poly]
polyOverXnaddC [lemma, in mathcomp.algebra.poly]
polyOverXnsubC [lemma, in mathcomp.algebra.poly]
polyOverXsubC [lemma, in mathcomp.algebra.poly]
polyOverZ [lemma, in mathcomp.algebra.poly]
polyOver_dvdzP [lemma, in mathcomp.algebra.intdiv]
polyOver_subvs [lemma, in mathcomp.field.fieldext]
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_mul1_closed [lemma, in mathcomp.algebra.poly]
polyOver_mulr_2closed [lemma, in mathcomp.algebra.poly]
polyOver_addr_closed [lemma, in mathcomp.algebra.poly]
polyOver_poly [lemma, in mathcomp.algebra.poly]
polyOver_pred [definition, 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]
polyseqXaddC [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_swapXY__canonical__GRing_LRMorphism [definition, in mathcomp.algebra.polyXY]
polyXY_swapXY__canonical__GRing_Linear [definition, in mathcomp.algebra.polyXY]
polyXY_swapXY__canonical__GRing_RMorphism [definition, in mathcomp.algebra.polyXY]
polyXY_swapXY__canonical__GRing_Additive [definition, 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_unlockable [definition, in mathcomp.algebra.poly]
polyX_key [lemma, in mathcomp.algebra.poly]
polyX_def [definition, in mathcomp.algebra.poly]
PolyZintRing [section, in mathcomp.algebra.ssrint]
PolyZintRing.R [variable, in mathcomp.algebra.ssrint]
poly_square_freeP [lemma, in mathcomp.field.separable]
poly_rV_is_linear [lemma, in mathcomp.algebra.mxpoly]
poly_rV_K [lemma, in mathcomp.algebra.mxpoly]
poly_rV [definition, in mathcomp.algebra.mxpoly]
poly_XmY_eq0 [lemma, in mathcomp.algebra.polyXY]
poly_XaY_eq0 [lemma, in mathcomp.algebra.polyXY]
poly_XmY0 [lemma, in mathcomp.algebra.polyXY]
poly_XaY0 [lemma, in mathcomp.algebra.polyXY]
poly_XmY [definition, in mathcomp.algebra.polyXY]
poly_XaY [definition, in mathcomp.algebra.polyXY]
poly_polynomial__canonical__CountRing_IntegralDomain [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__CountRing_ComUnitRing [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__CountRing_UnitRing [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__CountRing_ComRing [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__CountRing_ComSemiRing [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__choice_SubCountable [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__CountRing_Ring [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__CountRing_Zmodule [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__CountRing_SemiRing [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__CountRing_Nmodule [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__choice_Countable [definition, in mathcomp.algebra.poly]
poly_invE [lemma, in mathcomp.algebra.poly]
poly_unitE [lemma, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_IntegralDomain [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_ComUnitAlgebra [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_ComUnitRing [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_UnitAlgebra [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_UnitRing [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_comp_poly__canonical__GRing_LRMorphism [definition, in mathcomp.algebra.poly]
poly_comp_poly__canonical__GRing_RMorphism [definition, in mathcomp.algebra.poly]
poly_alg_initial [lemma, in mathcomp.algebra.poly]
poly_horner_alg__canonical__GRing_LRMorphism [definition, in mathcomp.algebra.poly]
poly_horner_alg__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_horner_alg__canonical__GRing_RMorphism [definition, in mathcomp.algebra.poly]
poly_horner_alg__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_horner_eval__canonical__GRing_LRMorphism [definition, in mathcomp.algebra.poly]
poly_horner_eval__canonical__GRing_RMorphism [definition, in mathcomp.algebra.poly]
poly_horner_eval__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_horner_eval__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_ComAlgebra [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_Algebra [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_ComRing [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_ComSemiRing [definition, in mathcomp.algebra.poly]
poly_mul_comm [lemma, in mathcomp.algebra.poly]
poly_take_drop [lemma, in mathcomp.algebra.poly]
poly_drop_poly__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_drop_poly__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_take_poly__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_take_poly__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_even_odd [lemma, in mathcomp.algebra.poly]
poly_odd_poly__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_odd_poly__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_even_poly__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_even_poly__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_comp_poly__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_comp_poly__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_initial [lemma, in mathcomp.algebra.poly]
poly_morphX_comm [lemma, in mathcomp.algebra.poly]
poly_horner_morph__canonical__GRing_LRMorphism [definition, in mathcomp.algebra.poly]
poly_horner_morph__canonical__GRing_RMorphism [definition, in mathcomp.algebra.poly]
poly_horner_morph__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_horner_morph__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_map_poly__canonical__GRing_LRMorphism [definition, in mathcomp.algebra.poly]
poly_map_poly__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_map_poly__canonical__GRing_RMorphism [definition, in mathcomp.algebra.poly]
poly_map_poly__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_nderivn__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_nderivn__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_derivn__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_derivn__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_deriv__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_deriv__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_SubringClosed [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_SmulClosed [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_SemiringClosed [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_MulClosed [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_ZmodClosed [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_OppClosed [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_Semiring2Closed [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_Mul2Closed [definition, in mathcomp.algebra.poly]
poly_polyOver_pred__canonical__GRing_AddClosed [definition, in mathcomp.algebra.poly]
poly_monic_pred__canonical__GRing_MulClosed [definition, in mathcomp.algebra.poly]
poly_monic_pred__canonical__GRing_Mul2Closed [definition, in mathcomp.algebra.poly]
poly_def [lemma, in mathcomp.algebra.poly]
poly_ind [lemma, in mathcomp.algebra.poly]
poly_coefp__canonical__GRing_LRMorphism [definition, in mathcomp.algebra.poly]
poly_coefp__canonical__GRing_Linear [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_Lalgebra [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_Lmodule [definition, in mathcomp.algebra.poly]
poly_coefp__canonical__GRing_RMorphism [definition, in mathcomp.algebra.poly]
poly_polyC__canonical__GRing_RMorphism [definition, in mathcomp.algebra.poly]
poly_polyC__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_coefp__canonical__GRing_Additive [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_Ring [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_Zmodule [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_SemiRing [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__GRing_Nmodule [definition, in mathcomp.algebra.poly]
poly_unlockable [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_inj [lemma, in mathcomp.algebra.poly]
poly_polynomial__canonical__choice_SubChoice [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__eqtype_SubEquality [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__choice_Choice [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__eqtype_Equality [definition, in mathcomp.algebra.poly]
poly_polynomial__canonical__eqtype_SubType [definition, in mathcomp.algebra.poly]
poly_of_qpolyZ [lemma, in mathcomp.algebra.qpoly]
poly_of_qpolyX [lemma, in mathcomp.algebra.qpoly]
poly_of_qpolyM [lemma, in mathcomp.algebra.qpoly]
poly_of_qpolyD [lemma, in mathcomp.algebra.qpoly]
poly_of_qpoly_sum [lemma, in mathcomp.algebra.qpoly]
poly_of_size_mod [lemma, in mathcomp.algebra.qpoly]
poly_of_size_zmod.npoly.n [variable, in mathcomp.algebra.qpoly]
poly_of_size_zmod.npoly [section, in mathcomp.algebra.qpoly]
poly_of_size [definition, in mathcomp.algebra.qpoly]
poly_of_size_pred [definition, in mathcomp.algebra.qpoly]
poly_of_size_zmod.poly_of_size.n [variable, in mathcomp.algebra.qpoly]
poly_of_size_zmod.poly_of_size [section, in mathcomp.algebra.qpoly]
poly_of_size_zmod [section, in mathcomp.algebra.qpoly]
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]
porbit [module, in mathcomp.fingroup.perm]
porbitE [lemma, in mathcomp.fingroup.action]
porbitP [lemma, in mathcomp.fingroup.perm]
porbitPmin [lemma, in mathcomp.fingroup.perm]
porbits [definition, in mathcomp.fingroup.perm]
porbitsV [lemma, in mathcomp.fingroup.perm]
porbits_mul_tperm [lemma, in mathcomp.fingroup.perm]
porbitV [lemma, in mathcomp.fingroup.perm]
porbit_setP [lemma, in mathcomp.fingroup.perm]
porbit_perm [lemma, in mathcomp.fingroup.perm]
porbit_sym [lemma, in mathcomp.fingroup.perm]
porbit_traject [lemma, in mathcomp.fingroup.perm]
porbit_id [lemma, in mathcomp.fingroup.perm]
porbit_unlockable [definition, in mathcomp.fingroup.perm]
porbit_unlock_subterm [definition, in mathcomp.fingroup.perm]
porbit_Locked.unlock [axiom, in mathcomp.fingroup.perm]
porbit_Locked.body [axiom, in mathcomp.fingroup.perm]
porbit_Locked [module, in mathcomp.fingroup.perm]
porbit_actperm [lemma, in mathcomp.fingroup.action]
porbit.body [definition, in mathcomp.fingroup.perm]
porbit.unlock [definition, in mathcomp.fingroup.perm]
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]
powX_eq_mod [lemma, in mathcomp.field.qfpoly]
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]
pprodm_morphism [definition, 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.cyclotomic]
pQtoC [abbreviation, in mathcomp.field.algC]
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_itv [lemma, in mathcomp.algebra.interval]
predC_itvr [lemma, in mathcomp.algebra.interval]
predC_itvl [lemma, in mathcomp.algebra.interval]
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_sub [lemma, in mathcomp.ssreflect.ssrnat]
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_itv [definition, in mathcomp.algebra.interval]
pred_of_seq [definition, in mathcomp.ssreflect.seq]
pred_of_set_unlock [definition, in mathcomp.ssreflect.finset]
pred_of_set_unlock_subterm [definition, in mathcomp.ssreflect.finset]
pred_of_set.unlock [definition, in mathcomp.ssreflect.finset]
pred_of_set.body [definition, in mathcomp.ssreflect.finset]
pred_of_set [module, in mathcomp.ssreflect.finset]
pred_of_set_Locked.unlock [axiom, in mathcomp.ssreflect.finset]
pred_of_set_Locked.body [axiom, in mathcomp.ssreflect.finset]
pred_of_set_Locked [module, in mathcomp.ssreflect.finset]
pred_of_vspace [definition, in mathcomp.algebra.vector]
pred_Nirr [definition, in mathcomp.character.character]
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 [definition, in mathcomp.ssreflect.seq]
prefixE [lemma, in mathcomp.ssreflect.seq]
prefixP [lemma, in mathcomp.ssreflect.seq]
PrefixSuffixInfix [section, in mathcomp.ssreflect.seq]
PrefixSuffixInfix.T [variable, in mathcomp.ssreflect.seq]
prefixs0 [lemma, in mathcomp.ssreflect.seq]
prefixs1 [lemma, in mathcomp.ssreflect.seq]
prefixW [lemma, in mathcomp.ssreflect.seq]
prefix_index [lemma, in mathcomp.ssreflect.seq]
prefix_drop_gt0 [lemma, in mathcomp.ssreflect.seq]
prefix_take [lemma, in mathcomp.ssreflect.seq]
prefix_uniq [lemma, in mathcomp.ssreflect.seq]
prefix_suffix_trans [lemma, in mathcomp.ssreflect.seq]
prefix_infix_trans [lemma, in mathcomp.ssreflect.seq]
prefix_infix [lemma, in mathcomp.ssreflect.seq]
prefix_revLR [lemma, in mathcomp.ssreflect.seq]
prefix_rev [lemma, in mathcomp.ssreflect.seq]
prefix_rcons [lemma, in mathcomp.ssreflect.seq]
prefix_catl [lemma, in mathcomp.ssreflect.seq]
prefix_trans [lemma, in mathcomp.ssreflect.seq]
prefix_prefix [lemma, in mathcomp.ssreflect.seq]
prefix_catr [lemma, in mathcomp.ssreflect.seq]
prefix_cons [lemma, in mathcomp.ssreflect.seq]
prefix_refl [lemma, in mathcomp.ssreflect.seq]
prefix_subseq [lemma, in mathcomp.ssreflect.seq]
prefix_sorted [lemma, in mathcomp.ssreflect.path]
prefix_path [lemma, in mathcomp.ssreflect.path]
prefix0s [lemma, in mathcomp.ssreflect.seq]
prefix1s [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_partition_pblock [lemma, in mathcomp.ssreflect.finset]
preim_partitionP [lemma, in mathcomp.ssreflect.finset]
preim_partition [definition, in mathcomp.ssreflect.finset]
preim_autE [lemma, in mathcomp.fingroup.automorphism]
preim_seq [definition, in mathcomp.ssreflect.fintype]
preim_iinv [lemma, in mathcomp.ssreflect.fintype]
PreInSuffix [section, in mathcomp.ssreflect.path]
PreInSuffix.e [variable, in mathcomp.ssreflect.path]
PreInSuffix.T [variable, in mathcomp.ssreflect.path]
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.env_sind [definition, in mathcomp.fingroup.presentation]
Presentation.env_rec [definition, in mathcomp.fingroup.presentation]
Presentation.env_ind [definition, in mathcomp.fingroup.presentation]
Presentation.env_rect [definition, 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.formula_sind [definition, in mathcomp.fingroup.presentation]
Presentation.formula_rec [definition, in mathcomp.fingroup.presentation]
Presentation.formula_ind [definition, in mathcomp.fingroup.presentation]
Presentation.formula_rect [definition, 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_sind [definition, in mathcomp.fingroup.presentation]
Presentation.rel_type_rec [definition, in mathcomp.fingroup.presentation]
Presentation.rel_type_ind [definition, in mathcomp.fingroup.presentation]
Presentation.rel_type_rect [definition, 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.term_sind [definition, in mathcomp.fingroup.presentation]
Presentation.term_rec [definition, in mathcomp.fingroup.presentation]
Presentation.term_ind [definition, in mathcomp.fingroup.presentation]
Presentation.term_rect [definition, in mathcomp.fingroup.presentation]
Presentation.type [inductive, in mathcomp.fingroup.presentation]
Presentation.type_sind [definition, in mathcomp.fingroup.presentation]
Presentation.type_rec [definition, in mathcomp.fingroup.presentation]
Presentation.type_ind [definition, in mathcomp.fingroup.presentation]
Presentation.type_rect [definition, in mathcomp.fingroup.presentation]
prev [definition, in mathcomp.ssreflect.path]
prevE [lemma, in mathcomp.ssreflect.fingraph]
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_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_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.hb_instance_202.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_202.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_202.hb_instance_202 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_191.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_191.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_191.hb_instance_191 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_181.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_181.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_181.hb_instance_181 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_159.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_159.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_159.hb_instance_159 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_146.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_146.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_146.hb_instance_146 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_136.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_136.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_136.hb_instance_136 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_111.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_111.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_111.hb_instance_111 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_100.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_100.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_100.hb_instance_100 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_91.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_91.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_91.hb_instance_91 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_82.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_82.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_82.hb_instance_82 [section, in mathcomp.field.finfield]
PrimeChar.hb_instance_73.charRp [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_73.R [variable, in mathcomp.field.finfield]
PrimeChar.hb_instance_73.hb_instance_73 [section, in mathcomp.field.finfield]
PrimeChar.p [variable, in mathcomp.field.finfield]
PrimeChar.PrimeCharRing [section, in mathcomp.field.finfield]
PrimeChar.PrimeCharRing.charRp [variable, in mathcomp.field.finfield]
PrimeChar.PrimeCharRing.natrFp [variable, in mathcomp.field.finfield]
PrimeChar.PrimeCharRing.R0 [variable, in mathcomp.field.finfield]
_ *p: _ [notation, in mathcomp.field.finfield]
PrimeDecompAux [module, in mathcomp.ssreflect.prime]
PrimeDecompAux.add_totient_factor [definition, in mathcomp.ssreflect.prime]
PrimeDecompAux.add_divisors [definition, in mathcomp.ssreflect.prime]
PrimeDecompAux.cons_pfactor [definition, in mathcomp.ssreflect.prime]
PrimeDecompAux.edivn2 [definition, in mathcomp.ssreflect.prime]
PrimeDecompAux.edivn2P [lemma, in mathcomp.ssreflect.prime]
PrimeDecompAux.elogn2 [definition, in mathcomp.ssreflect.prime]
PrimeDecompAux.elogn2P [lemma, in mathcomp.ssreflect.prime]
PrimeDecompAux.Elogn2Spec [constructor, in mathcomp.ssreflect.prime]
PrimeDecompAux.elogn2_spec [inductive, in mathcomp.ssreflect.prime]
PrimeDecompAux.ifnz [definition, in mathcomp.ssreflect.prime]
PrimeDecompAux.ifnzP [lemma, in mathcomp.ssreflect.prime]
PrimeDecompAux.IfnzPos [constructor, in mathcomp.ssreflect.prime]
PrimeDecompAux.IfnzZero [constructor, in mathcomp.ssreflect.prime]
PrimeDecompAux.ifnz_spec [inductive, in mathcomp.ssreflect.prime]
_ ^? _ :: _ (nat_scope) [notation, in mathcomp.ssreflect.prime]
PrimeField [section, in mathcomp.algebra.zmodp]
PrimeField.F_prime.p_pr [variable, in mathcomp.algebra.zmodp]
PrimeField.F_prime [section, in mathcomp.algebra.zmodp]
PrimeField.p [variable, in mathcomp.algebra.zmodp]
PrimeIdealr [module, in mathcomp.algebra.ring_quotient]
PrimeIdealrElpiOperations [module, in mathcomp.algebra.ring_quotient]
PrimeIdealr.axioms_ [record, in mathcomp.algebra.ring_quotient]
PrimeIdealr.class [projection, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports [module, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr__to__ring_quotient_Idealr [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr_class__to__ring_quotient_Idealr_class [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr__to__GRing_ZmodClosed [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr_class__to__GRing_ZmodClosed_class [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr__to__GRing_OppClosed [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr_class__to__GRing_OppClosed_class [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr__to__GRing_AddClosed [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr_class__to__GRing_AddClosed_class [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr__to__ring_quotient_ProperIdeal [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.ring_quotient_PrimeIdealr_class__to__ring_quotient_ProperIdeal_class [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.GRing_isAddClosed_mixin [projection, in mathcomp.algebra.ring_quotient]
PrimeIdealr.GRing_isOppClosed_mixin [projection, in mathcomp.algebra.ring_quotient]
PrimeIdealr.pack_ [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.phant_on_ [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.phant_clone [definition, in mathcomp.algebra.ring_quotient]
PrimeIdealr.ring_quotient_isPrimeIdealrClosed_mixin [projection, in mathcomp.algebra.ring_quotient]
PrimeIdealr.ring_quotient_isProperIdeal_mixin [projection, in mathcomp.algebra.ring_quotient]
PrimeIdealr.sort [projection, in mathcomp.algebra.ring_quotient]
PrimeIdealr.type [record, in mathcomp.algebra.ring_quotient]
PrimeIdealTheory [section, in mathcomp.algebra.ring_quotient]
PrimeIdealTheory.pidealI [variable, in mathcomp.algebra.ring_quotient]
PrimeIdealTheory.R [variable, in mathcomp.algebra.ring_quotient]
primeNsig [lemma, in mathcomp.ssreflect.prime]
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]
primesM [lemma, in mathcomp.ssreflect.prime]
primesX [lemma, 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_eq0 [lemma, in mathcomp.ssreflect.prime]
primes_uniq [lemma, in mathcomp.ssreflect.prime]
primes_exponent [lemma, in mathcomp.solvable.abelian]
prime_modn_expSn [lemma, in mathcomp.ssreflect.binomial]
prime_dvd_bin [lemma, in mathcomp.ssreflect.binomial]
prime_idealrM [lemma, in mathcomp.algebra.ring_quotient]
prime_idealr_closed_subproof [definition, in mathcomp.algebra.ring_quotient]
prime_idealr_closed [definition, in mathcomp.algebra.ring_quotient]
prime_invariant_irr_extendible [lemma, in mathcomp.character.inertia]
prime_meetG [lemma, in mathcomp.fingroup.fingroup]
prime_TIg [lemma, in mathcomp.fingroup.fingroup]
prime_subgroupVti [lemma, in mathcomp.solvable.pgroup]
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_Ohm1P [lemma, in mathcomp.solvable.extremal]
prime_abelem [lemma, in mathcomp.solvable.abelian]
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]
PrimitivePoly [section, in mathcomp.field.qfpoly]
PrimitivePoly.F [variable, in mathcomp.field.qfpoly]
PrimitivePoly.h [variable, in mathcomp.field.qfpoly]
PrimitivePoly.Hh [variable, in mathcomp.field.qfpoly]
PrimitivePoly.pred_card_qT_gt0 [variable, in mathcomp.field.qfpoly]
PrimitivePoly.sh_gt1 [variable, in mathcomp.field.qfpoly]
PrimitivePoly.sh_gt2 [variable, in mathcomp.field.qfpoly]
PrimitiveRoots [section, in mathcomp.solvable.cyclic]
Primitive_Element_Theorem [lemma, in mathcomp.field.separable]
primitive_poly_in_qpoly_eq0 [lemma, in mathcomp.field.qfpoly]
primitive_mi [lemma, in mathcomp.field.qfpoly]
primitive_polyP [lemma, in mathcomp.field.qfpoly]
primitive_poly [definition, in mathcomp.field.qfpoly]
primitive_root_splitting_abelian [lemma, in mathcomp.character.mxrepresentation]
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_natf_neq0 [lemma, in mathcomp.algebra.poly]
prim_root_dvd_eq0 [lemma, in mathcomp.algebra.poly]
prim_root_pi_eq0 [lemma, in mathcomp.algebra.poly]
prim_root_charF [lemma, in mathcomp.algebra.poly]
prim_root_exp_coprime [lemma, in mathcomp.algebra.poly]
prim_root_eq0 [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]
print [definition, in mathcomp.algebra.rat]
print [definition, in mathcomp.algebra.ssralg]
print_int [definition, in mathcomp.algebra.ssrint]
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]
prodg_ffun [lemma, in mathcomp.fingroup.gproduct]
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_aspace [definition, in mathcomp.field.fieldext]
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_unlockable [definition, in mathcomp.field.falgebra]
prodv_key [lemma, in mathcomp.field.falgebra]
prodv0 [lemma, in mathcomp.field.falgebra]
prodv1 [lemma, in mathcomp.field.falgebra]
prod_tpermP [lemma, in mathcomp.fingroup.perm]
prod_Cyclotomic [lemma, in mathcomp.field.cyclotomic]
prod_cyclotomic [lemma, in mathcomp.field.cyclotomic]
prod_cfunE [lemma, in mathcomp.character.classfun]
prod_subG [lemma, in mathcomp.fingroup.fingroup]
prod_constt [lemma, in mathcomp.solvable.pgroup]
prod_prime_decomp [lemma, in mathcomp.ssreflect.prime]
prod_t_correct [lemma, in mathcomp.solvable.burnside_app]
prod_tuple [definition, in mathcomp.solvable.burnside_app]
prod_repr_lin [lemma, in mathcomp.character.character]
prod_repr [definition, in mathcomp.character.character]
prod_mx_repr [lemma, in mathcomp.character.character]
prod_enumP [lemma, in mathcomp.ssreflect.fintype]
prod_enum [definition, in mathcomp.ssreflect.fintype]
prod_map_poly [lemma, in mathcomp.algebra.poly]
prod_nat_seq_neq1 [lemma, in mathcomp.ssreflect.bigop]
prod_nat_seq_eq1 [lemma, in mathcomp.ssreflect.bigop]
prod_nat_seq_neq0 [lemma, in mathcomp.ssreflect.bigop]
prod_nat_seq_eq0 [lemma, in mathcomp.ssreflect.bigop]
prod_nat_const_nat [lemma, in mathcomp.ssreflect.bigop]
prod_nat_const [lemma, in mathcomp.ssreflect.bigop]
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_orthoE [lemma, in mathcomp.algebra.spectral]
proj_ortho_proj [lemma, in mathcomp.algebra.spectral]
proj_ortho_0 [lemma, in mathcomp.algebra.spectral]
proj_ortho_id [lemma, in mathcomp.algebra.spectral]
proj_ortho_compl_sub [lemma, in mathcomp.algebra.spectral]
proj_ortho_sub [lemma, in mathcomp.algebra.spectral]
proj_ortho [definition, in mathcomp.algebra.spectral]
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]
properC [lemma, in mathcomp.ssreflect.finset]
properCl [lemma, in mathcomp.ssreflect.finset]
properCr [lemma, in mathcomp.ssreflect.finset]
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]
ProperIdeal [module, in mathcomp.algebra.ring_quotient]
ProperIdealElpiOperations [module, in mathcomp.algebra.ring_quotient]
ProperIdeal.axioms_ [record, in mathcomp.algebra.ring_quotient]
ProperIdeal.class [projection, in mathcomp.algebra.ring_quotient]
ProperIdeal.Exports [module, in mathcomp.algebra.ring_quotient]
ProperIdeal.pack_ [definition, in mathcomp.algebra.ring_quotient]
ProperIdeal.phant_on_ [definition, in mathcomp.algebra.ring_quotient]
ProperIdeal.phant_clone [definition, in mathcomp.algebra.ring_quotient]
ProperIdeal.ring_quotient_isProperIdeal_mixin [projection, in mathcomp.algebra.ring_quotient]
ProperIdeal.sort [projection, in mathcomp.algebra.ring_quotient]
ProperIdeal.type [record, in mathcomp.algebra.ring_quotient]
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]
properP [lemma, in mathcomp.ssreflect.fintype]
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_neq [lemma, in mathcomp.ssreflect.finset]
proper_ideal_subproof [definition, in mathcomp.algebra.ring_quotient]
proper_ideal [definition, in mathcomp.algebra.ring_quotient]
proper_addv [definition, in mathcomp.algebra.vector]
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_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.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_pgFun [definition, in mathcomp.solvable.pgroup]
pseries_gFun [definition, in mathcomp.solvable.pgroup]
pseries_igFun [definition, 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 [definition, 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]
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]
push_invariant [definition, in mathcomp.ssreflect.path]
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.cyclotomic]
pZtoC [abbreviation, in mathcomp.field.algC]
pZtoC [abbreviation, in mathcomp.field.algnum]
pZtoQ [abbreviation, in mathcomp.algebra.intdiv]
pZtoQ [abbreviation, in mathcomp.field.cyclotomic]
pZtoQ [abbreviation, in mathcomp.field.algC]
pZtoQ [abbreviation, in mathcomp.field.algnum]
p_A [abbreviation, in mathcomp.algebra.mxpoly]
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_rank_abelian [lemma, in mathcomp.solvable.abelian]
p_rank_Ohm1 [lemma, in mathcomp.solvable.abelian]
p_rank_p'quotient [lemma, in mathcomp.solvable.abelian]
p_rank_dprod [lemma, in mathcomp.solvable.abelian]
p_rank_quotient [lemma, in mathcomp.solvable.abelian]
p_rank_le_rank [lemma, in mathcomp.solvable.abelian]
p_rank_pmaxElem_exists [lemma, in mathcomp.solvable.abelian]
p_rank_Hall [lemma, in mathcomp.solvable.abelian]
p_rank_Sylow [lemma, in mathcomp.solvable.abelian]
p_rankJ [lemma, in mathcomp.solvable.abelian]
p_rankElem_max [lemma, in mathcomp.solvable.abelian]
p_rankS [lemma, in mathcomp.solvable.abelian]
p_rank_abelem [lemma, in mathcomp.solvable.abelian]
p_rank_le_logn [lemma, in mathcomp.solvable.abelian]
p_rank1 [lemma, in mathcomp.solvable.abelian]
p_rank_gt0 [lemma, in mathcomp.solvable.abelian]
p_rank_geP [lemma, in mathcomp.solvable.abelian]
p_rank_witness [lemma, in mathcomp.solvable.abelian]
p_rank [definition, in mathcomp.solvable.abelian]
p_abelem_split1 [lemma, in mathcomp.solvable.maximal]
p_core_Fitting [lemma, in mathcomp.solvable.maximal]
p_index_maximal [lemma, in mathcomp.solvable.maximal]
p_maximal_index [lemma, in mathcomp.solvable.maximal]
p_maximal_normal [lemma, in mathcomp.solvable.maximal]
p'groupEpi [lemma, in mathcomp.solvable.pgroup]
p'group_quotient_cent_prime [lemma, in mathcomp.solvable.pgroup]
p'natE [lemma, in mathcomp.ssreflect.prime]
p'natEpi [lemma, in mathcomp.ssreflect.prime]
p'nat_coprime [lemma, in mathcomp.ssreflect.prime]
p'_elt_constt [lemma, in mathcomp.solvable.pgroup]
p1ElemE [lemma, in mathcomp.solvable.abelian]
p2Elem_dprodP [lemma, in mathcomp.solvable.abelian]
p2group_abelian [lemma, in mathcomp.solvable.sylow]
p3group_extraspecial [lemma, in mathcomp.solvable.maximal]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (54001 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1931 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1658 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7199 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15214 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (224 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (132 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2371 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2266 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (732 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21455 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (647 entries) |