mathlib3 documentation

data.pnat.factors

Prime factors of nonzero naturals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

prime_multiset: Type of multisets of prime numbers.
factor_multiset n: Multiset of prime factors of n.

@[protected, instance]

def prime_multiset.canonically_ordered_add_monoid :

canonically_ordered_add_monoid prime_multiset

@[protected, instance]

def prime_multiset.has_sub :

has_sub prime_multiset

@[protected, instance]

def prime_multiset.has_ordered_sub :

has_ordered_sub prime_multiset

def prime_multiset :

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

Equations

prime_multiset = multiset nat.primes

Instances for prime_multiset

@[protected, instance]

def prime_multiset.distrib_lattice :

distrib_lattice prime_multiset

@[protected, instance]

def prime_multiset.order_bot :

order_bot prime_multiset

@[protected, instance]

def prime_multiset.semilattice_sup :

semilattice_sup prime_multiset

@[protected, instance]

def prime_multiset.inhabited :

inhabited prime_multiset

@[protected, instance]

meta def prime_multiset.has_repr :

has_repr prime_multiset

def prime_multiset.of_prime (p : nat.primes) :

The multiset consisting of a single prime

Equations

prime_multiset.of_prime p = {p}

theorem prime_multiset.card_of_prime (p : nat.primes) :

⇑multiset.card (prime_multiset.of_prime p) = 1

def prime_multiset.to_nat_multiset :

prime_multiset → 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

prime_multiset.to_nat_multiset = λ (v : prime_multiset), multiset.map (λ (p : nat.primes), ↑p) v

@[protected, instance]

def prime_multiset.coe_nat :

has_coe prime_multiset (multiset ℕ)

Equations

prime_multiset.coe_nat = {coe := prime_multiset.to_nat_multiset}

def prime_multiset.coe_nat_monoid_hom :

prime_multiset →+ multiset ℕ

prime_multiset.coe, the coercion from a multiset of primes to a multiset of naturals, promoted to an add_monoid_hom.

Equations

prime_multiset.coe_nat_monoid_hom = {to_fun := coe coe_to_lift, map_zero' := prime_multiset.coe_nat_monoid_hom._proof_1, map_add' := prime_multiset.coe_nat_monoid_hom._proof_2}

@[simp]

theorem prime_multiset.coe_coe_nat_monoid_hom :

⇑prime_multiset.coe_nat_monoid_hom = coe

theorem prime_multiset.coe_nat_injective :

function.injective coe

theorem prime_multiset.coe_nat_of_prime (p : nat.primes) :

↑(prime_multiset.of_prime p) = {↑p}

theorem prime_multiset.coe_nat_prime (v : prime_multiset) (p : ℕ) (h : p ∈ ↑v) :

def prime_multiset.to_pnat_multiset :

prime_multiset → multiset ℕ+

Converts a prime_multiset to a multiset ℕ+.

Equations

prime_multiset.to_pnat_multiset = λ (v : prime_multiset), multiset.map (λ (p : nat.primes), ↑p) v

@[protected, instance]

def prime_multiset.coe_pnat :

has_coe prime_multiset (multiset ℕ+)

Equations

prime_multiset.coe_pnat = {coe := prime_multiset.to_pnat_multiset}

def prime_multiset.coe_pnat_monoid_hom :

prime_multiset →+ multiset ℕ+

coe_pnat, the coercion from a multiset of primes to a multiset of positive naturals, regarded as an add_monoid_hom.

Equations

prime_multiset.coe_pnat_monoid_hom = {to_fun := coe coe_to_lift, map_zero' := prime_multiset.coe_pnat_monoid_hom._proof_1, map_add' := prime_multiset.coe_pnat_monoid_hom._proof_2}

@[simp]

theorem prime_multiset.coe_coe_pnat_monoid_hom :

⇑prime_multiset.coe_pnat_monoid_hom = coe

theorem prime_multiset.coe_pnat_injective :

function.injective coe

theorem prime_multiset.coe_pnat_of_prime (p : nat.primes) :

↑(prime_multiset.of_prime p) = {↑p}

theorem prime_multiset.coe_pnat_prime (v : prime_multiset) (p : ℕ+) (h : p ∈ ↑v) :

@[protected, instance]

def prime_multiset.coe_multiset_pnat_nat :

has_coe (multiset ℕ+) (multiset ℕ)

Equations

prime_multiset.coe_multiset_pnat_nat = {coe := λ (v : multiset ℕ+), multiset.map (λ (n : ℕ+), ↑n) v}

theorem prime_multiset.coe_pnat_nat (v : prime_multiset) :

def prime_multiset.prod (v : prime_multiset) :

The product of a prime_multiset, as a ℕ+.

Equations

v.prod = ↑v.prod

theorem prime_multiset.coe_prod (v : prime_multiset) :

↑(v.prod) = ↑v.prod

theorem prime_multiset.prod_of_prime (p : nat.primes) :

(prime_multiset.of_prime p).prod = ↑p

def prime_multiset.of_nat_multiset (v : multiset ℕ) (h : ∀ (p : ℕ), p ∈ v → nat.prime p) :

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

Equations

prime_multiset.of_nat_multiset v h = multiset.pmap (λ (p : ℕ) (hp : nat.prime p), ⟨p, hp⟩) v h

theorem prime_multiset.to_of_nat_multiset (v : multiset ℕ) (h : ∀ (p : ℕ), p ∈ v → nat.prime p) :

↑(prime_multiset.of_nat_multiset v h) = v

theorem prime_multiset.prod_of_nat_multiset (v : multiset ℕ) (h : ∀ (p : ℕ), p ∈ v → nat.prime p) :

↑((prime_multiset.of_nat_multiset v h).prod) = v.prod

def prime_multiset.of_pnat_multiset (v : multiset ℕ+) (h : ∀ (p : ℕ+), p ∈ v → p.prime) :

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

Equations

prime_multiset.of_pnat_multiset v h = multiset.pmap (λ (p : ℕ+) (hp : p.prime), ⟨↑p, hp⟩) v h

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

↑(prime_multiset.of_pnat_multiset v h) = v

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

(prime_multiset.of_pnat_multiset v h).prod = v.prod

def prime_multiset.of_nat_list (l : list ℕ) (h : ∀ (p : ℕ), p ∈ l → nat.prime p) :

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

Equations

prime_multiset.of_nat_list l h = prime_multiset.of_nat_multiset ↑l h

theorem prime_multiset.prod_of_nat_list (l : list ℕ) (h : ∀ (p : ℕ), p ∈ l → nat.prime p) :

↑((prime_multiset.of_nat_list l h).prod) = l.prod

def prime_multiset.of_pnat_list (l : list ℕ+) (h : ∀ (p : ℕ+), p ∈ l → p.prime) :

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

Equations

prime_multiset.of_pnat_list l h = prime_multiset.of_pnat_multiset ↑l h

theorem prime_multiset.prod_of_pnat_list (l : list ℕ+) (h : ∀ (p : ℕ+), p ∈ l → p.prime) :

(prime_multiset.of_pnat_list l h).prod = 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

def pnat.factor_multiset (n : ℕ+) :

The prime factors of n, regarded as a multiset

Equations

n.factor_multiset = prime_multiset.of_nat_list ↑n.factors _

theorem pnat.prod_factor_multiset (n : ℕ+) :

n.factor_multiset.prod = n

The product of the factors is the original number

theorem pnat.coe_nat_factor_multiset (n : ℕ+) :

↑(n.factor_multiset) = ↑(↑n.factors)

theorem prime_multiset.factor_multiset_prod (v : prime_multiset) :

v.prod.factor_multiset = v

If we start with a multiset of primes, take the product and then factor it, we get back the original multiset.

def pnat.factor_multiset_equiv :

ℕ+ ≃ prime_multiset

Positive integers biject with multisets of primes.

Equations

pnat.factor_multiset_equiv = {to_fun := pnat.factor_multiset, inv_fun := prime_multiset.prod, left_inv := pnat.prod_factor_multiset, right_inv := prime_multiset.factor_multiset_prod}

theorem pnat.factor_multiset_one :

1.factor_multiset = 0

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

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

(n * m).factor_multiset = n.factor_multiset + m.factor_multiset

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

(n ^ m).factor_multiset = m • n.factor_multiset

theorem pnat.factor_multiset_of_prime (p : nat.primes) :

↑p.factor_multiset = prime_multiset.of_prime p

Factoring a prime gives the corresponding one-element multiset.

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

m.factor_multiset ≤ n.factor_multiset ↔ 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.factor_multiset_le_iff' {m : ℕ+} {v : prime_multiset} :

m.factor_multiset ≤ v ↔ m ∣ v.prod

theorem prime_multiset.prod_dvd_iff {u v : prime_multiset} :

u.prod ∣ v.prod ↔ u ≤ v

theorem prime_multiset.prod_dvd_iff' {u : prime_multiset} {n : ℕ+} :

u.prod ∣ n ↔ u ≤ n.factor_multiset

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

(m.gcd n).factor_multiset = m.factor_multiset ⊓ n.factor_multiset

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

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

(m.lcm n).factor_multiset = m.factor_multiset ⊔ n.factor_multiset

theorem pnat.count_factor_multiset (m : ℕ+) (p : nat.primes) (k : ℕ) :

↑p ^ k ∣ m ↔ k ≤ multiset.count p m.factor_multiset

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

theorem prime_multiset.prod_inf (u v : prime_multiset) :

(u ⊓ v).prod = u.prod.gcd v.prod

theorem prime_multiset.prod_sup (u v : prime_multiset) :

(u ⊔ v).prod = u.prod.lcm v.prod