The type of multisets of prime numbers. Unique factorization gives an equivalence between this set and ℕ+, as we will formalize below.
Equations
Equations
- prime_multiset.inhabited = prime_multiset.inhabited._proof_1.mpr multiset.inhabited
Equations
Equations
The multiset consisting of a single prime
Equations
- prime_multiset.of_prime p = p :: 0
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
Equations
Equations
Equations
- prime_multiset.to_pnat_multiset = λ (v : prime_multiset), multiset.map (λ (p : nat.primes), ↑p) v
Equations
Equations
Equations
- prime_multiset.of_nat_multiset v h = multiset.pmap (λ (p : ℕ) (hp : nat.prime p), ⟨p, hp⟩) v h
Equations
- prime_multiset.of_pnat_multiset v h = multiset.pmap (λ (p : ℕ+) (hp : p.prime), ⟨↑p, hp⟩) v h
Lists can be coerced to multisets; here we have some results about how this interacts with our constructions on multisets.
Equations
Equations
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
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.
Factoring gives a homomorphism from the multiplicative monoid ℕ+ to the additive monoid of multisets.
Factoring a prime gives the corresponding one-element multiset.
We now have four different results that all encode the idea that inequality of multisets corresponds to divisibility of positive integers.
The gcd and lcm operations on positive integers correspond to the inf and sup operations on multisets.
The number of occurrences of p in the factor multiset of m is the same as the p-adic valuation of m.