# Documentation

Mathlib.Data.PNat.Factors

# Prime factors of nonzero naturals #

This file defines the factorization of a nonzero natural number n as a multiset of primes, the multiplicity of p in this factors multiset being the p-adic valuation of n.

## Main declarations #

• PrimeMultiset: Type of multisets of prime numbers.
• FactorMultiset n: Multiset of prime factors of n.

The type of multisets of prime numbers. Unique factorization gives an equivalence between this set and ℕ+, as we will formalize below.

Instances For

The multiset consisting of a single prime

Instances For
theorem PrimeMultiset.card_ofPrime (p : Nat.Primes) :
Multiset.card () = 1

We can forget the primality property and regard a multiset of primes as just a multiset of positive integers, or a multiset of natural numbers. In the opposite direction, if we have a multiset of positive integers or natural numbers, together with a proof that all the elements are prime, then we can regard it as a multiset of primes. The next block of results records obvious properties of these coercions.

Instances For

PrimeMultiset.coe, the coercion from a multiset of primes to a multiset of naturals, promoted to an AddMonoidHom.

Instances For
@[simp]

Converts a PrimeMultiset to a Multiset ℕ+.

Instances For

coePNat, the coercion from a multiset of primes to a multiset of positive naturals, regarded as an AddMonoidHom.

Instances For

The product of a PrimeMultiset, as a ℕ+.

Instances For
def PrimeMultiset.ofNatMultiset (v : ) (h : ∀ (p : ), p v) :

If a Multiset ℕ consists only of primes, it can be recast as a PrimeMultiset.

Instances For
theorem PrimeMultiset.to_ofNatMultiset (v : ) (h : ∀ (p : ), p v) :
theorem PrimeMultiset.prod_ofNatMultiset (v : ) (h : ∀ (p : ), p v) :
def PrimeMultiset.ofPNatMultiset (v : ) (h : ∀ (p : ℕ+), p v) :

If a Multiset ℕ+ consists only of primes, it can be recast as a PrimeMultiset.

Instances For
theorem PrimeMultiset.to_ofPNatMultiset (v : ) (h : ∀ (p : ℕ+), p v) :
theorem PrimeMultiset.prod_ofPNatMultiset (v : ) (h : ∀ (p : ℕ+), p v) :
def PrimeMultiset.ofNatList (l : ) (h : ∀ (p : ), p l) :

Lists can be coerced to multisets; here we have some results about how this interacts with our constructions on multisets.

Instances For
theorem PrimeMultiset.prod_ofNatList (l : ) (h : ∀ (p : ), p l) :
def PrimeMultiset.ofPNatList (l : ) (h : ∀ (p : ℕ+), p l) :

If a List ℕ+ consists only of primes, it can be recast as a PrimeMultiset with the coercion from lists to multisets.

Instances For
theorem PrimeMultiset.prod_ofPNatList (l : ) (h : ∀ (p : ℕ+), p l) :

The product map gives a homomorphism from the additive monoid of multisets to the multiplicative monoid ℕ+.

The prime factors of n, regarded as a multiset

Instances For

The product of the factors is the original number

If we start with a multiset of primes, take the product and then factor it, we get back the original multiset.

Positive integers biject with multisets of primes.

Instances For

Factoring gives a homomorphism from the multiplicative monoid ℕ+ to the additive monoid of multisets.

theorem PNat.factorMultiset_pow (n : ℕ+) (m : ) :
=

Factoring a prime gives the corresponding one-element multiset.

theorem PNat.factorMultiset_le_iff {m : ℕ+} {n : ℕ+} :

We now have four different results that all encode the idea that inequality of multisets corresponds to divisibility of positive integers.

theorem PNat.factorMultiset_gcd (m : ℕ+) (n : ℕ+) :

The gcd and lcm operations on positive integers correspond to the inf and sup operations on multisets.

theorem PNat.count_factorMultiset (m : ℕ+) (p : Nat.Primes) (k : ) :
Pow.pow (p) k m

The number of occurrences of p in the factor multiset of m is the same as the p-adic valuation of m.