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 ofn
.
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
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
Instances For
Equations
- PrimeMultiset.coeNat = { coe := PrimeMultiset.toNatMultiset }
PrimeMultiset.coe
, the coercion from a multiset of primes to a multiset of
naturals, promoted to an AddMonoidHom
.
Equations
- PrimeMultiset.coeNatMonoidHom = { toFun := Coe.coe, map_zero' := PrimeMultiset.coeNatMonoidHom.proof_1, map_add' := PrimeMultiset.coeNatMonoidHom.proof_2 }
Instances For
Converts a PrimeMultiset
to a Multiset ℕ+
.
Equations
- v.toPNatMultiset = Multiset.map Coe.coe v
Instances For
Equations
- PrimeMultiset.coePNat = { coe := PrimeMultiset.toPNatMultiset }
coePNat
, the coercion from a multiset of primes to a multiset of positive
naturals, regarded as an AddMonoidHom
.
Equations
- PrimeMultiset.coePNatMonoidHom = { toFun := Coe.coe, map_zero' := PrimeMultiset.coePNatMonoidHom.proof_1, map_add' := PrimeMultiset.coePNatMonoidHom.proof_2 }
Instances For
Equations
- PrimeMultiset.coeMultisetPNatNat = { coe := fun (v : Multiset ℕ+) => Multiset.map Coe.coe v }
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
Instances For
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
Instances For
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
Instances For
If a List ℕ+
consists only of primes, it can be recast as a PrimeMultiset
with
the coercion from lists to multisets.
Equations
Instances For
The product map gives a homomorphism from the additive monoid of multisets to the multiplicative monoid ℕ+.
The prime factors of n, regarded as a multiset
Equations
- n.factorMultiset = PrimeMultiset.ofNatList (↑n).primeFactorsList ⋯
Instances For
The product of the factors is the original number
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
- PNat.factorMultisetEquiv = { toFun := PNat.factorMultiset, invFun := PrimeMultiset.prod, left_inv := PNat.prod_factorMultiset, right_inv := PrimeMultiset.factorMultiset_prod }
Instances For
Factoring gives a homomorphism from the multiplicative monoid ℕ+ to the additive monoid of multisets.
Factoring a prime gives the corresponding one-element multiset.
The number of occurrences of p in the factor multiset of m is the same as the p-adic valuation of m.