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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |

## P

p [abbreviation, in zmodp]p [definition, in extremal]

p [abbreviation, in zmodp]

PackSocle [constructor, in mxrepresentation]

PackSocleK [lemma, in mxrepresentation]

pack_subFinType [definition, in fintype]

pack_subCountType [definition, in choice]

pairg1 [definition, in gproduct]

pairg1_morphism [definition, in gproduct]

pairg1_morphM [lemma, in gproduct]

pairmap [definition, in seq]

pairmapK [lemma, in seq]

pairmap_tuple [definition, in tuple]

pairmap_cat [lemma, in seq]

pairmap_tupleP [lemma, in tuple]

pair_of_sd [definition, in gproduct]

pair_of_section [definition, in jordanholder]

pair_big_dep [lemma, in bigop]

pair_eqP [lemma, in eqtype]

pair_of_tagK [lemma, in choice]

pair_big [lemma, in bigop]

pair_bigA [lemma, in bigop]

pair_eq1 [lemma, in eqtype]

pair_eqE [lemma, in eqtype]

pair_eq [definition, in eqtype]

pair_of_mxvec_index [definition, in matrix]

pair_eq2 [lemma, in eqtype]

pair_of_tag [definition, in choice]

pair1g [definition, in gproduct]

pair1g_morphism [definition, in gproduct]

pair1g_morphM [lemma, in gproduct]

partG_eq1 [lemma, in pgroup]

PartialAction [section, in action]

PartialAction.aT [variable, in action]

PartialAction.D [variable, in action]

PartialAction.OrbitStabilizer [section, in action]

PartialAction.OrbitStabilizer.G [variable, in action]

PartialAction.OrbitStabilizer.sGD [variable, in action]

PartialAction.OrbitStabilizer.x [variable, in action]

PartialAction.rT [variable, in action]

PartialAction.to [variable, in action]

PartialFunctorTheory [section, in gfunctor]

PartialFunctorTheory.BasicTheory [section, in gfunctor]

PartialFunctorTheory.BasicTheory.F [variable, in gfunctor]

PartialFunctorTheory.F1 [variable, in gfunctor]

PartialFunctorTheory.F2 [variable, in gfunctor]

PartialFunctorTheory.Modulo [section, in gfunctor]

PartialFunctorTheory.Modulo.F1 [variable, in gfunctor]

PartialFunctorTheory.Modulo.F2 [variable, in gfunctor]

partial_product [definition, in gproduct]

partition [definition, in finset]

Partitions [section, in finset]

Partitions.BigOps [section, in finset]

Partitions.BigOps.idx [variable, in finset]

Partitions.BigOps.op [variable, in finset]

Partitions.BigOps.R [variable, in finset]

Partitions.I [variable, in finset]

Partitions.Preim [section, in finset]

Partitions.Preim.f [variable, in finset]

Partitions.Preim.rT [variable, in finset]

Partitions.T [variable, in finset]

partition_big_imset [lemma, in finset]

partition_big [lemma, in bigop]

partn [definition, in prime]

partnC [lemma, in prime]

partnI [lemma, in prime]

partnNK [lemma, in prime]

partnT [lemma, in prime]

partn_gcd [lemma, in prime]

partn_exp [lemma, in prime]

partn_part [lemma, in prime]

partn_biglcm [lemma, in prime]

partn_exponentS [lemma, in abelian]

partn_lcm [lemma, in prime]

partn_dvd [lemma, in prime]

partn_eq1 [lemma, in prime]

partn_mul [lemma, in prime]

partn_biggcd [lemma, in prime]

partn_pi [lemma, in prime]

partn0 [lemma, in prime]

partn1 [lemma, in prime]

part_pnat_id [lemma, in prime]

part_pnat [lemma, in prime]

part_p'nat [lemma, in prime]

part_gt0 [lemma, in prime]

Pascal [lemma, in binomial]

path [definition, in path]

path [library]

pathP [lemma, in path]

Paths [section, in path]

Paths.n0 [variable, in path]

Paths.Path [section, in path]

Paths.Path.e [variable, in path]

Paths.Path.x0_cycle [variable, in path]

Paths.T [variable, in path]

path_cat [lemma, in path]

path_rev [lemma, in path]

path_connect [lemma, in fingraph]

path_setIgr [definition, in gseries]

path_sorted [lemma, in path]

path_merge [lemma, in path]

path_rcons [lemma, in path]

path_map [lemma, in path]

path_min_sorted [lemma, in path]

pcancel [definition, in ssrfun]

PcanChoiceMixin [definition, in choice]

PcanCountMixin [definition, in choice]

PcanEqMixin [definition, in eqtype]

PcanFinMixin [definition, in fintype]

pcan_inj [lemma, in ssrfun]

pcan_pcomp [lemma, in ssrfun]

pcan_enumP [lemma, in fintype]

pcan_pickleK [lemma, in choice]

pcomp [definition, in ssrfun]

pcore [definition, in pgroup]

PcoreDef [section, in pgroup]

PcoreDef.A [variable, in pgroup]

PcoreDef.gT [variable, in pgroup]

PcoreDef.pi [variable, in pgroup]

pcoreI [lemma, in pgroup]

pcoreJ [lemma, in pgroup]

pcoreNK [lemma, in pgroup]

PCoreProps [section, in pgroup]

PCoreProps.gT [variable, in pgroup]

PCoreProps.pi [variable, in pgroup]

pcoreS [lemma, in pgroup]

pcore_modp [lemma, in pgroup]

pcore_pgFun [definition, in pgroup]

pcore_gFun [definition, in pgroup]

pcore_igFun [definition, in pgroup]

pcore_mod_group [definition, in pgroup]

pcore_group [definition, in pgroup]

pcore_mod_res [lemma, in pgroup]

pcore_sub_Hall [lemma, in pgroup]

pcore_mod1 [lemma, in pgroup]

pcore_Fitting [lemma, in maximal]

pcore_mod [definition, in pgroup]

pcore_max [lemma, in pgroup]

pcore_psubgroup [lemma, in pgroup]

pcore_faithful_mx_irr [lemma, in mxabelem]

pcore_sub [lemma, in pgroup]

pcore_pgroup_id [lemma, in pgroup]

pcore_char [lemma, in pgroup]

pcore_mod_sub [lemma, in pgroup]

pcore_sub_rstab_mxsimple [lemma, in mxabelem]

pcore_sub_rker_mx_irr [lemma, in mxabelem]

pcore_normal [lemma, in pgroup]

pcore_pgroup [lemma, in pgroup]

pcore_faithful_irr_act [lemma, in sylow]

pcore_sub_astab_irr [lemma, in sylow]

pcore_setI_normal [lemma, in pgroup]

pcycle [definition, in perm]

pcycleE [lemma, in action]

pcycles [definition, in perm]

pcycle_id [lemma, in perm]

pcycle_traject [lemma, in perm]

pcycle_actperm [lemma, in action]

pcycle_sym [lemma, in perm]

pcycle_perm [lemma, in perm]

pdiv [definition, in prime]

pdivP [lemma, in prime]

pdiv_gt0 [lemma, in prime]

pdiv_min_dvd [lemma, in prime]

pdiv_leq [lemma, in prime]

pdiv_prime [lemma, in prime]

pdiv_pfactor [lemma, in prime]

pdiv_p_elt [lemma, in abelian]

pdiv_dvd [lemma, in prime]

pdiv_id [lemma, in prime]

pE [definition, in mxabelem]

pElem [definition, in abelian]

pElemI [lemma, in abelian]

pElemJ [lemma, in abelian]

pElemP [lemma, in abelian]

pElemS [lemma, in abelian]

Perm [constructor, in perm]

perm [abbreviation, in perm]

perm [library]

PermAction [section, in action]

PermAction.rT [variable, in action]

PermDef [module, in perm]

PermDefSection [section, in perm]

PermDefSection.T [variable, in perm]

PermDefSig [module, in perm]

PermDefSig.fun_of_permE [axiom, in perm]

PermDefSig.fun_of_perm [axiom, in perm]

PermDefSig.perm [axiom, in perm]

PermDefSig.permE [axiom, in perm]

PermDef.fun_of_perm [definition, in perm]

PermDef.fun_of_permE [lemma, in perm]

PermDef.perm [definition, in perm]

PermDef.permE [lemma, in perm]

permE [lemma, in perm]

PermIn [section, in automorphism]

PermIn.A [variable, in automorphism]

PermIn.f [variable, in automorphism]

PermIn.injf [variable, in automorphism]

PermIn.sBf [variable, in automorphism]

PermIn.T [variable, in automorphism]

permJ [lemma, in perm]

permK [lemma, in perm]

permKV [lemma, in perm]

permM [lemma, in perm]

permP [lemma, in perm]

PermSeq [section, in seq]

PermSeq.T [variable, in seq]

PermutationParity [section, in perm]

PermutationParity.T [variable, in perm]

permX [lemma, in perm]

perm_mx [definition, in matrix]

perm_eqP [lemma, in seq]

perm_inj [lemma, in perm]

perm_cat2r [lemma, in seq]

perm_cat2l [lemma, in seq]

perm_oneP [lemma, in perm]

perm_eqrP [lemma, in seq]

perm_on [definition, in perm]

perm_of_finGroupType [definition, in perm]

perm_of_baseFinGroupType [definition, in perm]

perm_finGroupType [definition, in perm]

perm_baseFinGroupType [definition, in perm]

perm_unlock [definition, in perm]

perm_for_subFinType [definition, in perm]

perm_for_finType [definition, in perm]

perm_for_subCountType [definition, in perm]

perm_for_countType [definition, in perm]

perm_for_choiceType [definition, in perm]

perm_for_eqType [definition, in perm]

perm_for_subType [definition, in perm]

perm_subFinType [definition, in perm]

perm_finType [definition, in perm]

perm_subCountType [definition, in perm]

perm_countType [definition, in perm]

perm_choiceType [definition, in perm]

perm_eqType [definition, in perm]

perm_subType [definition, in perm]

perm_faithful [lemma, in action]

perm_eqlP [lemma, in seq]

perm_finMixin [definition, in perm]

perm_type [inductive, in perm]

perm_mx_is_perm [lemma, in matrix]

perm_countMixin [definition, in perm]

perm_inv [definition, in perm]

perm_mulP [lemma, in perm]

perm_one [definition, in perm]

perm_onM [lemma, in perm]

perm_mx1 [lemma, in matrix]

perm_mxM [lemma, in matrix]

perm_catAC [lemma, in seq]

perm_sort [lemma, in path]

perm_invK [lemma, in perm]

perm_mact [lemma, in action]

perm_uniq [lemma, in seq]

perm_filterC [lemma, in seq]

perm_onto [lemma, in perm]

perm_eqr [abbreviation, in seq]

perm_in [definition, in automorphism]

perm_choiceMixin [definition, in perm]

perm_cons [lemma, in seq]

perm_eq_uniq [lemma, in seq]

perm_proof [lemma, in perm]

perm_eq [definition, in seq]

perm_eql [abbreviation, in seq]

perm_eq_size [lemma, in seq]

perm_sortP [lemma, in path]

perm_eq_refl [lemma, in seq]

perm_closed [lemma, in perm]

perm_inE [lemma, in automorphism]

perm_act1P [lemma, in action]

perm_invP [lemma, in perm]

perm_eq_trans [lemma, in seq]

perm_eqMixin [definition, in perm]

perm_of [definition, in perm]

perm_catC [lemma, in seq]

perm_mul [definition, in perm]

perm_on1 [lemma, in perm]

perm_action [definition, in action]

perm_def [abbreviation, in perm]

perm_merge [lemma, in path]

perm_eq_mem [lemma, in seq]

perm_mxV [lemma, in matrix]

perm_rot [lemma, in seq]

perm_eq_abelian_type [lemma, in abelian]

perm_in_on [lemma, in automorphism]

perm_in_inj [lemma, in automorphism]

perm_rcons [lemma, in seq]

perm_of_baseFinGroupMixin [definition, in perm]

perm_eql [abbreviation, in seq]

perm_eq_sym [lemma, in seq]

perm_eqr [abbreviation, in seq]

perm_catCA [lemma, in seq]

perm_rotr [lemma, in seq]

perm1 [lemma, in perm]

PervasiveMonoids [section, in bigop]

Pextraspecial [module, in extraspecial]

Pextraspecial.act [definition, in extraspecial]

Pextraspecial.action [definition, in extraspecial]

Pextraspecial.actP [lemma, in extraspecial]

Pextraspecial.Construction [section, in extraspecial]

Pextraspecial.Construction.p [variable, in extraspecial]

Pextraspecial.gactP [lemma, in extraspecial]

Pextraspecial.groupAction [definition, in extraspecial]

Pextraspecial.gtype [definition, in extraspecial]

Pextraspecial.ngtype [definition, in extraspecial]

Pextraspecial.ngtypeQ [definition, in extraspecial]

pfactor [definition, in prime]

pfactorK [lemma, in prime]

pfactorKpdiv [lemma, in prime]

pfactor_dvdn [lemma, in prime]

pfactor_coprime [lemma, in prime]

pfactor_gt0 [lemma, in prime]

pfactor_dvdnn [lemma, in prime]

pfamily [definition, in finfun]

pfamilyP [lemma, in finfun]

pffun_on [definition, in finfun]

pffun_onP [lemma, in finfun]

pgroup [definition, in pgroup]

pgroup [library]

PgroupDefs [section, in pgroup]

PgroupDefs.gT [variable, in pgroup]

pgroupE [lemma, in pgroup]

pgroupJ [lemma, in pgroup]

pgroupM [lemma, in pgroup]

pgroupNK [lemma, in pgroup]

pgroupP [lemma, in pgroup]

PgroupProps [section, in pgroup]

PgroupProps.gT [variable, in pgroup]

pgroupS [lemma, in pgroup]

pgroup_pi [lemma, in pgroup]

pgroup_nil [lemma, in sylow]

pgroup_p [lemma, in pgroup]

pgroup_sol [lemma, in sylow]

pgroup_fix_mod [lemma, in sylow]

pgroup_pdiv [lemma, in pgroup]

pgroup1 [lemma, in pgroup]

ph [abbreviation, in ssrbool]

ph [abbreviation, in ssrbool]

pHall [definition, in pgroup]

pHallE [lemma, in pgroup]

pHallJ [lemma, in pgroup]

pHallJnorm [lemma, in pgroup]

pHallJ2 [lemma, in pgroup]

pHallNK [lemma, in pgroup]

pHallP [lemma, in pgroup]

pHall_id [lemma, in pgroup]

pHall_subl [lemma, in pgroup]

pHall_Hall [lemma, in pgroup]

pHall_sub [lemma, in pgroup]

pHall_pgroup [lemma, in pgroup]

Phant [constructor, in ssreflect]

phant [inductive, in ssreflect]

phantom [inductive, in ssreflect]

Phantom [constructor, in ssreflect]

phant_id [definition, in ssrfun]

phi [definition, in prime]

phiE [lemma, in prime]

PhiJ [lemma, in maximal]

PhiS [lemma, in maximal]

Phi_quotient_id [lemma, in maximal]

Phi_proper [lemma, in maximal]

phi_gen [lemma, in cyclic]

Phi_normal [lemma, in maximal]

Phi_quotient_cyclic [lemma, in maximal]

phi_coprime [lemma, in prime]

Phi_min [lemma, in maximal]

phi_pfactor [lemma, in prime]

Phi_mulg [lemma, in maximal]

Phi_char [lemma, in maximal]

Phi_nongen [lemma, in maximal]

Phi_cprod [lemma, in maximal]

phi_gt0 [lemma, in prime]

Phi_joing [lemma, in maximal]

Phi_quotient_abelem [lemma, in maximal]

Phi_sub_max [lemma, in maximal]

Phi_sub [lemma, in maximal]

phi_count_coprime [lemma, in prime]

Pick [constructor, in fintype]

pick [definition, in fintype]

pickle [definition, in choice]

pickleK [lemma, in choice]

pickleK_inv [lemma, in choice]

pickle_inv [definition, in choice]

pickle_invK [lemma, in choice]

pickP [lemma, in fintype]

pick_spec [inductive, in fintype]

pid_mx_block [lemma, in matrix]

pid_mx [definition, in matrix]

pid_mx_id [lemma, in matrix]

pid_mx_minv [lemma, in matrix]

pid_mx_1 [lemma, in matrix]

pid_mx_col [lemma, in matrix]

pid_mx_minh [lemma, in matrix]

pid_mx_row [lemma, in matrix]

pid_mx_0 [lemma, in matrix]

PiNat [section, in prime]

pinvmx [definition, in mxalgebra]

piOhm1 [lemma, in abelian]

piSg [lemma, in fingroup]

pi_of_prime [lemma, in prime]

pi_max_pdiv [lemma, in prime]

pi_of_partn [lemma, in prime]

pi_arg_of_fin_pred [definition, in prime]

pi_arg_of_nat [definition, in prime]

pi_of [definition, in prime]

pi_pnat [lemma, in prime]

pi_pdiv [lemma, in prime]

pi_wrapped_arg [definition, in prime]

pi_of_muln [lemma, in prime]

pi_of_exponent [lemma, in abelian]

pi_center_nilpotent [lemma, in sylow]

pi_p'nat [lemma, in prime]

pi_of_exp [lemma, in prime]

pi_unwrapped_arg [definition, in prime]

pi_p'group [lemma, in pgroup]

pi_pgroup [lemma, in pgroup]

pi_of_dvd [lemma, in prime]

pi'_p'group [lemma, in pgroup]

pi'_p'nat [lemma, in prime]

PlainTheory [section, in finfun]

PlainTheory.aT [variable, in finfun]

PlainTheory.Family [section, in finfun]

PlainTheory.Family.F [variable, in finfun]

PlainTheory.rT [variable, in finfun]

plusE [lemma, in ssrnat]

pmap [definition, in seq]

Pmap [section, in seq]

pmapS_filter [lemma, in seq]

Pmapub [section, in seq]

Pmapub.p [variable, in seq]

Pmapub.sT [variable, in seq]

Pmapub.T [variable, in seq]

pmap_uniq [lemma, in seq]

pmap_filter [lemma, in seq]

pmap_sub_uniq [lemma, in seq]

Pmap.aT [variable, in seq]

Pmap.f [variable, in seq]

Pmap.fK [variable, in seq]

Pmap.g [variable, in seq]

Pmap.rT [variable, in seq]

PMax [section, in maximal]

pmaxElem [definition, in abelian]

pmaxElemJ [lemma, in abelian]

pmaxElemP [lemma, in abelian]

pmaxElemS [lemma, in abelian]

pmaxElem_LdivP [lemma, in abelian]

pmaxElem_exists [lemma, in abelian]

pmaxElem_extraspecial [lemma, in maximal]

PMax.gT [variable, in maximal]

PMax.M [variable, in maximal]

PMax.p [variable, in maximal]

PMax.P [variable, in maximal]

PMax.pP [variable, in maximal]

pmorphimF [lemma, in gfunctor]

pmorphim_pgroup [lemma, in pgroup]

pmorphim_pHall [lemma, in pgroup]

pnat [definition, in prime]

pnatE [lemma, in prime]

pnatI [lemma, in prime]

pnatNK [lemma, in prime]

pnatP [lemma, in prime]

pnatPpi [lemma, in prime]

pnat_div [lemma, in prime]

pnat_coprime [lemma, in prime]

pnat_1 [lemma, in prime]

pnat_mul [lemma, in prime]

pnat_dvd [lemma, in prime]

pnat_exponent [lemma, in abelian]

pnat_exp [lemma, in prime]

pnat_id [lemma, in prime]

pnat_pi [lemma, in prime]

pnElem [definition, in abelian]

pnElemE [lemma, in abelian]

pnElemI [lemma, in abelian]

pnElemJ [lemma, in abelian]

pnElemP [lemma, in abelian]

pnElemPcard [lemma, in abelian]

pnElemS [lemma, in abelian]

pnElem_prime [lemma, in abelian]

pnElem0 [lemma, in abelian]

Poly [definition, in poly]

poly [library]

polyC [definition, in poly]

PolyCompose [section, in poly]

PolyCompose.R [variable, in poly]

polyC_rmorphism [definition, in poly]

polyC_additive [definition, in poly]

polyC_opp [lemma, in poly]

polyC_exp [lemma, in poly]

polyC_eq0 [lemma, in poly]

polyC_natmul [lemma, in poly]

polyC_inj [lemma, in poly]

polyC_add [lemma, in poly]

polyC_is_rmorphism [lemma, in poly]

polyC_mul [lemma, in poly]

polyC_sub [lemma, in poly]

polyC0 [lemma, in poly]

polyC1 [lemma, in poly]

PolyK [lemma, in poly]

Polynomial [constructor, in poly]

Polynomial [section, in poly]

polynomial [record, in poly]

PolynomialComRing [section, in poly]

PolynomialComRing.R [variable, in poly]

PolynomialIdomain [section, in poly]

PolynomialIdomain.R [variable, in poly]

PolynomialTheory [section, in poly]

PolynomialTheory.R [variable, in poly]

polynomial_idomainType [definition, in poly]

polynomial_comUnitRingType [definition, in poly]

polynomial_unitAlgType [definition, in poly]

polynomial_unitRingType [definition, in poly]

polynomial_algType [definition, in poly]

polynomial_comRingType [definition, in poly]

polynomial_lalgType [definition, in poly]

polynomial_lmodType [definition, in poly]

polynomial_ringType [definition, in poly]

polynomial_zmodType [definition, in poly]

polynomial_choiceType [definition, in poly]

polynomial_eqType [definition, in poly]

polynomial_subType [definition, in poly]

polynomial_choiceMixin [definition, in poly]

polynomial_eqMixin [definition, in poly]

Polynomial.R [variable, in poly]

polyP [lemma, in poly]

polyseq [projection, in poly]

polyseqC [lemma, in poly]

polyseqK [lemma, in poly]

polyseqX [lemma, in poly]

polyseq_cons [lemma, in poly]

polyseq_poly [lemma, in poly]

polyseq1 [lemma, in poly]

polySpred [lemma, in poly]

polyX [definition, in poly]

poly_unit [definition, in poly]

poly_rV_is_linear [lemma, in mxpoly]

poly_mulC [lemma, in poly]

poly_idomainMixin [lemma, in poly]

poly_comp_scall [lemma, in poly]

poly_unitRingMixin [definition, in poly]

poly_ind [lemma, in poly]

poly_cons_def [lemma, in poly]

poly_comp_addl [lemma, in poly]

poly_of [definition, in poly]

poly_comp_rmorphism [definition, in poly]

poly_comp_linear [definition, in poly]

poly_comp_additive [definition, in poly]

poly_idomainType [definition, in poly]

poly_comUnitRingType [definition, in poly]

poly_unitAlgType [definition, in poly]

poly_unitRingType [definition, in poly]

poly_algType [definition, in poly]

poly_comRingType [definition, in poly]

poly_lalgType [definition, in poly]

poly_lmodType [definition, in poly]

poly_lmodMixin [definition, in poly]

poly_ringType [definition, in poly]

poly_zmodType [definition, in poly]

poly_choiceType [definition, in poly]

poly_eqType [definition, in poly]

poly_subType [definition, in poly]

poly_compA [lemma, in poly]

poly_comp_is_additive [lemma, in poly]

poly_comp_subl [lemma, in poly]

poly_cons [definition, in poly]

poly_compE [lemma, in poly]

poly_initial [lemma, in poly]

poly_com0p [lemma, in poly]

poly_rV [definition, in mxpoly]

poly_comp_amulX [lemma, in poly]

poly_comp_rmorphr [lemma, in poly]

poly_comXp [lemma, in poly]

poly_compC [lemma, in poly]

poly_comp_mull [lemma, in poly]

poly_comp0 [lemma, in poly]

poly_inv [definition, in poly]

poly_mulVp [lemma, in poly]

poly_comp_translateK [lemma, in poly]

poly_comp [definition, in poly]

poly_zmodMixin [definition, in poly]

poly_inj [lemma, in poly]

poly_compX [lemma, in poly]

poly_intro_unit [lemma, in poly]

poly_inv_out [lemma, in poly]

poly_def [lemma, in poly]

poly_rV_linear [definition, in mxpoly]

poly_rV_additive [definition, in mxpoly]

poly_morphX_comm [lemma, in poly]

poly_rV_K [lemma, in mxpoly]

poly_ringMixin [definition, in poly]

poly_comp_is_linear [lemma, in poly]

poly0Vpos [lemma, in poly]

pop_succn [definition, in ssrnat]

PosNotEq0 [constructor, in ssrnat]

posnP [lemma, in ssrnat]

pos_of_nat [definition, in ssrnat]

powerset [definition, in finfun]

powers_mx [definition, in mxpoly]

pprod [abbreviation, in gproduct]

pprod [abbreviation, in gproduct]

pprodE [lemma, in gproduct]

pprodEY [lemma, in gproduct]

pprodg1 [lemma, in gproduct]

pprodm [definition, in gproduct]

pprodmE [lemma, in gproduct]

pprodmEl [lemma, in gproduct]

pprodmEr [lemma, in gproduct]

pprodmM [lemma, in gproduct]

pprodm_morphism [definition, in gproduct]

pprodP [lemma, in gproduct]

pprod1g [lemma, in gproduct]

Pquotient [section, in pgroup]

pquotient_pHall [lemma, in pgroup]

pquotient_pcore [lemma, in pgroup]

pquotient_pgroup [lemma, in pgroup]

Pquotient.G [variable, in pgroup]

Pquotient.gT [variable, in pgroup]

Pquotient.H [variable, in pgroup]

Pquotient.K [variable, in pgroup]

Pquotient.p [variable, in pgroup]

Pquotient.pi [variable, in pgroup]

Pquotient.piK [variable, in pgroup]

pred [definition, in ssrbool]

predArgType [definition, in ssrbool]

predC [definition, in ssrbool]

predC_closed [lemma, in fingraph]

predC1 [definition, in eqtype]

predD [definition, in ssrbool]

predD1 [definition, in eqtype]

predD1P [lemma, in eqtype]

predE [lemma, in ssrnat]

predI [definition, in ssrbool]

Predicates [section, in ssrbool]

Predicates.T [variable, in ssrbool]

predn [definition, in ssrnat]

prednK [lemma, in ssrnat]

predn_subS [lemma, in ssrnat]

predn_exp [lemma, in binomial]

predn_sub [lemma, in ssrnat]

predPredType [definition, in ssrbool]

predT [definition, in ssrbool]

PredType [constructor, in ssrbool]

predType [record, in ssrbool]

predT_subset [lemma, in fintype]

predU [definition, in ssrbool]

predU1 [definition, in eqtype]

predU1l [lemma, in eqtype]

predU1P [lemma, in eqtype]

predU1r [lemma, in eqtype]

predX [definition, in eqtype]

predX_prod_enum [lemma, in fintype]

pred_class [abbreviation, in ssrbool]

pred_of_set_unlock [definition, in finset]

pred_sort [projection, in ssrbool]

pred_of_set_def [abbreviation, in finset]

pred_of_set [abbreviation, in finset]

pred_of_eq_seq [definition, in seq]

pred_of_mem_pred [definition, in ssrbool]

pred_of_argType [definition, in ssrbool]

pred_of_mem [definition, in ssrbool]

pred_of_simpl [definition, in ssrbool]

pred0 [definition, in ssrbool]

pred0b [definition, in fintype]

pred0P [lemma, in fintype]

pred0Pn [lemma, in fintype]

pred1 [definition, in eqtype]

pred1E [lemma, in eqtype]

pred2 [definition, in eqtype]

pred2P [lemma, in eqtype]

pred3 [definition, in eqtype]

pred4 [definition, in eqtype]

PreGroupIdentities [section, in fingroup]

PreGroupIdentities.T [variable, in fingroup]

preim [definition, in ssrbool]

preimset [definition, in finset]

preimsetC [lemma, in finset]

preimsetD [lemma, in finset]

preimsetI [lemma, in finset]

preimsetS [lemma, in finset]

preimsetT [lemma, in finset]

preimsetU [lemma, in finset]

preimset_proper [lemma, in finset]

preimset0 [lemma, in finset]

preim_at [definition, in finset]

preim_permV [lemma, in perm]

preim_partitionP [lemma, in finset]

preim_partition [definition, in finset]

preim_iinv [lemma, in fintype]

preim_seq [definition, in fintype]

preim_autE [lemma, in automorphism]

Presentation [module, in presentation]

presentation [library]

PresentationTheory [section, in presentation]

Presentation.And [constructor, in presentation]

Presentation.and_rel [definition, in presentation]

Presentation.bool_of_rel [definition, in presentation]

Presentation.Cast [definition, in presentation]

Presentation.Comm [constructor, in presentation]

Presentation.Conj [constructor, in presentation]

Presentation.Cst [constructor, in presentation]

Presentation.Env [constructor, in presentation]

Presentation.env [inductive, in presentation]

Presentation.env1 [definition, in presentation]

Presentation.Eq1 [definition, in presentation]

Presentation.Eq2 [constructor, in presentation]

Presentation.Eq3 [definition, in presentation]

Presentation.eval [definition, in presentation]

Presentation.Exp [constructor, in presentation]

Presentation.Formula [constructor, in presentation]

Presentation.formula [inductive, in presentation]

Presentation.Generator [constructor, in presentation]

Presentation.hom [definition, in presentation]

Presentation.Idx [constructor, in presentation]

Presentation.Inv [constructor, in presentation]

Presentation.iso [definition, in presentation]

Presentation.Mul [constructor, in presentation]

Presentation.NoRel [constructor, in presentation]

Presentation.Presentation [section, in presentation]

Presentation.rel [definition, in presentation]

Presentation.Rel [constructor, in presentation]

Presentation.rel_type [inductive, in presentation]

Presentation.sat [definition, in presentation]

Presentation.term [inductive, in presentation]

Presentation.type [inductive, in presentation]

prev [definition, in path]

prev_at [definition, in path]

prev_cycle [lemma, in path]

prev_rev [lemma, in path]

prev_rotr [lemma, in path]

prev_nth [lemma, in path]

prev_rot [lemma, in path]

prev_map [lemma, in path]

prev_next [lemma, in path]

pre_symmetric [definition, in ssrbool]

pre_image [lemma, in fintype]

prime [definition, in prime]

prime [library]

PrimeField [section, in zmodp]

PrimeField.F_prime [section, in zmodp]

PrimeField.F_prime.p_pr [variable, in zmodp]

PrimeField.p [variable, in zmodp]

primeP [lemma, in prime]

primePn [lemma, in prime]

primePns [lemma, in prime]

primes [definition, in prime]

primes_mul [lemma, in prime]

primes_prime [lemma, in prime]

primes_exp [lemma, in prime]

primes_exponent [lemma, in abelian]

primes_uniq [lemma, in prime]

primes_part [lemma, in prime]

prime_TIg [lemma, in fingroup]

prime_nt_dvdP [lemma, in prime]

prime_subgroupVti [lemma, in pgroup]

prime_decomp [definition, in prime]

prime_decomp [section, in prime]

prime_gt0 [lemma, in prime]

prime_meetG [lemma, in fingroup]

prime_coprime [lemma, in prime]

prime_dvd_bin [lemma, in binomial]

prime_decomp_rec [definition, in prime]

prime_gt1 [lemma, in prime]

prime_decomp_correct [lemma, in prime]

prime_Ohm1P [lemma, in extremal]

prime_abelem [lemma, in abelian]

prime_oddPn [lemma, in prime]

prime_cyclic [lemma, in cyclic]

prime_decompE [lemma, in prime]

Primitive [section, in primitive_action]

primitive [definition, in primitive_action]

PrimitiveDef [section, in primitive_action]

PrimitiveDef.A [variable, in primitive_action]

PrimitiveDef.aT [variable, in primitive_action]

PrimitiveDef.S [variable, in primitive_action]

PrimitiveDef.sT [variable, in primitive_action]

PrimitiveDef.to [variable, in primitive_action]

PrimitiveRoots [section, in cyclic]

primitive_root_of_unity [definition, in poly]

primitive_root_splitting_abelian [lemma, in mxrepresentation]

primitive_action [library]

Primitive.aT [variable, in primitive_action]

Primitive.G [variable, in primitive_action]

Primitive.S [variable, in primitive_action]

Primitive.sT [variable, in primitive_action]

Primitive.to [variable, in primitive_action]

prim_trans_norm [lemma, in primitive_action]

prim_order_dvd [lemma, in poly]

prim_expr_mod [lemma, in poly]

prim_expr_order [lemma, in poly]

prim_order_exists [lemma, in poly]

prim_order_gt0 [lemma, in poly]

prim_rootP [lemma, in poly]

principal_comp [definition, in mxrepresentation]

principal_comp_subproof [lemma, in mxrepresentation]

ProdEqType [section, in eqtype]

ProdEqType.T1 [variable, in eqtype]

ProdEqType.T2 [variable, in eqtype]

ProdFinType [section, in fintype]

ProdFinType.T1 [variable, in fintype]

ProdFinType.T2 [variable, in fintype]

ProdMorph [section, in gproduct]

ProdMorph.Cprodm [section, in gproduct]

ProdMorph.Cprodm.cfHK [variable, in gproduct]

ProdMorph.Cprodm.eqfHK [variable, in gproduct]

ProdMorph.Cprodm.eqHK_G [variable, in gproduct]

ProdMorph.Cprodm.fH [variable, in gproduct]

ProdMorph.Cprodm.fK [variable, in gproduct]

ProdMorph.Cprodm.G [variable, in gproduct]

ProdMorph.Cprodm.H [variable, in gproduct]

ProdMorph.Cprodm.K [variable, in gproduct]

ProdMorph.defs [section, in gproduct]

ProdMorph.defs.A [variable, in gproduct]

ProdMorph.defs.B [variable, in gproduct]

ProdMorph.defs.fA [variable, in gproduct]

ProdMorph.defs.fB [variable, in gproduct]

ProdMorph.Dprodm [section, in gproduct]

ProdMorph.Dprodm.cfHK [variable, in gproduct]

ProdMorph.Dprodm.eqHK_G [variable, in gproduct]

ProdMorph.Dprodm.fH [variable, in gproduct]

ProdMorph.Dprodm.fK [variable, in gproduct]

ProdMorph.Dprodm.G [variable, in gproduct]

ProdMorph.Dprodm.H [variable, in gproduct]

ProdMorph.Dprodm.K [variable, in gproduct]

ProdMorph.gT [variable, in gproduct]

ProdMorph.Props [section, in gproduct]

ProdMorph.Props.actf [variable, in gproduct]

ProdMorph.Props.eqfHK [variable, in gproduct]

ProdMorph.Props.fH [variable, in gproduct]

ProdMorph.Props.fK [variable, in gproduct]

ProdMorph.Props.H [variable, in gproduct]

ProdMorph.Props.K [variable, in gproduct]

ProdMorph.Props.nHK [variable, in gproduct]

ProdMorph.rT [variable, in gproduct]

ProdMorph.Sdprodm [section, in gproduct]

ProdMorph.Sdprodm.actf [variable, in gproduct]

ProdMorph.Sdprodm.eqHK_G [variable, in gproduct]

ProdMorph.Sdprodm.fH [variable, in gproduct]

ProdMorph.Sdprodm.fK [variable, in gproduct]

ProdMorph.Sdprodm.G [variable, in gproduct]

ProdMorph.Sdprodm.H [variable, in gproduct]

ProdMorph.Sdprodm.K [variable, in gproduct]

prodn_cond_gt0 [lemma, in bigop]

prodn_gt0 [lemma, in bigop]

prodsgP [lemma, in fingroup]

Product [section, in center]

Product.gT [variable, in center]

prodVector [definition, in vector]

ProdVector [section, in vector]

ProdVector.K [variable, in vector]

ProdVector.V [variable, in vector]

ProdVector.W [variable, in vector]

prod_group [definition, in gproduct]

prod_tpermP [lemma, in perm]

prod_finType [definition, in fintype]

prod_constt [lemma, in pgroup]

prod_countMixin [definition, in choice]

prod_prime_decomp [lemma, in prime]

prod_factors_of_unity [lemma, in poly]

prod_choiceMixin [definition, in choice]

prod_enumP [lemma, in fintype]

prod_eqMixin [definition, in eqtype]

prod_finMixin [definition, in fintype]

prod_factors_monic [lemma, in poly]

prod_eqType [definition, in eqtype]

prod_countType [definition, in choice]

prod_choiceType [definition, in choice]

prod_enum [definition, in fintype]

prod_nat_const_nat [lemma, in bigop]

prod_nat_const [lemma, in bigop]

Projection [section, in vector]

Projection.K [variable, in vector]

Projection.Sumv_Pi [section, in vector]

Projection.Sumv_Pi.P [variable, in vector]

Projection.Sumv_Pi.I [variable, in vector]

Projection.Sumv_Pi.V_ [variable, in vector]

Projection.V [variable, in vector]

projv [definition, in vector]

projv_id [lemma, in vector]

proj_mx_0 [lemma, in mxalgebra]

proj_mx_compl_sub [lemma, in mxalgebra]

proj_mx [definition, in mxalgebra]

proj_mx_id [lemma, in mxalgebra]

proj_mx_hom [lemma, in mxrepresentation]

proj_factmodS [lemma, in mxrepresentation]

proj_mx_sub [lemma, in mxalgebra]

proj_mx_proj [lemma, in mxalgebra]

proper [definition, in fintype]

properD [lemma, in finset]

properD1 [lemma, in finset]

properE [lemma, in fintype]

properEcard [lemma, in finset]

properEneq [lemma, in finset]

properG_ltn_log [lemma, in pgroup]

properI [lemma, in finset]

properIl [lemma, in finset]

properIr [lemma, in finset]

properIset [lemma, in finset]

properJ [lemma, in fingroup]

ProperMxsum [constructor, in mxalgebra]

ProperMxsumExpr [constructor, in mxalgebra]

properP [lemma, in fintype]

ProperSumv [constructor, in vector]

ProperSumvExpr [constructor, in vector]

properT [lemma, in finset]

PropertiesDefs [section, in nilpotent]

PropertiesDefs.A [variable, in nilpotent]

PropertiesDefs.gT [variable, in nilpotent]

properU [lemma, in finset]

properUl [lemma, in finset]

properUr [lemma, in finset]

properxx [lemma, in fintype]

proper_mxsum_rank [projection, in mxalgebra]

proper_sub [lemma, in fintype]

proper_neq [lemma, in finset]

proper_mxsumP [definition, in mxalgebra]

proper_subn [lemma, in fintype]

proper_irrefl [lemma, in fintype]

proper_trans [lemma, in fintype]

proper_sub_trans [lemma, in fintype]

proper_card [lemma, in fintype]

proper_mxsum_val [projection, in mxalgebra]

proper_addvP [definition, in vector]

proper_addv_val [projection, in vector]

proper_addv_dim [projection, in vector]

proper_addv_expr [record, in vector]

proper_mxsum_expr [record, in mxalgebra]

proper0 [lemma, in finset]

proper1G [lemma, in fingroup]

proper1set [lemma, in finset]

prop_congr [lemma, in ssrbool]

prop_in3 [definition, in ssrbool]

prop_in111 [definition, in ssrbool]

prop_in21 [definition, in ssrbool]

prop_on1 [definition, in ssrbool]

prop_in12 [definition, in ssrbool]

prop_for [definition, in ssrbool]

prop_on2 [definition, in ssrbool]

prop_in11 [definition, in ssrbool]

prop_in1 [definition, in ssrbool]

prop_in2 [definition, in ssrbool]

protect_term [definition, in ssreflect]

pseries [definition, in pgroup]

PseriesDefs [section, in pgroup]

PseriesDefs.A [variable, in pgroup]

PseriesDefs.gT [variable, in pgroup]

PseriesDefs.pis [variable, in pgroup]

pseriesJ [lemma, in pgroup]

pseriesS [lemma, in pgroup]

pseries_pgFun [definition, in pgroup]

pseries_gFun [definition, in pgroup]

pseries_igFun [definition, in pgroup]

pseries_group [definition, in pgroup]

pseries_subfun [lemma, in pgroup]

pseries_char_catr [lemma, in pgroup]

pseries_rcons_id [lemma, in pgroup]

pseries_norm2 [lemma, in pgroup]

pseries_rcons [lemma, in pgroup]

pseries_catl_id [lemma, in pgroup]

pseries_pop2 [lemma, in pgroup]

pseries_sub_catl [lemma, in pgroup]

pseries_char [lemma, in pgroup]

pseries_catr_id [lemma, in pgroup]

pseries_char_catl [lemma, in pgroup]

pseries_normal [lemma, in pgroup]

pseries_sub_catr [lemma, in pgroup]

pseries_sub [lemma, in pgroup]

pseries_pop [lemma, in pgroup]

pseries_group_set [lemma, in pgroup]

pseries1 [lemma, in pgroup]

psubgroup [definition, in pgroup]

psubgroupJ [lemma, in pgroup]

psubgroup1 [lemma, in pgroup]

pT [abbreviation, in perm]

pvaddE [lemma, in vector]

pval [definition, in perm]

pvalE [lemma, in perm]

pvf [definition, in vector]

pvfK [lemma, in vector]

pvoppE [lemma, in vector]

pvscaleE [lemma, in vector]

pv2p [definition, in vector]

pv2pK [lemma, in vector]

pX1p2id [lemma, in extraspecial]

pX1p2n_pgroup [lemma, in extraspecial]

pX1p2n_extraspecial [lemma, in extraspecial]

pX1p2S [lemma, in extraspecial]

pX1p2_extraspecial [lemma, in extraspecial]

pX1p2_pgroup [lemma, in extraspecial]

pZ [definition, in maximal]

p_rankElem_max [lemma, in abelian]

p_elt_exp [lemma, in pgroup]

p_elt_constt [lemma, in pgroup]

p_group1 [lemma, in pgroup]

p_abelem_split1 [lemma, in maximal]

p_maximal_normal [lemma, in maximal]

p_rankJ [lemma, in abelian]

p_rank_abelem [lemma, in abelian]

p_group [definition, in pgroup]

p_natP [lemma, in prime]

p_elt [definition, in pgroup]

p_eltM_norm [lemma, in pgroup]

p_rank_witness [lemma, in abelian]

p_rank_le_logn [lemma, in abelian]

p_Sylow [lemma, in pgroup]

p_part_eq1 [lemma, in prime]

p_rank_pmaxElem_exists [lemma, in abelian]

p_rank [definition, in abelian]

p_rank_abelian [lemma, in abelian]

p_rank_geP [lemma, in abelian]

p_A [abbreviation, in mxpoly]

p_gt1 [definition, in maximal]

p_eltNK [lemma, in pgroup]

p_groupP [lemma, in pgroup]

p_eltJ [lemma, in pgroup]

p_gt0 [definition, in mxabelem]

p_eltX [lemma, in pgroup]

p_rank_gt0 [lemma, in abelian]

p_part_gt1 [lemma, in prime]

p_rank_Hall [lemma, in abelian]

p_gt1 [definition, in mxabelem]

p_rank1 [lemma, in abelian]

p_gt0 [definition, in maximal]

p_index_maximal [lemma, in maximal]

p_pr [definition, in mxabelem]

p_gt1 [definition, in extremal]

p_maximal_index [lemma, in maximal]

p_pr [definition, in maximal]

p_rank_p'quotient [lemma, in abelian]

p_rank_quotient [lemma, in abelian]

p_rank_Ohm1 [lemma, in abelian]

p_gt1 [definition, in extraspecial]

p_rank_le_rank [lemma, in abelian]

p_core_Fitting [lemma, in maximal]

p_elt1 [lemma, in pgroup]

p_pr [definition, in maximal]

p_eltM [lemma, in pgroup]

p_gt0 [definition, in extremal]

p_eltV [lemma, in pgroup]

p_pr [definition, in mxabelem]

p_part [lemma, in prime]

p_rank_Sylow [lemma, in abelian]

p_rankS [lemma, in abelian]

p_gt0 [definition, in extraspecial]

p_rank_dprod [lemma, in abelian]

p_groupJ [lemma, in pgroup]

p'groupEpi [lemma, in pgroup]

p'group_quotient_cent_prime [lemma, in pgroup]

p'natE [lemma, in prime]

p'natEpi [lemma, in prime]

p'nat_coprime [lemma, in prime]

p'_elt_constt [lemma, in pgroup]

p1ElemE [lemma, in abelian]

p2Elem_dprodP [lemma, in abelian]

p2group_abelian [lemma, in sylow]

p2pv [definition, in vector]

p2pvK [lemma, in vector]

p3group_extraspecial [lemma, in 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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |