P (Abbreviations)
| 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 (Abbreviations)
p [abbrev, in mathcomp.boot.fintype]P [abbrev, in mathcomp.boot.finset]
p [abbrev, in mathcomp.algebra.zmodp]
p_A [abbrev, in mathcomp.algebra.mxpoly]
passmx.m [abbrev, in mathcomp.algebra.vector]
passmx.m [abbrev, in mathcomp.algebra.vector]
passmx.m [abbrev, in mathcomp.algebra.vector]
passmx.n [abbrev, in mathcomp.algebra.vector]
passmx.n [abbrev, in mathcomp.algebra.vector]
passmx.n [abbrev, in mathcomp.algebra.vector]
passmx.n [abbrev, in mathcomp.algebra.vector]
passmx.p [abbrev, in mathcomp.algebra.vector]
path [abbrev, in mathcomp.boot.path]
path [abbrev, in mathcomp.boot.path]
Path [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.clone [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.copy [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.Exports.pathType [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.on [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Path.on_ [abbrev, in mathcomp.analysis.homotopy_theory.continuous_path]
Pdiv.Field.leq_trunc_divp [abbrev, in mathcomp.algebra.polydiv]
Pdiv.IdomainUnit.leq_trunc_divp [abbrev, in mathcomp.algebra.polydiv]
perm [abbrev, in mathcomp.finite_group.perm]
perm_eql [abbrev, in mathcomp.boot.seq]
perm_eql [abbrev, in mathcomp.boot.seq]
perm_eqr [abbrev, in mathcomp.boot.seq]
perm_eqr [abbrev, in mathcomp.boot.seq]
perm_tseq [abbrev, in mathcomp.boot.seq]
perms [abbrev, in mathcomp.boot.seq]
pfamily [abbrev, in mathcomp.boot.finfun]
pffun_on [abbrev, in mathcomp.boot.finfun]
pFrobenius_aut [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
pFtoE [abbrev, in mathcomp.algebra.polyXY]
ph [abbrev, in mathcomp.classical.wochoice]
ph [abbrev, in mathcomp.classical.filter]
PhantomF [abbrev, in mathcomp.analysis.landau]
PhantomF [abbrev, in mathcomp.analysis.landau]
PhantomF [abbrev, in mathcomp.analysis.landau]
pi [abbrev, in mathcomp.boot.generic_quotient]
PiConst [abbrev, in mathcomp.boot.generic_quotient]
piE [abbrev, in mathcomp.boot.generic_quotient]
PiEmbed [abbrev, in mathcomp.boot.generic_quotient]
PiMono1 [abbrev, in mathcomp.boot.generic_quotient]
PiMono2 [abbrev, in mathcomp.boot.generic_quotient]
PiMorph [abbrev, in mathcomp.boot.generic_quotient]
PiMorph1 [abbrev, in mathcomp.boot.generic_quotient]
PiMorph11 [abbrev, in mathcomp.boot.generic_quotient]
PiMorph2 [abbrev, in mathcomp.boot.generic_quotient]
pinv [abbrev, in mathcomp.classical.functions]
pinv [abbrev, in mathcomp.classical.functions]
Pointed [abbrev, in mathcomp.classical.classical_sets]
Pointed.clone [abbrev, in mathcomp.classical.classical_sets]
Pointed.copy [abbrev, in mathcomp.classical.classical_sets]
Pointed.Exports.pointedType [abbrev, in mathcomp.classical.classical_sets]
Pointed.on [abbrev, in mathcomp.classical.classical_sets]
Pointed.on_ [abbrev, in mathcomp.classical.classical_sets]
PointedDiscreteOrderTopology [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.Exports.pdiscreteOrderTopologicalType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteOrderTopology.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.Exports.pdiscreteTopologicalType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedDiscreteTopology.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
PointedFiltered [abbrev, in mathcomp.classical.filter]
PointedFiltered.clone [abbrev, in mathcomp.classical.filter]
PointedFiltered.copy [abbrev, in mathcomp.classical.filter]
PointedFiltered.Exports.pfilteredType [abbrev, in mathcomp.classical.filter]
PointedFiltered.on [abbrev, in mathcomp.classical.filter]
PointedFiltered.on_ [abbrev, in mathcomp.classical.filter]
PointedNbhs [abbrev, in mathcomp.classical.filter]
PointedNbhs.clone [abbrev, in mathcomp.classical.filter]
PointedNbhs.copy [abbrev, in mathcomp.classical.filter]
PointedNbhs.Exports.pnbhsType [abbrev, in mathcomp.classical.filter]
PointedNbhs.on [abbrev, in mathcomp.classical.filter]
PointedNbhs.on_ [abbrev, in mathcomp.classical.filter]
PointedTopological [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.clone [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.copy [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.Exports.ptopologicalType [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.on [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedTopological.on_ [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
PointedUniform [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.clone [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.copy [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.Exports.puniformType [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.on [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
PointedUniform.on_ [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
poisson [abbrev, in mathcomp.analysis.probability_theory.poisson_distribution]
porbit [abbrev, in mathcomp.finite_group.perm]
POrderedNbhs [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedNbhs.clone [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedNbhs.copy [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedNbhs.on [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedNbhs.on_ [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPointedTopological [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPointedTopological.clone [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPointedTopological.copy [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPointedTopological.on [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPointedTopological.on_ [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPseudoMetric [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPseudoMetric.clone [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPseudoMetric.copy [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPseudoMetric.on [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedPseudoMetric.on_ [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedTopological [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedTopological.clone [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedTopological.copy [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedTopological.on [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedTopological.on_ [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedUniform [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedUniform.clone [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedUniform.copy [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedUniform.on [abbrev, in mathcomp.analysis.topology_theory.order_topology]
POrderedUniform.on_ [abbrev, in mathcomp.analysis.topology_theory.order_topology]
Pos.sixteen [abbrev, in mathcomp.boot.ssrAC]
Pos.ten [abbrev, in mathcomp.boot.ssrAC]
pPbij [abbrev, in mathcomp.classical.functions]
pPinj [abbrev, in mathcomp.classical.functions]
pprod [abbrev, in mathcomp.finite_group.gproduct]
pprod [abbrev, in mathcomp.finite_group.gproduct]
pQtoC [abbrev, in mathcomp.field.cyclotomic]
pQtoC [abbrev, in mathcomp.field.algnum]
pQtoC [abbrev, in mathcomp.field.algC]
pred_of_set [abbrev, in mathcomp.boot.finset]
pred_set [abbrev, in mathcomp.classical.classical_sets]
predn [abbrev, in mathcomp.boot.ssrnat]
predOfType [abbrev, in mathcomp.finmap.finmap]
predOfType [abbrev, in mathcomp.boot.finset]
preimage_class [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
preimage_class_measurable_fun [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
preimage_classes [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
preimage_classes_comp [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
preimage_itv_c_infty [abbrev, in mathcomp.classical.classical_sets]
preimage_itv_infty_c [abbrev, in mathcomp.classical.classical_sets]
preimage_itv_infty_o [abbrev, in mathcomp.classical.classical_sets]
preimage_itv_o_infty [abbrev, in mathcomp.classical.classical_sets]
PreTopologicalLmod_isTvs [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalLmod_isTvs.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalLmod_isTvs.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalLmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalLmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalLmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalLmodule.Exports.preTopologicalLmodType [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalLmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalLmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalNmodule [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalNmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalNmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalNmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalNmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalNmodule_isTopologicalNmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalNmodule_isTopologicalNmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalNmodule_isTopologicalNmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalNmodule_isTopologicalZmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalNmodule_isTopologicalZmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalNmodule_isTopologicalZmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreTopologicalZmodule [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalZmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalZmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalZmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreTopologicalZmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformLmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformLmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformLmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformLmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformLmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformLmodule_isUniformLmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformLmodule_isUniformLmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformLmodule_isUniformLmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformNmodule [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformNmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformNmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformNmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformNmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformNmodule_isUniformNmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformNmodule_isUniformNmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformNmodule_isUniformNmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformNmodule_isUniformZmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformNmodule_isUniformZmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformNmodule_isUniformZmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
PreUniformZmodule [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformZmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformZmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformZmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PreUniformZmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
prim_root_charF [abbrev, in mathcomp.algebra.poly]
primeChar_abelem [abbrev, in mathcomp.field.finfield]
primeChar_dimf [abbrev, in mathcomp.field.finfield]
primeChar_pgroup [abbrev, in mathcomp.field.finfield]
primeChar_scale [abbrev, in mathcomp.field.finfield]
primeChar_scale1 [abbrev, in mathcomp.field.finfield]
primeChar_scaleA [abbrev, in mathcomp.field.finfield]
primeChar_scaleAl [abbrev, in mathcomp.field.finfield]
primeChar_scaleAr [abbrev, in mathcomp.field.finfield]
primeChar_scaleDl [abbrev, in mathcomp.field.finfield]
primeChar_scaleDr [abbrev, in mathcomp.field.finfield]
primeChar_vectAxiom [abbrev, in mathcomp.field.finfield]
PrimeCharType [abbrev, in mathcomp.field.finfield]
PrimeIdealr [abbrev, in mathcomp.algebra.ring_quotient]
PrimeIdealr.clone [abbrev, in mathcomp.algebra.ring_quotient]
PrimeIdealr.copy [abbrev, in mathcomp.algebra.ring_quotient]
PrimeIdealr.Exports.prime_idealr [abbrev, in mathcomp.algebra.ring_quotient]
PrimeIdealr.on [abbrev, in mathcomp.algebra.ring_quotient]
PrimeIdealr.on_ [abbrev, in mathcomp.algebra.ring_quotient]
PrimePowerField [abbrev, in mathcomp.field.finfield]
pro1 [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
pro2 [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
Probability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.clone [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.copy [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.Exports.probability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.on [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Probability.on_ [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
ProbabilityKernel [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.clone [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.copy [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.Exports.probability_kernel [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.on [abbrev, in mathcomp.analysis.kernel]
ProbabilityKernel.on_ [abbrev, in mathcomp.analysis.kernel]
prod_measurable_funP [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
prod_open [abbrev, in mathcomp.analysis.topology_theory.function_spaces]
prop_of [abbrev, in mathcomp.classical.filter]
ProperIdeal [abbrev, in mathcomp.algebra.ring_quotient]
ProperIdeal.clone [abbrev, in mathcomp.algebra.ring_quotient]
ProperIdeal.copy [abbrev, in mathcomp.algebra.ring_quotient]
ProperIdeal.Exports.proper_ideal [abbrev, in mathcomp.algebra.ring_quotient]
ProperIdeal.on [abbrev, in mathcomp.algebra.ring_quotient]
ProperIdeal.on_ [abbrev, in mathcomp.algebra.ring_quotient]
PseudoMetric [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.clone [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.copy [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.Exports.pseudoMetricType [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.on [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoMetric.on_ [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
pseudoMetric_from_normedZmodType.T [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetric_isMetric [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
PseudoMetric_isMetric.axioms [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
PseudoMetric_isMetric.Build [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
PseudoMetricNormedZmod [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.clone [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.copy [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.Exports.pseudoMetricNormedZmodType [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.on [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod.on_ [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
PseudoMetricNormedZmod_Lmodule_isNormedModule [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Lmodule_isNormedModule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Tvs_isNormedModule [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Tvs_isNormedModule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoMetricNormedZmod_Tvs_isNormedModule.Build [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
PseudoPointedMetric [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.clone [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.copy [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.Exports.pseudoPMetricType [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.on [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
PseudoPointedMetric.on_ [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
purely_inseparable_elementP [abbrev, in mathcomp.field.separable]
Px [abbrev, in mathcomp.field.galois]
pZtoC [abbrev, in mathcomp.field.cyclotomic]
pZtoC [abbrev, in mathcomp.field.algnum]
pZtoC [abbrev, in mathcomp.field.algC]
pZtoQ [abbrev, in mathcomp.field.cyclotomic]
pZtoQ [abbrev, in mathcomp.field.algnum]
pZtoQ [abbrev, in mathcomp.field.algC]
pZtoQ [abbrev, in mathcomp.algebra.rat]