HepLean 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 #

source
def Nat.factorization (n : ℕ) :
ℕ →₀ ℕ

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
    source
    @[simp]
    theorem Nat.support_factorization (n : ℕ) :
    n.factorization.support = n.primeFactors

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

    source
    theorem Nat.factorization_def (n : ℕ) {p : ℕ} (pp : Nat.Prime p) :
    n.factorization p = padicValNat p n
    source
    @[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.

    source
    theorem Nat.factorization_eq_primeFactorsList_multiset (n : ℕ) :
    n.factorization = Multiset.toFinsupp ↑n.primeFactorsList
    source
    @[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.

    source
    @[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.

    source
    theorem Nat.Prime.factorization_pos_of_dvd {n : ℕ} {p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) (h : p ∣ n) :
    0 < n.factorization p
    source
    theorem Nat.multiplicity_eq_factorization {n : ℕ} {p : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) :
    multiplicity p n = n.factorization p

    Basic facts about factorization #

    source
    @[simp]
    theorem Nat.factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) :
    (n.factorization.prod fun (x1 x2 : ℕ) => x1 ^ x2) = n
    source
    theorem Nat.eq_of_factorization_eq {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : ℕ), a.factorization p = b.factorization p) :
    a = b
    source
    theorem Nat.factorization_inj :
    Set.InjOn Nat.factorization {x : ℕ | x ≠ 0}

    Every nonzero natural number has a unique prime factorization

    source
    @[simp]
    theorem Nat.factorization_zero :
    Nat.factorization 0 = 0
    source
    @[simp]
    theorem Nat.factorization_one :
    Nat.factorization 1 = 0

    Lemmas characterising when n.factorization p = 0 #

    source
    theorem Nat.factorization_eq_zero_iff (n : ℕ) (p : ℕ) :
    n.factorization p = 0 ↔ ¬Nat.Prime p ∨ ¬p ∣ n ∨ n = 0
    source
    @[simp]
    theorem Nat.factorization_eq_zero_of_non_prime (n : ℕ) {p : ℕ} (hp : ¬Nat.Prime p) :
    n.factorization p = 0
    source
    @[simp]
    theorem Nat.factorization_zero_right (n : ℕ) :
    n.factorization 0 = 0
    source
    theorem Nat.factorization_eq_zero_of_not_dvd {n : ℕ} {p : ℕ} (h : ¬p ∣ n) :
    n.factorization p = 0
    source
    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 #

    source
    @[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

    source
    theorem Nat.factorization_le_iff_dvd {d : ℕ} {n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :
    d.factorization ≤ n.factorization ↔ d ∣ n
    source
    theorem Nat.factorization_prod {α : Type u_1} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) :
    (S.prod g).factorization = ∑ x ∈ S, (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 = 2 and g = id.

    source
    @[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 #

    source
    @[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

    source
    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

    source
    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. #

    source
    theorem Nat.prod_pow_factorization_eq_self {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.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.

    source
    def Nat.factorizationEquiv :
    ℕ+ ≃ ↑{f : ℕ →₀ ℕ | ∀ p ∈ f.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 #

      source
      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

      source
      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.

      source
      def Nat.«termOrd_proj[_]_» :
      Lean.ParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Nat.«termOrd_compl[_]_» :
        Lean.ParserDescr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Nat.ord_proj_dvd (n : ℕ) (p : ℕ) :
          p ^ n.factorization p ∣ n

          Factorization LCM definitions #

          source
          def Nat.factorizationLCMLeft (a : ℕ) (b : ℕ) :
          ℕ

          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
            source
            def Nat.factorizationLCMRight (a : ℕ) (b : ℕ) :
            ℕ

            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