Documentation

Mathlib.Data.Nat.Factorization.Basic

Prime factorizations #

n.factorization is the finitely supported function ℕ →₀ ℕ mapping each prime factor of n to its multiplicity in n. For example, since 2000 = 2^4 * 5^3,

TODO #

n.factorization is the finitely supported function ℕ →₀ ℕ mapping each prime factor of n to its multiplicity in n.

Equations
  • n.factorization = { support := n.primeFactors, toFun := fun (p : ) => if Nat.Prime p then padicValNat p n else 0, mem_support_toFun := }
Instances For
    @[simp]
    theorem Nat.support_factorization (n : ) :
    n.factorization.support = n.primeFactors

    The support of n.factorization is exactly n.primeFactors.

    theorem Nat.factorization_def (n : ) {p : } (pp : Nat.Prime p) :
    n.factorization p = padicValNat p n
    @[simp]
    theorem Nat.factors_count_eq {n : } {p : } :
    List.count p n.factors = n.factorization p

    We can write both n.factorization p and n.factors.count p to represent the power of p in the factorization of n: we declare the former to be the simp-normal form.

    theorem Nat.factorization_eq_factors_multiset (n : ) :
    n.factorization = Multiset.toFinsupp n.factors
    theorem Nat.multiplicity_eq_factorization {n : } {p : } (pp : Nat.Prime p) (hn : n 0) :
    multiplicity p n = (n.factorization p)

    Basic facts about factorization #

    @[simp]
    theorem Nat.factorization_prod_pow_eq_self {n : } (hn : n 0) :
    (n.factorization.prod fun (x x_1 : ) => x ^ x_1) = n
    theorem Nat.eq_of_factorization_eq {a : } {b : } (ha : a 0) (hb : b 0) (h : ∀ (p : ), a.factorization p = b.factorization p) :
    a = b

    Every nonzero natural number has a unique prime factorization

    Lemmas characterising when n.factorization p = 0 #

    theorem Nat.factorization_eq_zero_iff (n : ) (p : ) :
    n.factorization p = 0 ¬Nat.Prime p ¬p n n = 0
    @[simp]
    theorem Nat.factorization_eq_zero_of_non_prime (n : ) {p : } (hp : ¬Nat.Prime p) :
    n.factorization p = 0
    theorem Nat.factorization_eq_zero_of_not_dvd {n : } {p : } (h : ¬p n) :
    n.factorization p = 0
    theorem Nat.factorization_eq_zero_of_lt {n : } {p : } (h : n < p) :
    n.factorization p = 0
    @[simp]
    theorem Nat.factorization_zero_right (n : ) :
    n.factorization 0 = 0
    @[simp]
    theorem Nat.factorization_one_right (n : ) :
    n.factorization 1 = 0
    theorem Nat.dvd_of_factorization_pos {n : } {p : } (hn : n.factorization p 0) :
    p n
    theorem Nat.Prime.factorization_pos_of_dvd {n : } {p : } (hp : Nat.Prime p) (hn : n 0) (h : p n) :
    0 < n.factorization p
    theorem Nat.factorization_eq_zero_of_remainder {p : } {r : } (i : ) (hr : ¬p r) :
    (p * i + r).factorization p = 0
    theorem Nat.factorization_eq_zero_iff_remainder {p : } {r : } (i : ) (pp : Nat.Prime p) (hr0 : r 0) :
    ¬p r (p * i + r).factorization p = 0
    theorem Nat.factorization_eq_zero_iff' (n : ) :
    n.factorization = 0 n = 0 n = 1

    The only numbers with empty prime factorization are 0 and 1

    Lemmas about factorizations of products and powers #

    @[simp]
    theorem Nat.factorization_mul {a : } {b : } (ha : a 0) (hb : b 0) :
    (a * b).factorization = a.factorization + b.factorization

    For nonzero a and b, the power of p in a * b is the sum of the powers in a and b

    theorem Nat.prod_factorization_eq_prod_primeFactors {n : } {β : Type u_1} [CommMonoid β] (f : β) :
    n.factorization.prod f = pn.primeFactors, f p (n.factorization p)

    A product over n.factorization can be written as a product over n.primeFactors;

    theorem Nat.prod_primeFactors_prod_factorization {n : } {β : Type u_1} [CommMonoid β] (f : β) :
    pn.primeFactors, f p = n.factorization.prod fun (p x : ) => f p

    A product over n.primeFactors can be written as a product over n.factorization;

    theorem Nat.factorization_prod {α : Type u_1} {S : Finset α} {g : α} (hS : xS, g x 0) :
    (S.prod g).factorization = xS, (g x).factorization

    For any p : ℕ and any function g : α → ℕ that's non-zero on S : Finset α, the power of p in S.prod g equals the sum over x ∈ S of the powers of p in g x. Generalises factorization_mul, which is the special case where S.card = 2 and g = id.

    @[simp]
    theorem Nat.factorization_pow (n : ) (k : ) :
    (n ^ k).factorization = k n.factorization

    For any p, the power of p in n^k is k times the power in n

    Lemmas about factorizations of primes and prime powers #

    @[simp]
    theorem Nat.Prime.factorization {p : } (hp : Nat.Prime p) :
    p.factorization = Finsupp.single p 1

    The only prime factor of prime p is p itself, with multiplicity 1

    @[simp]
    theorem Nat.Prime.factorization_self {p : } (hp : Nat.Prime p) :
    p.factorization p = 1

    The multiplicity of prime p in p is 1

    theorem Nat.Prime.factorization_pow {p : } {k : } (hp : Nat.Prime p) :
    (p ^ k).factorization = Finsupp.single p k

    For prime p the only prime factor of p^k is p with multiplicity k

    theorem Nat.eq_pow_of_factorization_eq_single {n : } {p : } {k : } (hn : n 0) (h : n.factorization = Finsupp.single p k) :
    n = p ^ k

    If the factorization of n contains just one number p then n is a power of p

    theorem Nat.Prime.eq_of_factorization_pos {p : } {q : } (hp : Nat.Prime p) (h : p.factorization q 0) :
    p = q

    The only prime factor of prime p is p itself.

    Equivalence between ℕ+ and ℕ →₀ ℕ with support in the primes. #

    theorem Nat.prod_pow_factorization_eq_self {f : →₀ } (hf : pf.support, Nat.Prime p) :
    (f.prod fun (x x_1 : ) => x ^ x_1).factorization = f

    Any Finsupp f : ℕ →₀ ℕ whose support is in the primes is equal to the factorization of the product ∏ (a : ℕ) ∈ f.support, a ^ f a.

    theorem Nat.eq_factorization_iff {n : } {f : →₀ } (hn : n 0) (hf : pf.support, Nat.Prime p) :
    f = n.factorization (f.prod fun (x x_1 : ) => x ^ x_1) = n
    def Nat.factorizationEquiv :
    ℕ+ {f : →₀ | pf.support, Nat.Prime p}

    The equiv between ℕ+ and ℕ →₀ ℕ with support in the primes.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Nat.factorizationEquiv_apply (n : ℕ+) :
      (Nat.factorizationEquiv n) = (n).factorization
      theorem Nat.factorizationEquiv_inv_apply {f : →₀ } (hf : pf.support, Nat.Prime p) :
      (Nat.factorizationEquiv.symm f, hf) = f.prod fun (x x_1 : ) => x ^ x_1

      Generalisation of the "even part" and "odd part" of a natural number #

      We introduce the notations ord_proj[p] n for the largest power of the prime p that divides n and ord_compl[p] n for the complementary part. The ord naming comes from the $p$-adic order/valuation of a number, and proj and compl are for the projection and complementary projection. The term n.factorization p is the $p$-adic order itself. For example, ord_proj[2] n is the even part of n and ord_compl[2] n is the odd part.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Nat.ord_proj_of_not_prime (n : ) (p : ) (hp : ¬Nat.Prime p) :
          p ^ n.factorization p = 1
          @[simp]
          theorem Nat.ord_compl_of_not_prime (n : ) (p : ) (hp : ¬Nat.Prime p) :
          n / p ^ n.factorization p = n
          theorem Nat.ord_proj_dvd (n : ) (p : ) :
          p ^ n.factorization p n
          theorem Nat.ord_compl_dvd (n : ) (p : ) :
          n / p ^ n.factorization p n
          theorem Nat.ord_proj_pos (n : ) (p : ) :
          0 < p ^ n.factorization p
          theorem Nat.ord_proj_le {n : } (p : ) (hn : n 0) :
          p ^ n.factorization p n
          theorem Nat.ord_compl_pos {n : } (p : ) (hn : n 0) :
          0 < n / p ^ n.factorization p
          theorem Nat.ord_compl_le (n : ) (p : ) :
          n / p ^ n.factorization p n
          theorem Nat.ord_proj_mul_ord_compl_eq_self (n : ) (p : ) :
          p ^ n.factorization p * (n / p ^ n.factorization p) = n
          theorem Nat.ord_proj_mul {a : } {b : } (p : ) (ha : a 0) (hb : b 0) :
          p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p
          theorem Nat.ord_compl_mul (a : ) (b : ) (p : ) :
          a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

          Factorization and divisibility #

          theorem Nat.factorization_lt {n : } (p : ) (hn : n 0) :
          n.factorization p < n

          A crude upper bound on n.factorization p

          theorem Nat.factorization_le_of_le_pow {n : } {p : } {b : } (hb : n p ^ b) :
          n.factorization p b

          An upper bound on n.factorization p

          theorem Nat.factorization_le_iff_dvd {d : } {n : } (hd : d 0) (hn : n 0) :
          d.factorization n.factorization d n
          theorem Nat.factorization_prime_le_iff_dvd {d : } {n : } (hd : d 0) (hn : n 0) :
          (∀ (p : ), Nat.Prime pd.factorization p n.factorization p) d n
          theorem Nat.pow_succ_factorization_not_dvd {n : } {p : } (hn : n 0) (hp : Nat.Prime p) :
          ¬p ^ (n.factorization p + 1) n
          theorem Nat.factorization_le_factorization_mul_left {a : } {b : } (hb : b 0) :
          a.factorization (a * b).factorization
          theorem Nat.factorization_le_factorization_mul_right {a : } {b : } (ha : a 0) :
          b.factorization (a * b).factorization
          theorem Nat.Prime.pow_dvd_iff_le_factorization {p : } {k : } {n : } (pp : Nat.Prime p) (hn : n 0) :
          p ^ k n k n.factorization p
          theorem Nat.Prime.pow_dvd_iff_dvd_ord_proj {p : } {k : } {n : } (pp : Nat.Prime p) (hn : n 0) :
          p ^ k n p ^ k p ^ n.factorization p
          theorem Nat.Prime.dvd_iff_one_le_factorization {p : } {n : } (pp : Nat.Prime p) (hn : n 0) :
          p n 1 n.factorization p
          theorem Nat.exists_factorization_lt_of_lt {a : } {b : } (ha : a 0) (hab : a < b) :
          ∃ (p : ), a.factorization p < b.factorization p
          @[simp]
          theorem Nat.factorization_div {d : } {n : } (h : d n) :
          (n / d).factorization = n.factorization - d.factorization
          theorem Nat.dvd_ord_proj_of_dvd {n : } {p : } (hn : n 0) (pp : Nat.Prime p) (h : p n) :
          p p ^ n.factorization p
          theorem Nat.not_dvd_ord_compl {n : } {p : } (hp : Nat.Prime p) (hn : n 0) :
          ¬p n / p ^ n.factorization p
          theorem Nat.coprime_ord_compl {n : } {p : } (hp : Nat.Prime p) (hn : n 0) :
          p.Coprime (n / p ^ n.factorization p)
          theorem Nat.factorization_ord_compl (n : ) (p : ) :
          (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
          theorem Nat.dvd_ord_compl_of_dvd_not_dvd {p : } {d : } {n : } (hdn : d n) (hpd : ¬p d) :
          d n / p ^ n.factorization p
          theorem Nat.exists_eq_pow_mul_and_not_dvd {n : } (hn : n 0) (p : ) (hp : p 1) :
          ∃ (e : ) (n' : ), ¬p n' n = p ^ e * n'

          If n is a nonzero natural number and p ≠ 1, then there are natural numbers e and n' such that n' is not divisible by p and n = p^e * n'.

          theorem Nat.exists_eq_two_pow_mul_odd {n : } (hn : n 0) :
          ∃ (k : ) (m : ), Odd m n = 2 ^ k * m

          Any nonzero natural number is the product of an odd part m and a power of two 2 ^ k.

          theorem Nat.dvd_iff_div_factorization_eq_tsub {d : } {n : } (hd : d 0) (hdn : d n) :
          d n (n / d).factorization = n.factorization - d.factorization
          theorem Nat.ord_proj_dvd_ord_proj_of_dvd {a : } {b : } (hb0 : b 0) (hab : a b) (p : ) :
          p ^ a.factorization p p ^ b.factorization p
          theorem Nat.ord_proj_dvd_ord_proj_iff_dvd {a : } {b : } (ha0 : a 0) (hb0 : b 0) :
          (∀ (p : ), p ^ a.factorization p p ^ b.factorization p) a b
          theorem Nat.ord_compl_dvd_ord_compl_of_dvd {a : } {b : } (hab : a b) (p : ) :
          a / p ^ a.factorization p b / p ^ b.factorization p
          theorem Nat.ord_compl_dvd_ord_compl_iff_dvd (a : ) (b : ) :
          (∀ (p : ), a / p ^ a.factorization p b / p ^ b.factorization p) a b
          theorem Nat.dvd_iff_prime_pow_dvd_dvd (n : ) (d : ) :
          d n ∀ (p k : ), Nat.Prime pp ^ k dp ^ k n
          theorem Nat.prod_primeFactors_dvd (n : ) :
          pn.primeFactors, p n
          theorem Nat.factorization_gcd {a : } {b : } (ha_pos : a 0) (hb_pos : b 0) :
          (a.gcd b).factorization = a.factorization b.factorization
          theorem Nat.factorization_lcm {a : } {b : } (ha : a 0) (hb : b 0) :
          (a.lcm b).factorization = a.factorization b.factorization

          If a = ∏ pᵢ ^ nᵢ and b = ∏ pᵢ ^ mᵢ, then factorizationLCMLeft = ∏ pᵢ ^ kᵢ, where kᵢ = nᵢ if mᵢ ≤ nᵢ and 0 otherwise. Note that the product is over the divisors of lcm a b, so if one of a or b is 0 then the result is 1.

          Equations
          • a.factorizationLCMLeft b = (a.lcm b).factorization.prod fun (p n : ) => if b.factorization p a.factorization p then p ^ n else 1
          Instances For

            If a = ∏ pᵢ ^ nᵢ and b = ∏ pᵢ ^ mᵢ, then factorizationLCMRight = ∏ pᵢ ^ kᵢ, where kᵢ = mᵢ if nᵢ < mᵢ and 0 otherwise. Note that the product is over the divisors of lcm a b, so if one of a or b is 0 then the result is 1.

            Note that factorizationLCMRight a b is not factorizationLCMLeft b a: the difference is that in factorizationLCMLeft a b there are the primes whose exponent in a is bigger or equal than the exponent in b, while in factorizationLCMRight a b there are the primes whose exponent in b is strictly bigger than in a. For example factorizationLCMLeft 2 2 = 2, but factorizationLCMRight 2 2 = 1.

            Equations
            • a.factorizationLCMRight b = (a.lcm b).factorization.prod fun (p n : ) => if b.factorization p a.factorization p then 1 else p ^ n
            Instances For
              @[simp]
              theorem Nat.factorizationLCMLeft_zero_right (a : ) :
              a.factorizationLCMLeft 0 = 1
              @[simp]
              theorem Nat.factorizationLCMRight_zero_right (a : ) :
              a.factorizationLCMRight 0 = 1
              theorem Nat.factorizationLCMLeft_pos (a : ) (b : ) :
              0 < a.factorizationLCMLeft b
              theorem Nat.factorizationLCMRight_pos (a : ) (b : ) :
              0 < a.factorizationLCMRight b
              theorem Nat.coprime_factorizationLCMLeft_factorizationLCMRight (a : ) (b : ) :
              (a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)
              theorem Nat.factorizationLCMLeft_mul_factorizationLCMRight {a : } {b : } (ha : a 0) (hb : b 0) :
              a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b
              theorem Nat.factorizationLCMLeft_dvd_left (a : ) (b : ) :
              a.factorizationLCMLeft b a
              theorem Nat.factorizationLCMRight_dvd_right (a : ) (b : ) :
              a.factorizationLCMRight b b
              theorem Nat.sum_primeFactors_gcd_add_sum_primeFactors_mul {β : Type u_1} [AddCommMonoid β] (m : ) (n : ) (f : β) :
              (m.gcd n).primeFactors.sum f + (m * n).primeFactors.sum f = m.primeFactors.sum f + n.primeFactors.sum f
              theorem Nat.prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type u_1} [CommMonoid β] (m : ) (n : ) (f : β) :
              (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
              theorem Nat.setOf_pow_dvd_eq_Icc_factorization {n : } {p : } (pp : Nat.Prime p) (hn : n 0) :
              {i : | i 0 p ^ i n} = Set.Icc 1 (n.factorization p)
              theorem Nat.Icc_factorization_eq_pow_dvd (n : ) {p : } (pp : Nat.Prime p) :
              Finset.Icc 1 (n.factorization p) = Finset.filter (fun (i : ) => p ^ i n) (Finset.Ico 1 n)

              The set of positive powers of prime p that divide n is exactly the set of positive natural numbers up to n.factorization p.

              theorem Nat.factorization_eq_card_pow_dvd (n : ) {p : } (pp : Nat.Prime p) :
              n.factorization p = (Finset.filter (fun (i : ) => p ^ i n) (Finset.Ico 1 n)).card
              theorem Nat.Ico_filter_pow_dvd_eq {n : } {p : } {b : } (pp : Nat.Prime p) (hn : n 0) (hb : n p ^ b) :
              Finset.filter (fun (i : ) => p ^ i n) (Finset.Ico 1 n) = Finset.filter (fun (i : ) => p ^ i n) (Finset.Icc 1 b)

              Factorization and coprimes #

              theorem Nat.factorization_mul_apply_of_coprime {p : } {a : } {b : } (hab : a.Coprime b) :
              (a * b).factorization p = a.factorization p + b.factorization p

              For coprime a and b, the power of p in a * b is the sum of the powers in a and b

              theorem Nat.factorization_mul_of_coprime {a : } {b : } (hab : a.Coprime b) :
              (a * b).factorization = a.factorization + b.factorization

              For coprime a and b, the power of p in a * b is the sum of the powers in a and b

              theorem Nat.factorization_eq_of_coprime_left {p : } {a : } {b : } (hab : a.Coprime b) (hpa : p a.factors) :
              (a * b).factorization p = a.factorization p

              If p is a prime factor of a then the power of p in a is the same that in a * b, for any b coprime to a.

              theorem Nat.factorization_eq_of_coprime_right {p : } {a : } {b : } (hab : a.Coprime b) (hpb : p b.factors) :
              (a * b).factorization p = b.factorization p

              If p is a prime factor of b then the power of p in b is the same that in a * b, for any a coprime to b.

              Induction principles involving factorizations #

              def Nat.recOnPrimePow {P : Sort u_1} (h0 : P 0) (h1 : P 1) (h : (a p n : ) → Nat.Prime p¬p a0 < nP aP (p ^ n * a)) (a : ) :
              P a

              Given P 0, P 1 and a way to extend P a to P (p ^ n * a) for prime p not dividing a, we can define P for all natural numbers.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Nat.recOnPosPrimePosCoprime {P : Sort u_1} (hp : (p n : ) → Nat.Prime p0 < nP (p ^ n)) (h0 : P 0) (h1 : P 1) (h : (a b : ) → 1 < a1 < ba.Coprime bP aP bP (a * b)) (a : ) :
                P a

                Given P 0, P 1, and P (p ^ n) for positive prime powers, and a way to extend P a and P b to P (a * b) when a, b are positive coprime, we can define P for all natural numbers.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Nat.recOnPrimeCoprime {P : Sort u_1} (h0 : P 0) (hp : (p n : ) → Nat.Prime pP (p ^ n)) (h : (a b : ) → 1 < a1 < ba.Coprime bP aP bP (a * b)) (a : ) :
                  P a

                  Given P 0, P (p ^ n) for all prime powers, and a way to extend P a and P b to P (a * b) when a, b are positive coprime, we can define P for all natural numbers.

                  Equations
                  Instances For
                    def Nat.recOnMul {P : Sort u_1} (h0 : P 0) (h1 : P 1) (hp : (p : ) → Nat.Prime pP p) (h : (a b : ) → P aP bP (a * b)) (a : ) :
                    P a

                    Given P 0, P 1, P p for all primes, and a way to extend P a and P b to P (a * b), we can define P for all natural numbers.

                    Equations
                    Instances For
                      def Nat.recOnMul.hp'' {P : Sort u_1} (h1 : P 1) (hp : (p : ) → Nat.Prime pP p) (h : (a b : ) → P aP bP (a * b)) (p : ) (n : ) (hp' : Nat.Prime p) :
                      P (p ^ n)

                      The predicate holds on prime powers

                      Equations
                      Instances For
                        theorem Nat.multiplicative_factorization {β : Type u_1} [CommMonoid β] (f : β) (h_mult : ∀ (x y : ), x.Coprime yf (x * y) = f x * f y) (hf : f 1 = 1) {n : } :
                        n 0f n = n.factorization.prod fun (p k : ) => f (p ^ k)

                        For any multiplicative function f with f 1 = 1 and any n ≠ 0, we can evaluate f n by evaluating f at p ^ k over the factorization of n

                        theorem Nat.multiplicative_factorization' {n : } {β : Type u_1} [CommMonoid β] (f : β) (h_mult : ∀ (x y : ), x.Coprime yf (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) :
                        f n = n.factorization.prod fun (p k : ) => f (p ^ k)

                        For any multiplicative function f with f 1 = 1 and f 0 = 1, we can evaluate f n by evaluating f at p ^ k over the factorization of n

                        theorem Nat.eq_iff_prime_padicValNat_eq (a : ) (b : ) (ha : a 0) (hb : b 0) :
                        a = b ∀ (p : ), Nat.Prime ppadicValNat p a = padicValNat p b

                        Two positive naturals are equal if their prime padic valuations are equal

                        theorem Nat.prod_pow_prime_padicValNat (n : ) (hn : n 0) (m : ) (pr : n < m) :

                        Lemmas about factorizations of particular functions #

                        theorem Nat.card_multiples (n : ) (p : ) :
                        (Finset.filter (fun (e : ) => p e + 1) (Finset.range n)).card = n / p

                        Exactly n / p naturals in [1, n] are multiples of p. See Nat.card_multiples' for an alternative spelling of the statement.

                        theorem Nat.Ioc_filter_dvd_card_eq_div (n : ) (p : ) :
                        (Finset.filter (fun (x : ) => p x) (Finset.Ioc 0 n)).card = n / p

                        Exactly n / p naturals in (0, n] are multiples of p.

                        theorem Nat.card_multiples' (N : ) (n : ) :
                        (Finset.filter (fun (k : ) => k 0 n k) (Finset.range N.succ)).card = N / n

                        There are exactly ⌊N/n⌋ positive multiples of n that are ≤ N. See Nat.card_multiples for a "shifted-by-one" version.