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.
prime_multiset.coe, the coercion from a multiset of primes to a multiset of
naturals, promoted to an
coe_pnat, the coercion from a multiset of primes to a multiset of positive
naturals, regarded as an