# mathlibdocumentation

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
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

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
@[instance]

Equations
@[instance]

Converts a prime_multiset to a multiset ℕ+.

Equations
@[instance]

Equations
@[instance]

@[instance]

Equations

The product of a prime_multiset, as a ℕ+.

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

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

Equations
theorem prime_multiset.to_of_nat_multiset (v : multiset ) (h : ∀ (p : ), p v) :

theorem prime_multiset.prod_of_nat_multiset (v : multiset ) (h : ∀ (p : ), p v) :

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
theorem prime_multiset.to_of_pnat_multiset (v : multiset ℕ+) (h : ∀ (p : ℕ+), p v → p.prime) :

theorem prime_multiset.prod_of_pnat_multiset (v : multiset ℕ+) (h : ∀ (p : ℕ+), p v → p.prime) :

def prime_multiset.of_nat_list (l : list ) :
(∀ (p : ), p lprime_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 l) :

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) :
= l.prod

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
theorem pnat.prod_factor_multiset (n : ℕ+) :

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.

Equations

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

theorem pnat.factor_multiset_pow (n : ℕ+) (m : ) :

Factoring a prime gives the corresponding one-element multiset.

theorem pnat.factor_multiset_le_iff {m n : ℕ+} :
m n

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.

theorem pnat.count_factor_multiset (m : ℕ+) (p : nat.primes) (k : ) :
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.