mathlib documentation


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 #

def prime_multiset  :

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

theorem prime_multiset.add_sub_of_le {u v : prime_multiset} :
u vu + (v - u) = v

The multiset consisting of a single prime


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.


The product of a prime_multiset, as a ℕ+.

def prime_multiset.of_nat_multiset (v : multiset ) (h : ∀ (p : ), p p) :

If a multiset consists only of primes, it can be recast as a prime_multiset.

def prime_multiset.of_pnat_multiset (v : multiset ℕ+) (h : ∀ (p : ℕ+), p v → :

If a multiset ℕ+ consists only of primes, it can be recast as a prime_multiset.

def prime_multiset.of_nat_list (l : list ) (h : ∀ (p : ), p p) :

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

theorem prime_multiset.prod_of_nat_list (l : list ) (h : ∀ (p : ), p p) :
def prime_multiset.of_pnat_list (l : list ℕ+) (h : ∀ (p : ℕ+), p l → :

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

theorem prime_multiset.prod_of_pnat_list (l : list ℕ+) (h : ∀ (p : ℕ+), p l → :
theorem prime_multiset.prod_zero  : = 1

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

theorem prime_multiset.prod_add (u v : prime_multiset) :
(u + v).prod = ( *
theorem prime_multiset.prod_smul (d : ) (u : prime_multiset) :
(d u).prod = ^ d

The prime factors of n, regarded as a multiset


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.

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

Factoring a prime gives the corresponding one-element multiset.

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

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

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