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 #

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

The multiset consisting of a single prime

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

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

Equations

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

Equations

The product of a prime_multiset, as a ℕ+.

Equations

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

Equations

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

Equations

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

Equations

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

Equations
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

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.

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.