P (Definitions)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
P (Definitions)
p_elt [def, in mathcomp.solvable.pgroup]p_group [def, in mathcomp.solvable.pgroup]
p_rank [def, in mathcomp.solvable.abelian]
pair1g [def, in mathcomp.finite_group.gproduct]
pair1g_morphism [def, in mathcomp.finite_group.gproduct]
pair_eq [def, in mathcomp.boot.eqtype]
pair_invr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
pair_of_interval [def, in mathcomp.algebra.interval]
pair_of_mxvec_index [def, in mathcomp.algebra.matrix]
pair_of_sd [def, in mathcomp.finite_group.gproduct]
pair_of_section [def, in mathcomp.solvable.jordanholder]
pair_of_tag [def, in mathcomp.boot.choice]
pair_opp [def, in mathcomp.boot.nmodule]
pair_ortho_rec [def, in mathcomp.group_representation.classfun]
pair_ortho_rec [def, in mathcomp.algebra.sesquilinear]
pair_unitr [def, in mathcomp.algebra.algebraic_hierarchy.divalg]
pair_zero [def, in mathcomp.boot.nmodule]
pairg1 [def, in mathcomp.finite_group.gproduct]
pairg1_morphism [def, in mathcomp.finite_group.gproduct]
pairmap [def, in mathcomp.boot.seq]
pairmap_bseq [def, in mathcomp.boot.tuple]
pairmap_tuple [def, in mathcomp.boot.tuple]
pairwise [def, in mathcomp.boot.seq]
pairwise_orthogonal [def, in mathcomp.group_representation.classfun]
pairwise_orthogonal [def, in mathcomp.algebra.sesquilinear]
parse [def, in mathcomp.algebra.rat]
parse [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
parse_int [def, in mathcomp.algebra.ssrint]
partial_product [def, in mathcomp.finite_group.gproduct]
partition [def, in mathcomp.boot.finset]
partn [def, in mathcomp.boot.prime]
Pascal [def, in mathcomp.boot.binomial]
passmx.funmx [def, in mathcomp.algebra.vector]
passmx.hommx [def, in mathcomp.algebra.vector]
passmx.leigenspace [def, in mathcomp.algebra.vector]
passmx.leigenvalue [def, in mathcomp.algebra.vector]
passmx.msof [def, in mathcomp.algebra.vector]
passmx.mxof [def, in mathcomp.algebra.vector]
passmx.rVof [def, in mathcomp.algebra.vector]
passmx.vecof [def, in mathcomp.algebra.vector]
passmx.vsof [def, in mathcomp.algebra.vector]
path [def, in mathcomp.boot.path]
pblock [def, in mathcomp.boot.finset]
pcan_type [def, in mathcomp.boot.eqtype]
PCanIsCountable [def, in mathcomp.boot.choice]
PCanIsFinite [def, in mathcomp.boot.fintype]
pcore [def, in mathcomp.solvable.pgroup]
pcore_gFun [def, in mathcomp.solvable.pgroup]
pcore_group [def, in mathcomp.solvable.pgroup]
pcore_igFun [def, in mathcomp.solvable.pgroup]
pcore_mod [def, in mathcomp.solvable.pgroup]
pcore_mod_group [def, in mathcomp.solvable.pgroup]
pcore_pgFun [def, in mathcomp.solvable.pgroup]
pdiv [def, in mathcomp.boot.prime]
Pdiv.CommonIdomain.apply_irredp [def, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.coprimep [def, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdp [def, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.egcdp_rec [def, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gcdp [def, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gdcop [def, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.gdcop_rec [def, in mathcomp.algebra.polydiv]
Pdiv.CommonIdomain.irreducible_poly [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rcoprimep [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdivp [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rdvdp [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.redivp [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.redivp_expanded_def [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.redivp_rec [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.redivp_unlockable [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgcdp [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgdcop [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rgdcop_rec [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rmodp [def, in mathcomp.algebra.polydiv]
Pdiv.CommonRing.rscalp [def, in mathcomp.algebra.polydiv]
Pdiv.Field.mup [def, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.divp [def, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.dvdp [def, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.edivp [def, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.edivp_expanded_def [def, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.edivp_unlockable [def, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.eqp [def, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.modp [def, in mathcomp.algebra.polydiv]
Pdiv.IdomainDefs.scalp [def, in mathcomp.algebra.polydiv]
pElem [def, in mathcomp.solvable.abelian]
perm.body [def, in mathcomp.finite_group.perm]
perm.unlock [def, in mathcomp.finite_group.perm]
perm_action [def, in mathcomp.finite_group.action]
perm_eq [def, in mathcomp.boot.seq]
perm_in [def, in mathcomp.finite_group.automorphism]
perm_inv [def, in mathcomp.finite_group.perm]
perm_mul [def, in mathcomp.finite_group.perm]
perm_mx [def, in mathcomp.algebra.matrix]
perm_of [def, in mathcomp.finite_group.perm]
perm_on [def, in mathcomp.finite_group.perm]
perm_one [def, in mathcomp.finite_group.perm]
perm_unlock [def, in mathcomp.finite_group.perm]
perm_unlock_subterm [def, in mathcomp.finite_group.perm]
perms_rec [def, in mathcomp.boot.seq]
permutations [def, in mathcomp.boot.seq]
Pextraspecial.act [def, in mathcomp.solvable.extraspecial]
Pextraspecial.action [def, in mathcomp.solvable.extraspecial]
Pextraspecial.groupAction [def, in mathcomp.solvable.extraspecial]
Pextraspecial.gtype [def, in mathcomp.solvable.extraspecial]
Pextraspecial.ngtype [def, in mathcomp.solvable.extraspecial]
Pextraspecial.ngtypeQ [def, in mathcomp.solvable.extraspecial]
pfactor [def, in mathcomp.boot.prime]
pfamily_mem [def, in mathcomp.boot.finfun]
pffun_on_mem [def, in mathcomp.boot.finfun]
pgroup [def, in mathcomp.solvable.pgroup]
pHall [def, in mathcomp.solvable.pgroup]
pi.body [def, in mathcomp.boot.generic_quotient]
pi.unlock [def, in mathcomp.boot.generic_quotient]
pi_add_quot_morph [def, in mathcomp.algebra.ring_quotient]
pi_addr [def, in mathcomp.algebra.ring_quotient]
pi_arg [def, in mathcomp.boot.prime]
pi_arg_of_fin_pred [def, in mathcomp.boot.prime]
pi_arg_of_nat [def, in mathcomp.boot.prime]
pi_eq_quot [def, in mathcomp.boot.generic_quotient]
pi_eq_quot_mono [def, in mathcomp.boot.generic_quotient]
pi_inv_quot_morph [def, in mathcomp.algebra.ring_quotient]
pi_invr [def, in mathcomp.algebra.ring_quotient]
pi_is_additive [def, in mathcomp.algebra.ring_quotient]
pi_is_multiplicative [def, in mathcomp.algebra.ring_quotient]
pi_mul_quot_morph [def, in mathcomp.algebra.ring_quotient]
pi_mulr [def, in mathcomp.algebra.ring_quotient]
pi_of [def, in mathcomp.boot.prime]
pi_one_quot_morph [def, in mathcomp.algebra.ring_quotient]
pi_oner [def, in mathcomp.algebra.ring_quotient]
pi_opp_quot_morph [def, in mathcomp.algebra.ring_quotient]
pi_oppr [def, in mathcomp.algebra.ring_quotient]
pi_subdef [def, in mathcomp.boot.generic_quotient]
pi_subfext_inv_morph [def, in mathcomp.field.fieldext]
pi_subfext_mul_morph [def, in mathcomp.field.fieldext]
pi_subfext_opp_morph [def, in mathcomp.field.fieldext]
pi_subfx_add_morph [def, in mathcomp.field.fieldext]
pi_subfx_inj_morph [def, in mathcomp.field.fieldext]
pi_unit_quot_morph [def, in mathcomp.algebra.ring_quotient]
pi_unitr [def, in mathcomp.algebra.ring_quotient]
pi_unlock [def, in mathcomp.boot.generic_quotient]
pi_unlock_subterm [def, in mathcomp.boot.generic_quotient]
pi_zero_quot_morph [def, in mathcomp.algebra.ring_quotient]
pi_zeror [def, in mathcomp.algebra.ring_quotient]
pick [def, in mathcomp.boot.fintype]
pick_true [def, in mathcomp.boot.fintype]
pickle [def, in mathcomp.boot.choice]
pickle_inv [def, in mathcomp.boot.choice]
pickle_seq [def, in mathcomp.boot.choice]
pickle_tagged [def, in mathcomp.boot.choice]
pickleK [def, in mathcomp.boot.choice]
pid_mx [def, in mathcomp.algebra.matrix]
pinvmx [def, in mathcomp.algebra.mxalgebra]
plogp [def, in mathcomp.field.qfpoly]
pmap [def, in mathcomp.boot.seq]
pmaxElem [def, in mathcomp.solvable.abelian]
pnat [def, in mathcomp.boot.prime]
pnElem [def, in mathcomp.solvable.abelian]
poly [def, in mathcomp.algebra.poly]
Poly [def, in mathcomp.algebra.poly]
poly_expanded_def [def, in mathcomp.algebra.poly]
poly_inv [def, in mathcomp.algebra.poly]
poly_nil [def, in mathcomp.algebra.poly]
poly_of_size [def, in mathcomp.algebra.qpoly]
poly_of_size_pred [def, in mathcomp.algebra.qpoly]
poly_rV [def, in mathcomp.algebra.mxpoly]
poly_unit [def, in mathcomp.algebra.poly]
poly_unlockable [def, in mathcomp.algebra.poly]
poly_XaY [def, in mathcomp.algebra.polyXY]
poly_XmY [def, in mathcomp.algebra.polyXY]
polyC [def, in mathcomp.algebra.poly]
polyC_multiplicative [def, in mathcomp.algebra.poly]
polyOver [def, in mathcomp.algebra.poly]
polyOver_pred [def, in mathcomp.algebra.poly]
polyX [def, in mathcomp.algebra.poly]
polyX_def [def, in mathcomp.algebra.poly]
polyX_unlockable [def, in mathcomp.algebra.poly]
pop_succn [def, in mathcomp.boot.ssrnat]
porbit.body [def, in mathcomp.finite_group.perm]
porbit.unlock [def, in mathcomp.finite_group.perm]
porbit_unlock_subterm [def, in mathcomp.finite_group.perm]
porbit_unlockable [def, in mathcomp.finite_group.perm]
porbits [def, in mathcomp.finite_group.perm]
Pos.Nsucc [def, in mathcomp.boot.ssrAC]
Pos.of_hex_int [def, in mathcomp.boot.ssrAC]
Pos.of_hex_uint [def, in mathcomp.boot.ssrAC]
Pos.of_hex_uint_acc [def, in mathcomp.boot.ssrAC]
Pos.of_int [def, in mathcomp.boot.ssrAC]
Pos.of_num_int [def, in mathcomp.boot.ssrAC]
Pos.of_uint [def, in mathcomp.boot.ssrAC]
Pos.of_uint_acc [def, in mathcomp.boot.ssrAC]
Pos.to_little_uint [def, in mathcomp.boot.ssrAC]
Pos.to_num_uint [def, in mathcomp.boot.ssrAC]
Pos.to_uint [def, in mathcomp.boot.ssrAC]
pos_nat [def, in mathcomp.algebra.binnums]
pos_natE [def, in mathcomp.algebra.binnums]
pos_of_nat [def, in mathcomp.boot.ssrnat]
Pos_to_natE [def, in mathcomp.algebra.binnums]
PosNum [def, in mathcomp.algebra.interval_inference]
powers_mx [def, in mathcomp.algebra.mxpoly]
powerset [def, in mathcomp.boot.finset]
pprimeChar_scale [def, in mathcomp.field.finfield]
pPrimeCharType [def, in mathcomp.field.finfield]
pprodm [def, in mathcomp.finite_group.gproduct]
pprodm_morphism [def, in mathcomp.finite_group.gproduct]
pred0b [def, in mathcomp.boot.fintype]
pred1 [def, in mathcomp.boot.eqtype]
pred2 [def, in mathcomp.boot.eqtype]
pred3 [def, in mathcomp.boot.eqtype]
pred4 [def, in mathcomp.boot.eqtype]
pred_Nirr [def, in mathcomp.group_representation.character]
pred_of_itv [def, in mathcomp.algebra.interval]
pred_of_seq [def, in mathcomp.boot.seq]
pred_of_set.body [def, in mathcomp.boot.finset]
pred_of_set.unlock [def, in mathcomp.boot.finset]
pred_of_set_unlock [def, in mathcomp.boot.finset]
pred_of_set_unlock_subterm [def, in mathcomp.boot.finset]
pred_of_vspace [def, in mathcomp.algebra.vector]
predC1 [def, in mathcomp.boot.eqtype]
predD1 [def, in mathcomp.boot.eqtype]
predU1 [def, in mathcomp.boot.eqtype]
predX [def, in mathcomp.boot.eqtype]
prefix [def, in mathcomp.boot.seq]
preim_partition [def, in mathcomp.boot.finset]
preim_seq [def, in mathcomp.boot.fintype]
preimset [def, in mathcomp.boot.finset]
Presentation.and_rel [def, in mathcomp.finite_group.presentation]
Presentation.bool_of_rel [def, in mathcomp.finite_group.presentation]
Presentation.Cast [def, in mathcomp.finite_group.presentation]
Presentation.env1 [def, in mathcomp.finite_group.presentation]
Presentation.Eq1 [def, in mathcomp.finite_group.presentation]
Presentation.Eq3 [def, in mathcomp.finite_group.presentation]
Presentation.eval [def, in mathcomp.finite_group.presentation]
Presentation.hom [def, in mathcomp.finite_group.presentation]
Presentation.iso [def, in mathcomp.finite_group.presentation]
Presentation.rel [def, in mathcomp.finite_group.presentation]
Presentation.sat [def, in mathcomp.finite_group.presentation]
prev [def, in mathcomp.boot.path]
prev_at [def, in mathcomp.boot.path]
prime [def, in mathcomp.boot.prime]
prime_decomp [def, in mathcomp.boot.prime]
prime_decomp_rec [def, in mathcomp.boot.prime]
prime_idealr_closed [def, in mathcomp.algebra.ring_quotient]
PrimeDecompAux.add_divisors [def, in mathcomp.boot.prime]
PrimeDecompAux.add_totient_factor [def, in mathcomp.boot.prime]
PrimeDecompAux.cons_pfactor [def, in mathcomp.boot.prime]
PrimeDecompAux.edivn2 [def, in mathcomp.boot.prime]
PrimeDecompAux.elogn2 [def, in mathcomp.boot.prime]
PrimeDecompAux.ifnz [def, in mathcomp.boot.prime]
PrimeIdealr.pack_ [def, in mathcomp.algebra.ring_quotient]
PrimeIdealr.phant_clone [def, in mathcomp.algebra.ring_quotient]
PrimeIdealr.phant_on_ [def, in mathcomp.algebra.ring_quotient]
primes [def, in mathcomp.boot.prime]
primitive [def, in mathcomp.solvable.primitive_action]
primitive_poly [def, in mathcomp.field.qfpoly]
primitive_root_of_unity [def, in mathcomp.algebra.poly]
principal_comp [def, in mathcomp.group_representation.mxrepresentation]
principal_comp_def [def, in mathcomp.group_representation.mxrepresentation]
print [def, in mathcomp.algebra.rat]
print [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
print_int [def, in mathcomp.algebra.ssrint]
prod_enum [def, in mathcomp.boot.fintype]
prod_repr [def, in mathcomp.group_representation.character]
prod_tuple [def, in mathcomp.solvable.burnside_app]
prod_unsplit [def, in mathcomp.algebra.tensor]
prodv [def, in mathcomp.field.falgebra]
prodv_aspace [def, in mathcomp.field.fieldext]
prodv_unlockable [def, in mathcomp.field.falgebra]
proj_mx [def, in mathcomp.algebra.mxalgebra]
proj_ortho [def, in mathcomp.algebra.spectral]
projv [def, in mathcomp.algebra.vector]
proper [def, in mathcomp.boot.fintype]
proper_addv [def, in mathcomp.algebra.vector]
proper_addvP [def, in mathcomp.algebra.vector]
proper_ideal [def, in mathcomp.algebra.ring_quotient]
proper_mxsumP [def, in mathcomp.algebra.mxalgebra]
ProperIdeal.pack_ [def, in mathcomp.algebra.ring_quotient]
ProperIdeal.phant_clone [def, in mathcomp.algebra.ring_quotient]
ProperIdeal.phant_on_ [def, in mathcomp.algebra.ring_quotient]
pseries [def, in mathcomp.solvable.pgroup]
pseries_gFun [def, in mathcomp.solvable.pgroup]
pseries_group [def, in mathcomp.solvable.pgroup]
pseries_igFun [def, in mathcomp.solvable.pgroup]
pseries_pgFun [def, in mathcomp.solvable.pgroup]
psubgroup [def, in mathcomp.solvable.pgroup]
purely_inseparable [def, in mathcomp.field.separable]
purely_inseparable_element [def, in mathcomp.field.separable]
push_invariant [def, in mathcomp.boot.path]
pval [def, in mathcomp.finite_group.perm]