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 instInhabitedPrimeMultiset : Inhabited PrimeMultiset

Equations

• instInhabitedPrimeMultiset = Multiset.inhabitedMultiset

instance instAddCommMonoidPrimeMultiset : AddCommMonoid PrimeMultiset

Equations

• instAddCommMonoidPrimeMultiset = Multiset.instAddCancelCommMonoid.toAddCommMonoid

instance instDistribLatticePrimeMultiset : DistribLattice PrimeMultiset

Equations

• instDistribLatticePrimeMultiset = Multiset.instDistribLattice

instance instSemilatticeSupPrimeMultiset : SemilatticeSup PrimeMultiset

Equations

• instSemilatticeSupPrimeMultiset = Multiset.instLattice.toSemilatticeSup

instance instSubPrimeMultiset : Sub PrimeMultiset

Equations

• instSubPrimeMultiset = Multiset.instSub

instance instIsOrderedCancelAddMonoidPrimeMultiset : IsOrderedCancelAddMonoid PrimeMultiset

Equations

• instIsOrderedCancelAddMonoidPrimeMultiset = ⋯

instance instCanonicallyOrderedAddPrimeMultiset : CanonicallyOrderedAdd PrimeMultiset

Equations

• instCanonicallyOrderedAddPrimeMultiset = ⋯

instance instOrderBotPrimeMultiset : OrderBot PrimeMultiset

Equations

• instOrderBotPrimeMultiset = Multiset.instOrderBot

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}

@[simp]

theorem PrimeMultiset.card_ofPrime (p : Nat.Primes) : Multiset.card (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 Subtype.val 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

• PrimeMultiset.coeNatMonoidHom = Multiset.mapAddMonoidHom Subtype.val

@[simp]

theorem PrimeMultiset.coe_coeNatMonoidHom : ⇑coeNatMonoidHom = toNatMultiset

theorem PrimeMultiset.coeNat_injective : Function.Injective toNatMultiset

theorem PrimeMultiset.coeNat_ofPrime (p : Nat.Primes) : (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 Nat.Primes.toPNat 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

• PrimeMultiset.coePNatMonoidHom = Multiset.mapAddMonoidHom Nat.Primes.toPNat

@[simp]

theorem PrimeMultiset.coe_coePNatMonoidHom : ⇑coePNatMonoidHom = toPNatMultiset

theorem PrimeMultiset.coePNat_injective : Function.Injective toPNatMultiset

theorem PrimeMultiset.coePNat_ofPrime (p : Nat.Primes) : (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 PNat.val 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) : (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

@[simp]

theorem PrimeMultiset.mem_ofNatMultiset {p : ℕ+} {s : Multiset ℕ} (hs : ∀ p ∈ s, Nat.Prime p) : p ∈ (ofNatMultiset s hs).toPNatMultiset ↔ ↑p ∈ s

@[simp]

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

@[simp]

theorem PrimeMultiset.prod_ofNatMultiset (v : Multiset ℕ) (h : ∀ p ∈ v, Nat.Prime p) : ↑(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

@[simp]

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

@[simp]

theorem PrimeMultiset.prod_ofPNatMultiset (v : Multiset ℕ+) (h : ∀ p ∈ v, p.Prime) : (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

@[simp]

theorem PrimeMultiset.mem_ofNatList {p : ℕ+} {l : List ℕ} (hl : ∀ p ∈ l, Nat.Prime p) : p ∈ (ofNatList l hl).toPNatMultiset ↔ ↑p ∈ l

@[simp]

theorem PrimeMultiset.prod_ofNatList (l : List ℕ) (h : ∀ p ∈ l, Nat.Prime p) : ↑(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

@[simp]

theorem PrimeMultiset.toPNatMultiset_ofPNatList {l : List ℕ+} (hl : ∀ p ∈ l, p.Prime) : (ofPNatList l hl).toPNatMultiset = ↑l

@[simp]

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

@[simp]

theorem PrimeMultiset.prod_zero : prod 0 = 1

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

@[simp]

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

@[simp]

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).primeFactorsList ⋯

@[simp]

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).primeFactorsList

@[simp]

theorem PNat.mem_factorMultiset {p n : ℕ+} : p ∈ n.factorMultiset.toPNatMultiset ↔ p.Prime ∧ p ∣ n

@[simp]

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 }

@[simp]

theorem PNat.factorMultiset_one : factorMultiset 1 = 0

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

@[simp]

theorem PNat.factorMultiset_mul (n m : ℕ+) : (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

@[simp]

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.

@[simp]

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_mono {m n : ℕ+} : m ∣ n → m.factorMultiset ≤ n.factorMultiset

Alias of the reverse direction of PNat.factorMultiset_le_iff.

---

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

@[simp]

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

theorem PrimeMultiset.prod_dvd_prod {u v : PrimeMultiset} : u ≤ v → u.prod ∣ v.prod

Alias of the reverse direction of PrimeMultiset.prod_dvd_iff.

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

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