Mathlib.Data.Nat.Factorization.Defs

Module docstring

{"# 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, * factorization 2000 2 is 4 * factorization 2000 5 is 3 * factorization 2000 k is 0 for all other k : ℕ.

TODO

As discussed in this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/217875/topic/Multiplicity.20in.20the.20naturals We have lots of disparate ways of talking about the multiplicity of a prime in a natural number, including factors.count, padicValNat, multiplicity, and the material in Data/PNat/Factors. Move some of this material to this file, prove results about the relationships between these definitions, and (where appropriate) choose a uniform canonical way of expressing these ideas.
Moreover, the results here should be generalised to an arbitrary unique factorization monoid with a normalization function, and then deduplicated. The basics of this have been started in Mathlib/RingTheory/UniqueFactorizationDomain/.
Extend the inductions to any NormalizationMonoid with unique factorization.

","### Basic facts about factorization ","## Lemmas characterising when n.factorization p = 0 ","## Lemmas about factorizations of products and powers ","## Lemmas about factorizations of primes and prime powers ","### Equivalence between ℕ+ and ℕ →₀ ℕ with support in the primes. ","### Factorization and coprimes ","### Generalisation of the \"even part\" and \"odd part\" of a natural number ","### Factorization LCM definitions "}

Nat.factorization definition

(n : ℕ) : ℕ →₀ ℕ

Full source

/-- `n.factorization` is the finitely supported function `ℕ →₀ ℕ`
 mapping each prime factor of `n` to its multiplicity in `n`. -/
def factorization (n : ℕ) : ℕℕ →₀ ℕ where
  support := n.primeFactors
  toFun p := if p.Prime then padicValNat p n else 0
  mem_support_toFun := by simp [not_or]; aesop

Prime factorization function

Informal description

For a natural number $ n $, the function `n.factorization` is a finitely supported function $ \mathbb{N} \to \mathbb{N} $ that maps each prime factor $ p $ of $ n $ to its multiplicity in the prime factorization of $ n $, and maps all other natural numbers to 0.

Nat.support_factorization theorem

(n : ℕ) : (factorization n).support = n.primeFactors

Full source

/-- The support of `n.factorization` is exactly `n.primeFactors`. -/
@[simp] lemma support_factorization (n : ℕ) : (factorization n).support = n.primeFactors := rfl

Support of Prime Factorization Equals Prime Factors

Informal description

For any natural number $n$, the support of its prime factorization function (i.e., the set of primes appearing in its factorization) is exactly the set of prime factors of $n$.

Nat.factorization_def theorem

(n : ℕ) {p : ℕ} (pp : p.Prime) : n.factorization p = padicValNat p n

Full source

theorem factorization_def (n : ℕ) {p : ℕ} (pp : p.Prime) : n.factorization p = padicValNat p n := by
  simpa [factorization] using absurd pp

Factorization Equals p-adic Valuation for Primes

Informal description

For any natural number $n$ and any prime number $p$, the multiplicity of $p$ in the prime factorization of $n$ (denoted by $n.\text{factorization}(p)$) is equal to the $p$-adic valuation of $n$ (denoted by $\text{padicValNat}(p, n)$).

Nat.primeFactorsList_count_eq theorem

{n p : ℕ} : n.primeFactorsList.count p = n.factorization p

Full source

/-- 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. -/
@[simp]
theorem primeFactorsList_count_eq {n p : ℕ} : n.primeFactorsList.count p = n.factorization p := by
  rcases n.eq_zero_or_pos with (rfl | hn0)
  · simp [factorization, count]
  if pp : p.Prime then ?_ else
    rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]
    simp [factorization, pp]
  simp only [factorization_def _ pp]
  apply _root_.le_antisymm
  · rw [le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']
    exact List.le_count_iff_replicate_sublist.mp le_rfl |>.subperm
  · rw [← Nat.lt_add_one_iff, lt_iff_not_ge, ge_iff_le,
      le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']
    intro h
    have := h.count_le p
    simp at this

Equality of Prime Factor Count and Factorization Multiplicity

Informal description

For any natural numbers $n$ and $p$, the count of $p$ in the list of prime factors of $n$ is equal to the multiplicity of $p$ in the prime factorization of $n$, i.e., $\text{count}(p, n.\text{primeFactorsList}) = n.\text{factorization}(p)$.

Nat.factorization_eq_primeFactorsList_multiset theorem

(n : ℕ) : n.factorization = Multiset.toFinsupp (n.primeFactorsList : Multiset ℕ)

Full source

theorem factorization_eq_primeFactorsList_multiset (n : ℕ) :
    n.factorization = Multiset.toFinsupp (n.primeFactorsList : Multiset ℕ) := by
  ext p
  simp

Factorization as Multiset of Prime Factors

Informal description

For any natural number $n$, the prime factorization function $n.\text{factorization}$ is equal to the finitely supported function obtained by converting the multiset of prime factors of $n$ (given by $n.\text{primeFactorsList}$) into a finitely supported function $\mathbb{N} \to \mathbb{N}$ that counts multiplicities.

Nat.Prime.factorization_pos_of_dvd theorem

{n p : ℕ} (hp : p.Prime) (hn : n ≠ 0) (h : p ∣ n) : 0 < n.factorization p

Full source

theorem Prime.factorization_pos_of_dvd {n p : ℕ} (hp : p.Prime) (hn : n ≠ 0) (h : p ∣ n) :
    0 < n.factorization p := by
  rwa [← primeFactorsList_count_eq, count_pos_iff, mem_primeFactorsList_iff_dvd hn hp]

Positivity of Prime Multiplicity in Factorization for Divisors

Informal description

For any prime number $p$ and any nonzero natural number $n$, if $p$ divides $n$, then the multiplicity of $p$ in the prime factorization of $n$ is positive, i.e., $n.\text{factorization}(p) > 0$.

Nat.multiplicity_eq_factorization theorem

{n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) : multiplicity p n = n.factorization p

Full source

theorem multiplicity_eq_factorization {n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) :
    multiplicity p n = n.factorization p := by
  simp [factorization, pp, padicValNat_def' pp.ne_one hn.bot_lt]

Multiplicity Equals Factorization Exponent for Primes

Informal description

For any prime number $p$ and any nonzero natural number $n$, the multiplicity of $p$ in the prime factorization of $n$ is equal to the exponent of $p$ in the factorization of $n$, i.e., $\text{multiplicity}(p, n) = n.\text{factorization}(p)$.

Nat.factorization_prod_pow_eq_self theorem

{n : ℕ} (hn : n ≠ 0) : n.factorization.prod (· ^ ·) = n

Full source

@[simp]
theorem factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) : n.factorization.prod (· ^ ·) = n := by
  rw [factorization_eq_primeFactorsList_multiset n]
  simp only [← prod_toMultiset, factorization, Multiset.prod_coe, Multiset.toFinsupp_toMultiset]
  exact prod_primeFactorsList hn

Prime Factorization Product Equals Original Number

Informal description

For any nonzero natural number $n$, the product of the prime powers in its factorization equals $n$ itself, i.e., \[ \prod_{p \text{ prime}} p^{v_p(n)} = n \] where $v_p(n)$ denotes the exponent of the prime $p$ in the factorization of $n$.

Nat.factorization_inj theorem

: Set.InjOn factorization {x : ℕ | x ≠ 0}

Full source

/-- Every nonzero natural number has a unique prime factorization -/
theorem factorization_inj : Set.InjOn factorization { x : ℕ | x ≠ 0 } := fun a ha b hb h =>
  eq_of_factorization_eq ha hb fun p => by simp [h]

Injectivity of Prime Factorization on Nonzero Natural Numbers

Informal description

The prime factorization function is injective on the set of nonzero natural numbers. That is, for any two nonzero natural numbers $n$ and $m$, if their prime factorizations are equal (i.e., $n.\text{factorization} = m.\text{factorization}$), then $n = m$.

Nat.factorization_zero theorem

: factorization 0 = 0

Full source

@[simp]
theorem factorization_zero : factorization 0 = 0 := by ext; simp [factorization]

Factorization of Zero is Zero

Informal description

The prime factorization of the natural number $0$ is the zero function, i.e., $0.\text{factorization} = 0$.

Nat.factorization_one theorem

: factorization 1 = 0

Full source

@[simp]
theorem factorization_one : factorization 1 = 0 := by ext; simp [factorization]

Factorization of One is Zero

Informal description

The prime factorization of the natural number $1$ is the zero function, i.e., $1.\text{factorization} = 0$.

Nat.factorization_eq_zero_iff theorem

(n p : ℕ) : n.factorization p = 0 ↔ ¬p.Prime ∨ ¬p ∣ n ∨ n = 0

Full source

theorem factorization_eq_zero_iff (n p : ℕ) :
    n.factorization p = 0 ↔ ¬p.Prime ∨ ¬p ∣ n ∨ n = 0 := by
  simp_rw [← not_mem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]

Characterization of Zero Multiplicity in Prime Factorization: $n.\text{factorization}(p) = 0 \leftrightarrow (¬\text{Prime}(p) ∨ ¬(p \mid n) ∨ n = 0)$

Informal description

For any natural numbers $n$ and $p$, the multiplicity of $p$ in the prime factorization of $n$ is zero if and only if either $p$ is not prime, or $p$ does not divide $n$, or $n = 0$.

Nat.factorization_eq_zero_of_non_prime theorem

(n : ℕ) {p : ℕ} (hp : ¬p.Prime) : n.factorization p = 0

Full source

@[simp]
theorem factorization_eq_zero_of_non_prime (n : ℕ) {p : ℕ} (hp : ¬p.Prime) :
    n.factorization p = 0 := by simp [factorization_eq_zero_iff, hp]

Multiplicity of Non-Primes in Factorization is Zero

Informal description

For any natural number $n$ and any non-prime natural number $p$, the multiplicity of $p$ in the prime factorization of $n$ is zero, i.e., $n.\text{factorization}(p) = 0$.

Nat.factorization_zero_right theorem

(n : ℕ) : n.factorization 0 = 0

Full source

@[simp]
theorem factorization_zero_right (n : ℕ) : n.factorization 0 = 0 :=
  factorization_eq_zero_of_non_prime _ not_prime_zero

Zero Multiplicity in Prime Factorization is Zero

Informal description

For any natural number $n$, the multiplicity of $0$ in the prime factorization of $n$ is zero, i.e., $n.\text{factorization}(0) = 0$.

Nat.factorization_eq_zero_of_not_dvd theorem

{n p : ℕ} (h : ¬p ∣ n) : n.factorization p = 0

Full source

theorem factorization_eq_zero_of_not_dvd {n p : ℕ} (h : ¬p ∣ n) : n.factorization p = 0 := by
  simp [factorization_eq_zero_iff, h]

Vanishing of Prime Multiplicity for Non-Divisors

Informal description

For any natural numbers $n$ and $p$, if $p$ does not divide $n$, then the multiplicity of $p$ in the prime factorization of $n$ is zero, i.e., $n.\text{factorization}(p) = 0$.

Nat.factorization_eq_zero_of_remainder theorem

{p r : ℕ} (i : ℕ) (hr : ¬p ∣ r) : (p * i + r).factorization p = 0

Full source

theorem factorization_eq_zero_of_remainder {p r : ℕ} (i : ℕ) (hr : ¬p ∣ r) :
    (p * i + r).factorization p = 0 := by
  apply factorization_eq_zero_of_not_dvd
  rwa [← Nat.dvd_add_iff_right (Dvd.intro i rfl)]

Vanishing of Prime Multiplicity in Remainder Expression: $(p \cdot i + r).\text{factorization}(p) = 0$ when $p \nmid r$

Informal description

For any natural numbers $p$, $r$, and $i$, if $p$ does not divide $r$, then the multiplicity of $p$ in the prime factorization of $p \cdot i + r$ is zero, i.e., $(p \cdot i + r).\text{factorization}(p) = 0$.

Nat.factorization_mul theorem

{a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a * b).factorization = a.factorization + b.factorization

Full source

/-- For nonzero `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
@[simp]
theorem factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b).factorization = a.factorization + b.factorization := by
  ext p
  simp only [add_apply, ← primeFactorsList_count_eq,
    perm_iff_count.mp (perm_primeFactorsList_mul ha hb) p, count_append]

Multiplicativity of Prime Factorization: $(a \cdot b).\text{factorization} = a.\text{factorization} + b.\text{factorization}$ for $a, b \neq 0$

Informal description

For any nonzero natural numbers $a$ and $b$, the prime factorization of their product $a \cdot b$ is equal to the sum of their individual prime factorizations. That is, for every prime $p$, the multiplicity of $p$ in $a \cdot b$ equals the sum of its multiplicities in $a$ and $b$.

Nat.factorization_le_iff_dvd theorem

{d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : d.factorization ≤ n.factorization ↔ d ∣ n

Full source

theorem factorization_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :
    d.factorization ≤ n.factorization ↔ d ∣ n := by
  constructor
  · intro hdn
    set K := n.factorization - d.factorization with hK
    use K.prod (· ^ ·)
    rw [← factorization_prod_pow_eq_self hn, ← factorization_prod_pow_eq_self hd,
        ← Finsupp.prod_add_index' pow_zero pow_add, hK, add_tsub_cancel_of_le hdn]
  · rintro ⟨c, rfl⟩
    rw [factorization_mul hd (right_ne_zero_of_mul hn)]
    simp

Divisibility Criterion via Prime Factorization: $d \mid n \leftrightarrow d.\text{factorization} \leq n.\text{factorization}$ for $d, n \neq 0$

Informal description

For any nonzero natural numbers $d$ and $n$, the prime factorization of $d$ is pointwise less than or equal to the prime factorization of $n$ if and only if $d$ divides $n$. In other words, for every prime $p$, the exponent of $p$ in $d$ is less than or equal to its exponent in $n$ if and only if $d$ divides $n$.

Nat.factorization_prod theorem

 {α : Type*} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) :
  (S.prod g).factorization = S.sum fun x => (g x).factorization

Full source

/-- 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`. -/
theorem factorization_prod {α : Type*} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) :
    (S.prod g).factorization = S.sum fun x => (g x).factorization := by
  classical
    ext p
    refine Finset.induction_on' S ?_ ?_
    · simp
    · intro x T hxS hTS hxT IH
      have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
      simp [prod_insert hxT, sum_insert hxT, IH, factorization_mul (hS x hxS) hT]

Factorization of Product Equals Sum of Factorizations: $(\prod_{x \in S} g(x)).\text{factorization} = \sum_{x \in S} g(x).\text{factorization}$ for non-zero $g$ on $S$

Informal description

For any finite set $S$ of elements of type $\alpha$ and any function $g \colon \alpha \to \mathbb{N}$ that is non-zero on $S$, the multiplicity of a prime $p$ in the product $\prod_{x \in S} g(x)$ is equal to the sum of the multiplicities of $p$ in each $g(x)$ for $x \in S$. That is, for any prime $p$, $$(\prod_{x \in S} g(x)).\text{factorization}(p) = \sum_{x \in S} (g(x).\text{factorization}(p)).$$

Nat.factorization_pow theorem

(n k : ℕ) : factorization (n ^ k) = k • n.factorization

Full source

/-- For any `p`, the power of `p` in `n^k` is `k` times the power in `n` -/
@[simp]
theorem factorization_pow (n k : ℕ) : factorization (n ^ k) = k • n.factorization := by
  induction' k with k ih; · simp
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
    add_smul, one_smul, add_comm]

Prime Factorization of Powers: $\text{factorization}(n^k) = k \cdot \text{factorization}(n)$

Informal description

For any natural numbers $n$ and $k$, the prime factorization of $n^k$ is equal to $k$ times the prime factorization of $n$. That is, for every prime $p$, the multiplicity of $p$ in $n^k$ is $k$ times its multiplicity in $n$.

Nat.Prime.factorization theorem

{p : ℕ} (hp : Prime p) : p.factorization = single p 1

Full source

/-- The only prime factor of prime `p` is `p` itself, with multiplicity `1` -/
@[simp]
protected theorem Prime.factorization {p : ℕ} (hp : Prime p) : p.factorization = single p 1 := by
  ext q
  rw [← primeFactorsList_count_eq, primeFactorsList_prime hp, single_apply, count_singleton',
    if_congr eq_comm] <;> rfl

Prime Factorization of a Prime: $p.\text{factorization} = \text{single } p \, 1$

Informal description

For any prime natural number $p$, the prime factorization of $p$ is the finitely supported function that maps $p$ to $1$ and all other natural numbers to $0$. In other words, $p.\text{factorization} = \text{single } p \, 1$.

Nat.Prime.factorization_pow theorem

{p k : ℕ} (hp : Prime p) : (p ^ k).factorization = single p k

Full source

/-- For prime `p` the only prime factor of `p^k` is `p` with multiplicity `k` -/
theorem Prime.factorization_pow {p k : ℕ} (hp : Prime p) : (p ^ k).factorization = single p k := by
  simp [hp]

Prime Power Factorization: $(p^k).\text{factorization} = \text{single } p \, k$

Informal description

For any prime natural number $p$ and any natural number $k$, the prime factorization of $p^k$ is the finitely supported function that maps $p$ to $k$ and all other natural numbers to $0$. In other words, $(p^k).\text{factorization} = \text{single } p \, k$.

Nat.pow_succ_factorization_not_dvd theorem

{n p : ℕ} (hn : n ≠ 0) (hp : p.Prime) : ¬p ^ (n.factorization p + 1) ∣ n

Full source

theorem pow_succ_factorization_not_dvd {n p : ℕ} (hn : n ≠ 0) (hp : p.Prime) :
    ¬p ^ (n.factorization p + 1) ∣ n := by
  intro h
  rw [← factorization_le_iff_dvd (pow_pos hp.pos _).ne' hn] at h
  simpa [hp.factorization] using h p

Non-divisibility of $n$ by $p^{e+1}$ where $e$ is the exponent of $p$ in $n$'s factorization

Informal description

For any nonzero natural number $n$ and any prime number $p$, the prime power $p^{e+1}$ does not divide $n$, where $e$ is the exponent of $p$ in the prime factorization of $n$.

Nat.prod_pow_factorization_eq_self theorem

{f : ℕ →₀ ℕ} (hf : ∀ p : ℕ, p ∈ f.support → Prime p) : (f.prod (· ^ ·)).factorization = f

Full source

/-- Any Finsupp `f : ℕ →₀ ℕ` whose support is in the primes is equal to the factorization of
the product `∏ (a : ℕ) ∈ f.support, a ^ f a`. -/
theorem prod_pow_factorization_eq_self {f : ℕℕ →₀ ℕ} (hf : ∀ p : ℕ, p ∈ f.support → Prime p) :
    (f.prod (· ^ ·)).factorization = f := by
  have h : ∀ x : ℕ, x ∈ f.support → x ^ f x ≠ 0 := fun p hp =>
    pow_ne_zero _ (Prime.ne_zero (hf p hp))
  simp only [Finsupp.prod, factorization_prod h]
  conv =>
    rhs
    rw [(sum_single f).symm]
  exact sum_congr rfl fun p hp => Prime.factorization_pow (hf p hp)

Factorization of Prime Power Product Equals Original Function

Informal description

For any finitely supported function $f \colon \mathbb{N} \to \mathbb{N}$ such that every element $p$ in the support of $f$ is a prime number, the prime factorization of the product $\prod_{p \in \text{supp}(f)} p^{f(p)}$ is equal to $f$ itself. In other words, $$\left(\prod_{p \in \text{supp}(f)} p^{f(p)}\right).\text{factorization} = f.$$

Nat.factorizationEquiv definition

: ℕ+ ≃ {f : ℕ →₀ ℕ | ∀ p ∈ f.support, Prime p}

Full source

/-- The equiv between `ℕ+` and `ℕ →₀ ℕ` with support in the primes. -/
def factorizationEquiv : ℕ+ℕ+ ≃ { f : ℕ →₀ ℕ | ∀ p ∈ f.support, Prime p } where
  toFun := fun ⟨n, _⟩ => ⟨n.factorization, fun _ => prime_of_mem_primeFactors⟩
  invFun := fun ⟨f, hf⟩ =>
    ⟨f.prod _, prod_pow_pos_of_zero_not_mem_support fun H => not_prime_zero (hf 0 H)⟩
  left_inv := fun ⟨_, hx⟩ => Subtype.ext <| factorization_prod_pow_eq_self hx.ne.symm
  right_inv := fun ⟨_, hf⟩ => Subtype.ext <| prod_pow_factorization_eq_self hf

Equivalence between positive natural numbers and prime-supported finitely supported functions

Informal description

The equivalence between the type of positive natural numbers $\mathbb{N}^+$ and the type of finitely supported functions $f \colon \mathbb{N} \to \mathbb{N}$ where every element in the support of $f$ is a prime number. Explicitly: - The forward map sends a positive natural number $n$ to its prime factorization, represented as a finitely supported function that maps each prime factor $p$ of $n$ to its multiplicity in $n$. - The inverse map takes such a finitely supported function $f$ (with prime support) and returns the positive natural number obtained by taking the product of each prime $p$ raised to the power $f(p)$.

Nat.factorization_mul_apply_of_coprime theorem

{p a b : ℕ} (hab : Coprime a b) : (a * b).factorization p = a.factorization p + b.factorization p

Full source

/-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
theorem factorization_mul_apply_of_coprime {p a b : ℕ} (hab : Coprime a b) :
    (a * b).factorization p = a.factorization p + b.factorization p := by
  simp only [← primeFactorsList_count_eq,
    perm_iff_count.mp (perm_primeFactorsList_mul_of_coprime hab), count_append]

Multiplicativity of Prime Factorization for Coprime Numbers

Informal description

For any prime number $p$ and natural numbers $a$ and $b$ such that $a$ and $b$ are coprime, the multiplicity of $p$ in the prime factorization of $a \cdot b$ is equal to the sum of the multiplicities of $p$ in the prime factorizations of $a$ and $b$, i.e., \[ (a \cdot b).\text{factorization}(p) = a.\text{factorization}(p) + b.\text{factorization}(p). \]

Nat.factorization_mul_of_coprime theorem

{a b : ℕ} (hab : Coprime a b) : (a * b).factorization = a.factorization + b.factorization

Full source

/-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
theorem factorization_mul_of_coprime {a b : ℕ} (hab : Coprime a b) :
    (a * b).factorization = a.factorization + b.factorization := by
  ext q
  rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]

Prime Factorization is Additive for Coprime Numbers

Informal description

For any two coprime natural numbers $a$ and $b$, the prime factorization of their product $a \cdot b$ is equal to the sum of their individual prime factorizations. That is, \[ (a \cdot b).\text{factorization} = a.\text{factorization} + b.\text{factorization}, \] where the addition is performed pointwise on the multiplicities of each prime factor.

Nat.termOrdProj[_]_ definition

: Lean.ParserDescr✝

Full source

/-- We introduce the notations `ordProj[p] n` for the largest power of the prime `p` that
divides `n` and `ordCompl[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, `ordProj[2] n` is the even part of `n` and `ordCompl[2] n` is the odd part. -/
notation "ordProj[" p "] " n:arg => p ^ Nat.factorization n p

Largest power of a prime dividing a natural number

Informal description

The notation $\text{ordProj}[p]\, n$ denotes the largest power of the prime $p$ that divides $n$. Here, $p$ is a prime number and $n$ is a natural number. For example, $\text{ordProj}[2]\, n$ represents the even part of $n$.

Nat.termOrdCompl[_]_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc «termOrdProj[_]_»]
notation "ordCompl[" p "] " n:arg => n / ordProj[p] n

Complement of p-primary part of a natural number

Informal description

For natural numbers `n` and `p`, the notation `ordCompl[p] n` represents the complement of the `p`-primary part of `n`, defined as `n / ordProj[p] n` where `ordProj[p] n` is the largest power of `p` dividing `n`.

Nat.ordProj_dvd theorem

(n p : ℕ) : ordProj[p] n ∣ n

Full source

theorem ordProj_dvd (n p : ℕ) : ordProj[p] nordProj[p] n ∣ n := by
  if hp : p.Prime then ?_ else simp [hp]
  rw [← primeFactorsList_count_eq]
  apply dvd_of_primeFactorsList_subperm (pow_ne_zero _ hp.ne_zero)
  rw [hp.primeFactorsList_pow, List.subperm_ext_iff]
  intro q hq
  simp [List.eq_of_mem_replicate hq]

Divisibility of p-primary Part in Natural Numbers

Informal description

For any natural numbers $n$ and $p$, the $p$-primary part of $n$ (denoted $\text{ordProj}[p]\,n$) divides $n$. Here, $\text{ordProj}[p]\,n$ is defined as the largest power of $p$ that divides $n$.

Nat.factorizationLCMLeft definition

(a b : ℕ) : ℕ

Full source

/-- 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`. -/
def factorizationLCMLeft (a b : ℕ) : ℕ :=
  (Nat.lcm a b).factorization.prod fun p n ↦
    if b.factorization p ≤ a.factorization p then p ^ n else 1

Left factor of LCM based on prime factor multiplicities

Informal description

Given two natural numbers $ a $ and $ b $, the function `factorizationLCMLeft a b` computes the product $\prod_{p \mid \text{lcm}(a, b)} p^{k_p}$, where for each prime $ p $ dividing $\text{lcm}(a, b)$, the exponent $ k_p $ is defined as follows: - If the multiplicity of $ p $ in $ b $ is less than or equal to its multiplicity in $ a $, then $ k_p $ is the multiplicity of $ p $ in $\text{lcm}(a, b)$ (i.e., $ k_p = \max(v_p(a), v_p(b)) $). - Otherwise, $ k_p = 0 $. If either $ a $ or $ b $ is zero, the result is $ 1 $.

Nat.factorizationLCMRight definition

(a b : ℕ)

Full source

/-- 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`. -/
def factorizationLCMRight (a b : ℕ) :=
  (Nat.lcm a b).factorization.prod fun p n ↦
    if b.factorization p ≤ a.factorization p then 1 else p ^ n

Product of primes in LCM with strictly greater multiplicity in second argument

Informal description

Given two natural numbers $ a $ and $ b $, the function `factorizationLCMRight a b` computes the product $\prod_{p \mid \text{lcm}(a, b)} p^{k_p}$, where for each prime $ p $ dividing $\text{lcm}(a, b)$, the exponent $ k_p $ is defined as follows: - If the multiplicity of $ p $ in $ b $ is strictly greater than its multiplicity in $ a $, then $ k_p $ is the multiplicity of $ p $ in $\text{lcm}(a, b)$ (which equals its multiplicity in $ b $). - Otherwise, $ k_p = 0 $. Note that if either $ a $ or $ b $ is zero, the result is 1.