Documentation

Mathlib.Data.Nat.Factorization.Defs

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.primeFactorsList_count_eq {n : } {p : } :
    List.count p n.primeFactorsList = 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_primeFactorsList_multiset (n : ) :
    n.factorization = Multiset.toFinsupp n.primeFactorsList
    @[deprecated Nat.primeFactorsList_count_eq]
    theorem Nat.factors_count_eq {n : } {p : } :
    List.count p n.primeFactorsList = n.factorization p

    Alias of Nat.primeFactorsList_count_eq.


    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.

    @[deprecated Nat.factorization_eq_primeFactorsList_multiset]
    theorem Nat.factorization_eq_factors_multiset (n : ) :
    n.factorization = Multiset.toFinsupp n.primeFactorsList

    Alias of Nat.factorization_eq_primeFactorsList_multiset.

    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.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 (x1 x2 : ) => x1 ^ x2) = 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
    @[simp]
    theorem Nat.factorization_zero_right (n : ) :
    n.factorization 0 = 0
    theorem Nat.factorization_eq_zero_of_not_dvd {n : } {p : } (h : ¬p n) :
    n.factorization p = 0
    theorem Nat.factorization_eq_zero_of_remainder {p : } {r : } (i : ) (hr : ¬p r) :
    (p * i + r).factorization p = 0

    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.factorization_le_iff_dvd {d : } {n : } (hd : d 0) (hn : n 0) :
    d.factorization n.factorization d n
    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

    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.pow_succ_factorization_not_dvd {n : } {p : } (hn : n 0) (hp : Nat.Prime p) :
    ¬p ^ (n.factorization p + 1) n

    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 (x1 x2 : ) => x1 ^ x2).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.

    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

      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

      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
          theorem Nat.ord_proj_dvd (n : ) (p : ) :
          p ^ n.factorization p n

          Factorization LCM definitions #

          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