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 instOrderBotPrimeMultisetToLEToPreorderToPartialOrderToOrderedAddCommMonoidInstPrimeMultisetCanonicallyOrderedAddCommMonoid : OrderBot PrimeMultiset

Equations

• One or more equations did not get rendered due to their size.

instance instOrderedSubPrimeMultisetToLEToPreorderToPartialOrderToOrderedAddCommMonoidInstPrimeMultisetCanonicallyOrderedAddCommMonoidToAddToAddCommMagmaToAddCommSemigroupToAddCommMonoidInstPrimeMultisetSub : OrderedSub PrimeMultiset

Equations

• One or more equations did not get rendered due to their size.

unsafe instance PrimeMultiset.instReprPrimeMultiset : Repr PrimeMultiset

Equations

• PrimeMultiset.instReprPrimeMultiset = 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

• PrimeMultiset.toNatMultiset v = 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.toNatMultiset (PrimeMultiset.ofPrime p) = {↑p}

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

def PrimeMultiset.toPNatMultiset : PrimeMultiset → Multiset ℕ+

Converts a PrimeMultiset to a Multiset ℕ+.

Equations

• PrimeMultiset.toPNatMultiset v = 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.toPNatMultiset (PrimeMultiset.ofPrime p) = {↑p}

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

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 (PrimeMultiset.toPNatMultiset v) = PrimeMultiset.toNatMultiset v

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

The product of a PrimeMultiset, as a ℕ+.

Equations

• PrimeMultiset.prod v = Multiset.prod (PrimeMultiset.toPNatMultiset v)

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

theorem PrimeMultiset.prod_ofPrime (p : Nat.Primes) : PrimeMultiset.prod (PrimeMultiset.ofPrime p) = ↑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) => { val := p, property := hp }) v h

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

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

def PrimeMultiset.ofPNatMultiset (v : Multiset ℕ+) (h : ∀ p ∈ v, PNat.Prime p) : 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 : PNat.Prime p) => { val := ↑p, property := hp }) v h

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

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

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.prod (PrimeMultiset.ofNatList l h)) = List.prod l

def PrimeMultiset.ofPNatList (l : List ℕ+) (h : ∀ p ∈ l, PNat.Prime p) : 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, PNat.Prime p) : PrimeMultiset.prod (PrimeMultiset.ofPNatList l h) = List.prod l

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) : PrimeMultiset.prod (u + v) = PrimeMultiset.prod u * PrimeMultiset.prod v

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

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

The prime factors of n, regarded as a multiset

Equations

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

theorem PNat.prod_factorMultiset (n : ℕ+) : PrimeMultiset.prod (PNat.factorMultiset n) = n

The product of the factors is the original number

theorem PNat.coeNat_factorMultiset (n : ℕ+) : PrimeMultiset.toNatMultiset (PNat.factorMultiset n) = ↑(Nat.factors ↑n)

theorem PrimeMultiset.factorMultiset_prod (v : PrimeMultiset) : PNat.factorMultiset (PrimeMultiset.prod v) = 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 : ℕ+) : PNat.factorMultiset (n * m) = PNat.factorMultiset n + PNat.factorMultiset m

theorem PNat.factorMultiset_pow (n : ℕ+) (m : ℕ) : PNat.factorMultiset (n ^ m) = m • PNat.factorMultiset n

theorem PNat.factorMultiset_ofPrime (p : Nat.Primes) : PNat.factorMultiset ↑p = PrimeMultiset.ofPrime p

Factoring a prime gives the corresponding one-element multiset.

theorem PNat.factorMultiset_le_iff {m : ℕ+} {n : ℕ+} : PNat.factorMultiset m ≤ PNat.factorMultiset n ↔ 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} : PNat.factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v

theorem PrimeMultiset.prod_dvd_iff {u : PrimeMultiset} {v : PrimeMultiset} : PrimeMultiset.prod u ∣ PrimeMultiset.prod v ↔ u ≤ v

theorem PrimeMultiset.prod_dvd_iff' {u : PrimeMultiset} {n : ℕ+} : PrimeMultiset.prod u ∣ n ↔ u ≤ PNat.factorMultiset n

theorem PNat.factorMultiset_gcd (m : ℕ+) (n : ℕ+) : PNat.factorMultiset (PNat.gcd m n) = PNat.factorMultiset m ⊓ PNat.factorMultiset n

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

theorem PNat.factorMultiset_lcm (m : ℕ+) (n : ℕ+) : PNat.factorMultiset (PNat.lcm m n) = PNat.factorMultiset m ⊔ PNat.factorMultiset n

theorem PNat.count_factorMultiset (m : ℕ+) (p : Nat.Primes) (k : ℕ) : ↑p ^ k ∣ m ↔ k ≤ Multiset.count p (PNat.factorMultiset m)

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) : PrimeMultiset.prod (u ⊓ v) = PNat.gcd (PrimeMultiset.prod u) (PrimeMultiset.prod v)

theorem PrimeMultiset.prod_sup (u : PrimeMultiset) (v : PrimeMultiset) : PrimeMultiset.prod (u ⊔ v) = PNat.lcm (PrimeMultiset.prod u) (PrimeMultiset.prod v)