# 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.

Equations
Instances For
Equations
unsafe instance PrimeMultiset.instRepr :
Equations

The multiset consisting of a single prime

Equations
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.

Equations
Instances For
Equations

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem PrimeMultiset.coeNat_ofPrime (p : Nat.Primes) :
.toNatMultiset = {p}
theorem PrimeMultiset.coeNat_prime (v : PrimeMultiset) (p : ) (h : p v.toNatMultiset) :
p.Prime

Converts a PrimeMultiset to a Multiset ℕ+.

Equations
Instances For
Equations

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem PrimeMultiset.coePNat_ofPrime (p : Nat.Primes) :
.toPNatMultiset = {p}
theorem PrimeMultiset.coePNat_prime (v : PrimeMultiset) (p : ℕ+) (h : p v.toPNatMultiset) :
p.Prime
Equations
theorem PrimeMultiset.coePNat_nat (v : PrimeMultiset) :
Multiset.map PNat.val v.toPNatMultiset = v.toNatMultiset

The product of a PrimeMultiset, as a ℕ+.

Equations
• v.prod = v.toPNatMultiset.prod
Instances For
theorem PrimeMultiset.coe_prod (v : PrimeMultiset) :
v.prod = v.toNatMultiset.prod
def PrimeMultiset.ofNatMultiset (v : ) (h : pv, p.Prime) :

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

Equations
Instances For
theorem PrimeMultiset.to_ofNatMultiset (v : ) (h : pv, p.Prime) :
.toNatMultiset = v
theorem PrimeMultiset.prod_ofNatMultiset (v : ) (h : pv, p.Prime) :
.prod = v.prod
def PrimeMultiset.ofPNatMultiset (v : ) (h : pv, p.Prime) :

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

Equations
Instances For
theorem PrimeMultiset.to_ofPNatMultiset (v : ) (h : pv, p.Prime) :
.toPNatMultiset = v
theorem PrimeMultiset.prod_ofPNatMultiset (v : ) (h : pv, p.Prime) :
.prod = v.prod
def PrimeMultiset.ofNatList (l : ) (h : pl, p.Prime) :

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

Equations
Instances For
theorem PrimeMultiset.prod_ofNatList (l : ) (h : pl, p.Prime) :
().prod = l.prod
def PrimeMultiset.ofPNatList (l : ) (h : pl, p.Prime) :

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

Equations
Instances For
theorem PrimeMultiset.prod_ofPNatList (l : ) (h : pl, p.Prime) :
().prod = l.prod

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

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

The prime factors of n, regarded as a multiset

Equations
Instances For
theorem PNat.prod_factorMultiset (n : ℕ+) :
n.factorMultiset.prod = n

The product of the factors is the original number

theorem PNat.coeNat_factorMultiset (n : ℕ+) :
n.factorMultiset.toNatMultiset = (n).factors
theorem PrimeMultiset.factorMultiset_prod (v : PrimeMultiset) :
v.prod.factorMultiset = v

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
Instances For

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

theorem PNat.factorMultiset_mul (n : ℕ+) (m : ℕ+) :
(n * m).factorMultiset = n.factorMultiset + m.factorMultiset
theorem PNat.factorMultiset_pow (n : ℕ+) (m : ) :
(n ^ m).factorMultiset = m n.factorMultiset
theorem PNat.factorMultiset_ofPrime (p : Nat.Primes) :
(p).factorMultiset =

Factoring a prime gives the corresponding one-element multiset.

theorem PNat.factorMultiset_le_iff {m : ℕ+} {n : ℕ+} :
m.factorMultiset n.factorMultiset 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_le_iff' {m : ℕ+} {v : PrimeMultiset} :
m.factorMultiset v m v.prod
theorem PrimeMultiset.prod_dvd_iff' {u : PrimeMultiset} {n : ℕ+} :
u.prod n u n.factorMultiset
theorem PNat.factorMultiset_gcd (m : ℕ+) (n : ℕ+) :
(m.gcd n).factorMultiset = m.factorMultiset n.factorMultiset

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

theorem PNat.factorMultiset_lcm (m : ℕ+) (n : ℕ+) :
(m.lcm n).factorMultiset = m.factorMultiset n.factorMultiset
theorem PNat.count_factorMultiset (m : ℕ+) (p : Nat.Primes) (k : ) :
p ^ k m k Multiset.count p m.factorMultiset

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

theorem PrimeMultiset.prod_inf (u : PrimeMultiset) (v : PrimeMultiset) :
(u v).prod = u.prod.gcd v.prod
theorem PrimeMultiset.prod_sup (u : PrimeMultiset) (v : PrimeMultiset) :
(u v).prod = u.prod.lcm v.prod