Documentation

Mathlib.Data.PNat.Factors

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 #

The type of multisets of prime numbers. Unique factorization gives an equivalence between this set and ℕ+, as we will formalize below.

Equations
Instances For

    The multiset consisting of a single prime

    Equations
    Instances For

      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
      Instances For

        PrimeMultiset.coe, the coercion from a multiset of primes to a multiset of naturals, promoted to an AddMonoidHom.

        Equations
        Instances For
          theorem PrimeMultiset.coeNat_prime (v : PrimeMultiset) (p : ) (h : p v.toNatMultiset) :

          Converts a PrimeMultiset to a Multiset ℕ+.

          Equations
          Instances For

            coePNat, the coercion from a multiset of primes to a multiset of positive naturals, regarded as an AddMonoidHom.

            Equations
            Instances For
              theorem PrimeMultiset.coePNat_prime (v : PrimeMultiset) (p : ℕ+) (h : p v.toPNatMultiset) :
              p.Prime
              theorem PrimeMultiset.coePNat_nat (v : PrimeMultiset) :
              Multiset.map PNat.val v.toPNatMultiset = v.toNatMultiset

              The product of a PrimeMultiset, as a ℕ+.

              Equations
              • v.prod = v.toPNatMultiset.prod
              Instances For
                theorem PrimeMultiset.coe_prod (v : PrimeMultiset) :
                v.prod = v.toNatMultiset.prod

                If a Multiset consists only of primes, it can be recast as a PrimeMultiset.

                Equations
                Instances For
                  theorem PrimeMultiset.to_ofNatMultiset (v : Multiset ) (h : pv, Nat.Prime p) :
                  (PrimeMultiset.ofNatMultiset v h).toNatMultiset = v
                  theorem PrimeMultiset.prod_ofNatMultiset (v : Multiset ) (h : pv, Nat.Prime p) :
                  (PrimeMultiset.ofNatMultiset v h).prod = v.prod
                  def PrimeMultiset.ofPNatMultiset (v : Multiset ℕ+) (h : pv, p.Prime) :

                  If a Multiset ℕ+ consists only of primes, it can be recast as a PrimeMultiset.

                  Equations
                  Instances For
                    theorem PrimeMultiset.to_ofPNatMultiset (v : Multiset ℕ+) (h : pv, p.Prime) :
                    (PrimeMultiset.ofPNatMultiset v h).toPNatMultiset = v
                    theorem PrimeMultiset.prod_ofPNatMultiset (v : Multiset ℕ+) (h : pv, p.Prime) :
                    def PrimeMultiset.ofNatList (l : List ) (h : pl, Nat.Prime p) :

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

                    Equations
                    Instances For
                      theorem PrimeMultiset.prod_ofNatList (l : List ) (h : pl, Nat.Prime p) :
                      (PrimeMultiset.ofNatList l h).prod = l.prod
                      def PrimeMultiset.ofPNatList (l : List ℕ+) (h : pl, p.Prime) :

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

                      Equations
                      Instances For
                        theorem PrimeMultiset.prod_ofPNatList (l : List ℕ+) (h : pl, p.Prime) :
                        (PrimeMultiset.ofPNatList l h).prod = l.prod

                        The product map gives a homomorphism from the additive monoid of multisets to the multiplicative monoid ℕ+.

                        theorem PrimeMultiset.prod_add (u : PrimeMultiset) (v : PrimeMultiset) :
                        (u + v).prod = u.prod * v.prod
                        theorem PrimeMultiset.prod_smul (d : ) (u : PrimeMultiset) :
                        (d u).prod = u.prod ^ d

                        The prime factors of n, regarded as a multiset

                        Equations
                        Instances For
                          theorem PNat.prod_factorMultiset (n : ℕ+) :
                          n.factorMultiset.prod = n

                          The product of the factors is the original number

                          theorem PNat.coeNat_factorMultiset (n : ℕ+) :
                          n.factorMultiset.toNatMultiset = (↑n).primeFactorsList
                          theorem PrimeMultiset.factorMultiset_prod (v : PrimeMultiset) :
                          v.prod.factorMultiset = v

                          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
                          Instances For

                            Factoring gives a homomorphism from the multiplicative monoid ℕ+ to the additive monoid of multisets.

                            theorem PNat.factorMultiset_mul (n : ℕ+) (m : ℕ+) :
                            (n * m).factorMultiset = n.factorMultiset + m.factorMultiset
                            theorem PNat.factorMultiset_pow (n : ℕ+) (m : ) :
                            (n ^ m).factorMultiset = m n.factorMultiset
                            theorem PNat.factorMultiset_ofPrime (p : Nat.Primes) :
                            (↑p).factorMultiset = PrimeMultiset.ofPrime p

                            Factoring a prime gives the corresponding one-element multiset.

                            theorem PNat.factorMultiset_le_iff {m : ℕ+} {n : ℕ+} :
                            m.factorMultiset n.factorMultiset m n

                            We now have four different results that all encode the idea that inequality of multisets corresponds to divisibility of positive integers.

                            theorem PNat.factorMultiset_le_iff' {m : ℕ+} {v : PrimeMultiset} :
                            m.factorMultiset v m v.prod
                            theorem PrimeMultiset.prod_dvd_iff' {u : PrimeMultiset} {n : ℕ+} :
                            u.prod n u n.factorMultiset
                            theorem PNat.factorMultiset_gcd (m : ℕ+) (n : ℕ+) :
                            (m.gcd n).factorMultiset = m.factorMultiset n.factorMultiset

                            The gcd and lcm operations on positive integers correspond to the inf and sup operations on multisets.

                            theorem PNat.factorMultiset_lcm (m : ℕ+) (n : ℕ+) :
                            (m.lcm n).factorMultiset = m.factorMultiset n.factorMultiset
                            theorem PNat.count_factorMultiset (m : ℕ+) (p : Nat.Primes) (k : ) :
                            p ^ k m k Multiset.count p m.factorMultiset

                            The number of occurrences of p in the factor multiset of m is the same as the p-adic valuation of m.

                            theorem PrimeMultiset.prod_inf (u : PrimeMultiset) (v : PrimeMultiset) :
                            (u v).prod = u.prod.gcd v.prod
                            theorem PrimeMultiset.prod_sup (u : PrimeMultiset) (v : PrimeMultiset) :
                            (u v).prod = u.prod.lcm v.prod