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.

def PrimeMultiset : Type

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

Equations

• PrimeMultiset = Multiset Nat.Primes

instance instOrderBotPrimeMultiset : OrderBot PrimeMultiset

Equations

• instOrderBotPrimeMultiset = OrderBot.mk instOrderBotPrimeMultiset.proof_1

instance instOrderedSubPrimeMultiset : OrderedSub PrimeMultiset

Equations

• instOrderedSubPrimeMultiset = ⋯

unsafe instance PrimeMultiset.instRepr : Repr PrimeMultiset

Equations

• PrimeMultiset.instRepr = id inferInstance

def PrimeMultiset.ofPrime (p : Nat.Primes) : PrimeMultiset

The multiset consisting of a single prime

Equations

• PrimeMultiset.ofPrime p = {p}

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

def PrimeMultiset.toNatMultiset : PrimeMultiset → Multiset ℕ

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

• v.toNatMultiset = Multiset.map Coe.coe v

instance PrimeMultiset.coeNat : Coe PrimeMultiset (Multiset ℕ)

Equations

• PrimeMultiset.coeNat = { coe := PrimeMultiset.toNatMultiset }

def PrimeMultiset.coeNatMonoidHom : PrimeMultiset →+ Multiset ℕ

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.

@[simp]

theorem PrimeMultiset.coe_coeNatMonoidHom : ⇑PrimeMultiset.coeNatMonoidHom = Coe.coe

theorem PrimeMultiset.coeNat_injective : Function.Injective Coe.coe

theorem PrimeMultiset.coeNat_ofPrime (p : Nat.Primes) : (PrimeMultiset.ofPrime p).toNatMultiset = {↑p}

theorem PrimeMultiset.coeNat_prime (v : PrimeMultiset) (p : ℕ) (h : p ∈ v.toNatMultiset) : Nat.Prime p

def PrimeMultiset.toPNatMultiset : PrimeMultiset → Multiset ℕ+

Converts a PrimeMultiset to a Multiset ℕ+.

Equations

• v.toPNatMultiset = Multiset.map Coe.coe v

instance PrimeMultiset.coePNat : Coe PrimeMultiset (Multiset ℕ+)

Equations

• PrimeMultiset.coePNat = { coe := PrimeMultiset.toPNatMultiset }

def PrimeMultiset.coePNatMonoidHom : PrimeMultiset →+ Multiset ℕ+

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.

@[simp]

theorem PrimeMultiset.coe_coePNatMonoidHom : ⇑PrimeMultiset.coePNatMonoidHom = Coe.coe

theorem PrimeMultiset.coePNat_injective : Function.Injective Coe.coe

theorem PrimeMultiset.coePNat_ofPrime (p : Nat.Primes) : (PrimeMultiset.ofPrime p).toPNatMultiset = {↑p}

theorem PrimeMultiset.coePNat_prime (v : PrimeMultiset) (p : ℕ+) (h : p ∈ v.toPNatMultiset) : p.Prime

instance PrimeMultiset.coeMultisetPNatNat : Coe (Multiset ℕ+) (Multiset ℕ)

Equations

• PrimeMultiset.coeMultisetPNatNat = { coe := fun (v : Multiset ℕ+) => Multiset.map Coe.coe v }

theorem PrimeMultiset.coePNat_nat (v : PrimeMultiset) : Multiset.map PNat.val v.toPNatMultiset = v.toNatMultiset

def PrimeMultiset.prod (v : PrimeMultiset) : ℕ+

The product of a PrimeMultiset, as a ℕ+.

Equations

• v.prod = v.toPNatMultiset.prod

theorem PrimeMultiset.coe_prod (v : PrimeMultiset) : ↑v.prod = v.toNatMultiset.prod

theorem PrimeMultiset.prod_ofPrime (p : Nat.Primes) : (PrimeMultiset.ofPrime p).prod = ↑p

def PrimeMultiset.ofNatMultiset (v : Multiset ℕ) (h : ∀ p ∈ v, Nat.Prime p) : PrimeMultiset

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

Equations

• PrimeMultiset.ofNatMultiset v h = Multiset.pmap (fun (p : ℕ) (hp : Nat.Prime p) => ⟨p, hp⟩) v h

theorem PrimeMultiset.to_ofNatMultiset (v : Multiset ℕ) (h : ∀ p ∈ v, Nat.Prime p) : (PrimeMultiset.ofNatMultiset v h).toNatMultiset = v

theorem PrimeMultiset.prod_ofNatMultiset (v : Multiset ℕ) (h : ∀ p ∈ v, Nat.Prime p) : ↑(PrimeMultiset.ofNatMultiset v h).prod = v.prod

def PrimeMultiset.ofPNatMultiset (v : Multiset ℕ+) (h : ∀ p ∈ v, p.Prime) : PrimeMultiset

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

Equations

• PrimeMultiset.ofPNatMultiset v h = Multiset.pmap (fun (p : ℕ+) (hp : p.Prime) => ⟨↑p, hp⟩) v h

theorem PrimeMultiset.to_ofPNatMultiset (v : Multiset ℕ+) (h : ∀ p ∈ v, p.Prime) : (PrimeMultiset.ofPNatMultiset v h).toPNatMultiset = v

theorem PrimeMultiset.prod_ofPNatMultiset (v : Multiset ℕ+) (h : ∀ p ∈ v, p.Prime) : (PrimeMultiset.ofPNatMultiset v h).prod = v.prod

def PrimeMultiset.ofNatList (l : List ℕ) (h : ∀ p ∈ l, Nat.Prime p) : PrimeMultiset

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

Equations

• PrimeMultiset.ofNatList l h = PrimeMultiset.ofNatMultiset (↑l) h

theorem PrimeMultiset.prod_ofNatList (l : List ℕ) (h : ∀ p ∈ l, Nat.Prime p) : ↑(PrimeMultiset.ofNatList l h).prod = l.prod

def PrimeMultiset.ofPNatList (l : List ℕ+) (h : ∀ p ∈ l, p.Prime) : PrimeMultiset

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

Equations

• PrimeMultiset.ofPNatList l h = PrimeMultiset.ofPNatMultiset (↑l) h

theorem PrimeMultiset.prod_ofPNatList (l : List ℕ+) (h : ∀ p ∈ l, p.Prime) : (PrimeMultiset.ofPNatList l h).prod = l.prod

theorem PrimeMultiset.prod_zero : PrimeMultiset.prod 0 = 1

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

def PNat.factorMultiset (n : ℕ+) : PrimeMultiset

The prime factors of n, regarded as a multiset

Equations

• n.factorMultiset = PrimeMultiset.ofNatList (↑n).factors ⋯

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.

def PNat.factorMultisetEquiv : ℕ+ ≃ PrimeMultiset

Positive integers biject with multisets of primes.

Equations

• PNat.factorMultisetEquiv = { toFun := PNat.factorMultiset, invFun := PrimeMultiset.prod, left_inv := PNat.prod_factorMultiset, right_inv := PrimeMultiset.factorMultiset_prod }

theorem PNat.factorMultiset_one : PNat.factorMultiset 1 = 0

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 = PrimeMultiset.ofPrime p

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} {v : PrimeMultiset} : u.prod ∣ v.prod ↔ u ≤ v

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