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

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

          Equations
          Instances For

            The product of a PrimeMultiset, as a ℕ+.

            Equations
            Instances For

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

              Equations
              Instances For
                @[simp]
                theorem PrimeMultiset.mem_ofNatMultiset {p : ℕ+} {s : Multiset } (hs : ps, Nat.Prime p) :
                @[simp]
                @[simp]
                theorem PrimeMultiset.prod_ofNatMultiset (v : Multiset ) (h : pv, Nat.Prime p) :

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

                Equations
                Instances For
                  @[simp]
                  @[simp]
                  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
                    @[simp]
                    theorem PrimeMultiset.mem_ofNatList {p : ℕ+} {l : List } (hl : pl, Nat.Prime p) :
                    @[simp]
                    theorem PrimeMultiset.prod_ofNatList (l : List ) (h : pl, Nat.Prime p) :
                    (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
                      @[simp]
                      theorem PrimeMultiset.toPNatMultiset_ofPNatList {l : List ℕ+} (hl : pl, p.Prime) :
                      @[simp]
                      theorem PrimeMultiset.prod_ofPNatList (l : List ℕ+) (h : pl, p.Prime) :
                      @[simp]

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

                      @[simp]
                      theorem PrimeMultiset.prod_add (u v : PrimeMultiset) :
                      (u + v).prod = u.prod * v.prod
                      @[simp]
                      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
                        @[simp]

                        The product of the factors is the original number

                        @[simp]

                        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
                          @[simp]

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

                          @[simp]

                          Factoring a prime gives the corresponding one-element multiset.

                          @[simp]

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

                          Alias of the reverse direction of PNat.factorMultiset_le_iff.


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

                          Alias of the reverse direction of PrimeMultiset.prod_dvd_iff.

                          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.