Mathlib Map

Theorems · Definition · number theory

Nat.Primes.toPNat

Nat.Primes → ℕ+

The canonical map from Nat.Primes to ℕ+

Defined in
Mathlib.Data.PNat.Prime
Cited by
11 results in Mathlib
Foundations
Depth 25 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PrimeMultiset.toPNatMultiset · cited by 11PrimeMultiset.toPNatMulti…PrimeMultiset.coePNatMonoidHom · cited by 2PrimeMultiset.coePNatMono…PrimeMultiset.coe_prod · cited by 2PrimeMultiset.coe_prodNat.Primes.coe_pnat_injective · cited by 2Primes.coe_pnat_injectivePrimeMultiset.to_ofPNatMultiset · cited by 2PrimeMultiset.to_ofPNatMu…PNat.factorMultiset_ofPrime · cited by 1PNat.factorMultiset_ofPri…PrimeMultiset.prod_ofPrime · cited by 1PrimeMultiset.prod_ofPrimePrimeMultiset.coePNat_ofPrime · cited by 0PrimeMultiset.coePNat_ofP…PrimeMultiset.coePNat_nat · cited by 0PrimeMultiset.coePNat_natPrimeMultiset.coePNat_prime · cited by 0PrimeMultiset.coePNat_pri…Nat.Primes.coe_pnat_inj · cited by 0Primes.coe_pnat_injPNat.count_factorMultiset · cited by 0PNat.count_factorMultisetNat.Primes.coe_pnat_nat · cited by 0Primes.coe_pnat_natPNat · cited by 392PNatNat.Primes · cited by 63Nat.PrimesPrimes.toPNatCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • PNatstatement · cited by 392
  • Nat.Primesstatement and proof · cited by 63

Cited by13

Results whose statement or proof uses this declaration.