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
Main declarations #
prime_multiset: Type of multisets of prime numbers.
factor_multiset n: Multiset of prime factors of
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.