mathlib documentation

data.pnat.factors

def prime_multiset  :
Type

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

Equations
@[instance]

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

The multiset consisting of a single prime

Equations

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.

Equations

The product of a prime_multiset, as a ℕ+.

Equations
def prime_multiset.of_nat_multiset (v : multiset ) :
(∀ (p : ), p vnat.prime p)prime_multiset

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

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

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

Equations
def prime_multiset.of_nat_list (l : list ) :
(∀ (p : ), p lnat.prime p)prime_multiset

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

Equations
theorem prime_multiset.prod_of_nat_list (l : list ) (h : ∀ (p : ), p lnat.prime p) :

def prime_multiset.of_pnat_list (l : list ℕ+) :
(∀ (p : ℕ+), p l → p.prime)prime_multiset

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

Equations
theorem prime_multiset.prod_of_pnat_list (l : list ℕ+) (h : ∀ (p : ℕ+), p l → p.prime) :

theorem prime_multiset.prod_zero  :
0.prod = 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 = (u.prod) * v.prod

theorem prime_multiset.prod_smul (d : ) (u : prime_multiset) :
(d •ℕ u).prod = u.prod ^ d

The prime factors of n, regarded as a multiset

Equations

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.