doc-next-gen

Mathlib.Data.Nat.Factorization.Basic

Module docstring

{"# Basic lemmas on prime factorizations ","### 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 divisibility ","### Factorization and coprimes ","### Lemmas about factorizations of particular functions "}

Nat.factorization_eq_zero_of_lt theorem
{n p : ℕ} (h : n < p) : n.factorization p = 0
Full source 
theorem factorization_eq_zero_of_lt {n p : ℕ} (h : n < p) : n.factorization p = 0 :=
  Finsupp.not_mem_support_iff.mp (mt le_of_mem_primeFactors (not_le_of_lt h))
Prime Factorization Vanishes for Primes Greater Than Number
Informal description
For any natural numbers $n$ and $p$ such that $n < p$, the multiplicity of $p$ in the prime factorization of $n$ is zero, i.e., $n.\text{factorization}(p) = 0$.
Nat.dvd_of_factorization_pos theorem
{n p : ℕ} (hn : n.factorization p ≠ 0) : p ∣ n
Full source 
theorem dvd_of_factorization_pos {n p : ℕ} (hn : n.factorization p ≠ 0) : p ∣ n :=
  dvd_of_mem_primeFactorsList <| mem_primeFactors_iff_mem_primeFactorsList.1 <| mem_support_iff.2 hn
Nonzero Factorization Implies Divisibility
Informal description
For any natural numbers $n$ and $p$, if the multiplicity of $p$ in the prime factorization of $n$ is nonzero (i.e., $n.\text{factorization}(p) \neq 0$), then $p$ divides $n$.
Nat.factorization_eq_zero_iff_remainder theorem
{p r : ℕ} (i : ℕ) (pp : p.Prime) (hr0 : r ≠ 0) : ¬p ∣ r ↔ (p * i + r).factorization p = 0
Full source 
theorem factorization_eq_zero_iff_remainder {p r : ℕ} (i : ℕ) (pp : p.Prime) (hr0 : r ≠ 0) :
    ¬p ∣ r¬p ∣ r ↔ (p * i + r).factorization p = 0 := by
  refine ⟨factorization_eq_zero_of_remainder i, fun h => ?_⟩
  rw [factorization_eq_zero_iff] at h
  contrapose! h
  refine ⟨pp, ?_, ?_⟩
  · rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]
  · contrapose! hr0
    exact (add_eq_zero.1 hr0).2
Prime Divisibility and Factorization Remainder Condition: $\neg(p \mid r) \leftrightarrow (p \cdot i + r).\text{factorization}(p) = 0$
Informal description
For any natural numbers $p$, $r$, and $i$, where $p$ is prime and $r \neq 0$, the following equivalence holds: $p$ does not divide $r$ if and only if 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_eq_zero_iff' theorem
(n : ℕ) : n.factorization = 0 ↔ n = 0 ∨ n = 1
Full source 
/-- The only numbers with empty prime factorization are `0` and `1` -/
theorem factorization_eq_zero_iff' (n : ℕ) : n.factorization = 0 ↔ n = 0 ∨ n = 1 := by
  rw [factorization_eq_primeFactorsList_multiset n]
  simp [factorization, AddEquiv.map_eq_zero_iff, Multiset.coe_eq_zero]
Zero Factorization Condition: $n.\text{factorization} = 0 \leftrightarrow n = 0 \lor n = 1$
Informal description
For any natural number $n$, the prime factorization of $n$ is the zero function (i.e., $n.\text{factorization} = 0$) if and only if $n$ is equal to $0$ or $1$.
Nat.prod_factorization_eq_prod_primeFactors theorem
{β : Type*} [CommMonoid β] (f : ℕ → ℕ → β) : n.factorization.prod f = ∏ p ∈ n.primeFactors, f p (n.factorization p)
Full source 
/-- A product over `n.factorization` can be written as a product over `n.primeFactors`; -/
lemma prod_factorization_eq_prod_primeFactors {β : Type*} [CommMonoid β] (f : ℕ → ℕ → β) :
    n.factorization.prod f = ∏ p ∈ n.primeFactors, f p (n.factorization p) := rfl
Product over Prime Factorization Equals Product over Prime Factors
Informal description
For any commutative monoid $\beta$ and any function $f : \mathbb{N} \to \mathbb{N} \to \beta$, the product of $f$ over the prime factorization of a natural number $n$ is equal to the product of $f$ over the prime factors of $n$, evaluated at their respective multiplicities. In other words, \[ \prod_{p \in \mathbb{N}} f(p, n.factorization(p)) = \prod_{p \in n.primeFactors} f(p, n.factorization(p)) \] where $n.factorization(p)$ denotes the multiplicity of the prime $p$ in the factorization of $n$, and $n.primeFactors$ is the set of prime factors of $n$.
Nat.prod_primeFactors_prod_factorization theorem
{β : Type*} [CommMonoid β] (f : ℕ → β) : ∏ p ∈ n.primeFactors, f p = n.factorization.prod (fun p _ ↦ f p)
Full source 
/-- A product over `n.primeFactors` can be written as a product over `n.factorization`; -/
lemma prod_primeFactors_prod_factorization {β : Type*} [CommMonoid β] (f : ℕ → β) :
    ∏ p ∈ n.primeFactors, f p = n.factorization.prod (fun p _ ↦ f p) := rfl
Product over Prime Factors Equals Product over Factorization Support
Informal description
Let $n$ be a natural number and $\beta$ be a commutative monoid. For any function $f : \mathbb{N} \to \beta$, the product of $f(p)$ over all prime factors $p$ of $n$ is equal to the product of $f(p)$ over all $p$ in the support of $n$'s prime factorization (i.e., where $n.factorization(p) \neq 0$).
Nat.Prime.factorization_self theorem
{p : ℕ} (hp : Prime p) : p.factorization p = 1
Full source 
/-- The multiplicity of prime `p` in `p` is `1` -/
@[simp]
theorem Prime.factorization_self {p : ℕ} (hp : Prime p) : p.factorization p = 1 := by simp [hp]
Prime Multiplicity in Its Own Factorization: $p.\text{factorization}(p) = 1$
Informal description
For any prime natural number $p$, the multiplicity of $p$ in its own prime factorization is $1$, i.e., $p.\text{factorization}(p) = 1$.
Nat.factorizationEquiv_inv_apply theorem
{f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.support, Prime p) : (factorizationEquiv.symm ⟨f, hf⟩).1 = f.prod (· ^ ·)
Full source 
theorem factorizationEquiv_inv_apply {f : ℕℕ →₀ ℕ} (hf : ∀ p ∈ f.support, Prime p) :
    (factorizationEquiv.symm ⟨f, hf⟩).1 = f.prod (· ^ ·) :=
  rfl
Inverse of Factorization Equivalence as Product of Prime Powers
Informal description
For any finitely supported function $f \colon \mathbb{N} \to \mathbb{N}$ such that every prime $p$ in the support of $f$ is a prime number, the positive natural number corresponding to $f$ under the inverse of the factorization equivalence is equal to the product of each prime $p$ raised to the power $f(p)$, i.e., \[ \text{factorizationEquiv.symm}(f) = \prod_{p} p^{f(p)}. \]
Nat.ordProj_of_not_prime theorem
(n p : ℕ) (hp : ¬p.Prime) : ordProj[p] n = 1
Full source 
@[simp]
theorem ordProj_of_not_prime (n p : ℕ) (hp : ¬p.Prime) : ordProj[p] n = 1 := by
  simp [factorization_eq_zero_of_non_prime n hp]
Order Projection of Non-Prime is One
Informal description
For any natural numbers $n$ and $p$, if $p$ is not a prime number, then the order projection of $n$ with respect to $p$ is equal to $1$, i.e., $\text{ordProj}[p]\, n = 1$.
Nat.ordCompl_of_not_prime theorem
(n p : ℕ) (hp : ¬p.Prime) : ordCompl[p] n = n
Full source 
@[simp]
theorem ordCompl_of_not_prime (n p : ℕ) (hp : ¬p.Prime) : ordCompl[p] n = n := by
  simp [factorization_eq_zero_of_non_prime n hp]
Order Complement of Non-Prime is Identity
Informal description
For any natural numbers $n$ and $p$, if $p$ is not a prime number, then the order complement of $n$ with respect to $p$ is equal to $n$ itself, i.e., $\text{ordCompl}[p]\, n = n$.
Nat.ordCompl_dvd theorem
(n p : ℕ) : ordCompl[p] n ∣ n
Full source 
theorem ordCompl_dvd (n p : ℕ) : ordCompl[p] nordCompl[p] n ∣ n :=
  div_dvd_of_dvd (ordProj_dvd n p)
Divisibility of Order Complement in Natural Numbers
Informal description
For any natural numbers $n$ and $p$, the order complement of $n$ with respect to $p$ (denoted $\text{ordCompl}[p]\,n$) divides $n$. Here, $\text{ordCompl}[p]\,n$ is defined as the part of $n$ that is coprime to $p$, i.e., $n$ divided by the largest power of $p$ that divides $n$.
Nat.ordProj_pos theorem
(n p : ℕ) : 0 < ordProj[p] n
Full source 
theorem ordProj_pos (n p : ℕ) : 0 < ordProj[p] n := by
  if pp : p.Prime then simp [pow_pos pp.pos] else simp [pp]
Positivity of $p$-adic valuation
Informal description
For any natural numbers $n$ and $p$, the $p$-adic valuation of $n$ (denoted $\text{ordProj}[p]\,n$) is positive, i.e., $\text{ordProj}[p]\,n > 0$.
Nat.ordProj_le theorem
{n : ℕ} (p : ℕ) (hn : n ≠ 0) : ordProj[p] n ≤ n
Full source 
theorem ordProj_le {n : ℕ} (p : ℕ) (hn : n ≠ 0) : ordProj[p] n ≤ n :=
  le_of_dvd hn.bot_lt (Nat.ordProj_dvd n p)
Upper Bound on $p$-Primary Part of a Natural Number
Informal description
For any natural numbers $n$ and $p$, if $n$ is nonzero, then the $p$-primary part of $n$ (denoted $\text{ordProj}[p]\,n$) is less than or equal to $n$. Here, $\text{ordProj}[p]\,n$ is defined as the largest power of $p$ that divides $n$.
Nat.ordCompl_pos theorem
{n : ℕ} (p : ℕ) (hn : n ≠ 0) : 0 < ordCompl[p] n
Full source 
theorem ordCompl_pos {n : ℕ} (p : ℕ) (hn : n ≠ 0) : 0 < ordCompl[p] n := by
  if pp : p.Prime then
    exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)
  else
    simpa [Nat.factorization_eq_zero_of_non_prime n pp] using hn.bot_lt
Positivity of $p$-Order Complement for Nonzero Natural Numbers
Informal description
For any natural numbers $n$ and $p$, if $n$ is nonzero, then the $p$-order complement of $n$ (denoted $\text{ordCompl}[p]\,n$) is positive, i.e., $\text{ordCompl}[p]\,n > 0$. Here, the $p$-order complement of $n$ is the largest divisor of $n$ that is not divisible by $p$.
Nat.ordCompl_le theorem
(n p : ℕ) : ordCompl[p] n ≤ n
Full source 
theorem ordCompl_le (n p : ℕ) : ordCompl[p] n ≤ n :=
  Nat.div_le_self _ _
Upper Bound on $p$-Order Complement of a Natural Number
Informal description
For any natural numbers $n$ and $p$, the $p$-order complement of $n$ is less than or equal to $n$. Here, the $p$-order complement of $n$ is the largest divisor of $n$ that is not divisible by $p$.
Nat.ordProj_mul_ordCompl_eq_self theorem
(n p : ℕ) : ordProj[p] n * ordCompl[p] n = n
Full source 
theorem ordProj_mul_ordCompl_eq_self (n p : ℕ) : ordProj[p] n * ordCompl[p] n = n :=
  Nat.mul_div_cancel' (ordProj_dvd n p)
Decomposition of Natural Number into $p$-Primary Part and $p$-Order Complement: $\text{ordProj}[p]\,n \cdot \text{ordCompl}[p]\,n = n$
Informal description
For any natural numbers $n$ and $p$, the product of the $p$-primary part of $n$ (denoted $\text{ordProj}[p]\,n$) and the $p$-order complement of $n$ (denoted $\text{ordCompl}[p]\,n$) equals $n$. Here, $\text{ordProj}[p]\,n$ is the largest power of $p$ dividing $n$, and $\text{ordCompl}[p]\,n$ is the largest divisor of $n$ not divisible by $p$.
Nat.ordProj_mul theorem
{a b : ℕ} (p : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : ordProj[p] (a * b) = ordProj[p] a * ordProj[p] b
Full source 
theorem ordProj_mul {a b : ℕ} (p : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :
    ordProj[p] (a * b) = ordProj[p] a * ordProj[p] b := by
  simp [factorization_mul ha hb, pow_add]
Multiplicativity of $p$-Order Projection: $\text{ordProj}_p(a \cdot b) = \text{ordProj}_p(a) \cdot \text{ordProj}_p(b)$ for $a, b \neq 0$
Informal description
For any nonzero natural numbers $a$ and $b$, and for any prime $p$, the $p$-order projection of the product $a \cdot b$ is equal to the product of the $p$-order projections of $a$ and $b$. Here, the $p$-order projection of a number $n$ is the largest power of $p$ dividing $n$.
Nat.ordCompl_mul theorem
(a b p : ℕ) : ordCompl[p] (a * b) = ordCompl[p] a * ordCompl[p] b
Full source 
theorem ordCompl_mul (a b p : ℕ) : ordCompl[p] (a * b) = ordCompl[p] a * ordCompl[p] b := by
  if ha : a = 0 then simp [ha] else
  if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]
Multiplicativity of $p$-Order Complement: $\text{ordCompl}_p(a \cdot b) = \text{ordCompl}_p(a) \cdot \text{ordCompl}_p(b)$
Informal description
For any natural numbers $a$, $b$, and $p$, the $p$-order complement of the product $a \cdot b$ is equal to the product of the $p$-order complements of $a$ and $b$. Here, the $p$-order complement of a number $n$ is the largest divisor of $n$ that is coprime to $p$.
Nat.factorization_lt theorem
{n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p < n
Full source 
/-- A crude upper bound on `n.factorization p` -/
theorem factorization_lt {n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p < n := by
  by_cases pp : p.Prime
  · exact (Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <|
      Nat.lt_pow_self pp.one_lt
  · simpa only [factorization_eq_zero_of_non_prime n pp] using hn.bot_lt
Upper Bound on Prime Multiplicity in Factorization: $n.\text{factorization}(p) < n$ for $n \neq 0$
Informal description
For any nonzero natural number $n$ and any prime number $p$, the multiplicity of $p$ in the prime factorization of $n$ is strictly less than $n$, i.e., $n.\text{factorization}(p) < n$.
Nat.factorization_le_of_le_pow theorem
{n p b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b
Full source 
/-- An upper bound on `n.factorization p` -/
theorem factorization_le_of_le_pow {n p b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b := by
  if hn : n = 0 then simp [hn] else
  if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_non_prime n pp]
Upper Bound on Prime Multiplicity: $n \leq p^b \Rightarrow n.\text{factorization}(p) \leq b$
Informal description
For any natural numbers $n$, $p$, and $b$ such that $n \leq p^b$, the multiplicity of $p$ in the prime factorization of $n$ is at most $b$, i.e., $n.\text{factorization}(p) \leq b$.
Nat.factorization_prime_le_iff_dvd theorem
{d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : (∀ p : ℕ, p.Prime → d.factorization p ≤ n.factorization p) ↔ d ∣ n
Full source 
theorem factorization_prime_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :
    (∀ p : ℕ, p.Prime → d.factorization p ≤ n.factorization p) ↔ d ∣ n := by
  rw [← factorization_le_iff_dvd hd hn]
  refine ⟨fun h p => (em p.Prime).elim (h p) fun hp => ?_, fun h p _ => h p⟩
  simp_rw [factorization_eq_zero_of_non_prime _ hp]
  rfl
Divisibility Criterion via Prime Factorization: $d \mid n \leftrightarrow \forall p \text{ prime}, d.\text{factorization}(p) \leq n.\text{factorization}(p)$ for $d, n \neq 0$
Informal description
For any nonzero natural numbers $d$ and $n$, the following are equivalent: 1. For every prime number $p$, the multiplicity of $p$ in the prime factorization of $d$ is less than or equal to its multiplicity in the prime factorization of $n$. 2. $d$ divides $n$. In other words, $d \mid n$ if and only if for all primes $p$, $d.\text{factorization}(p) \leq n.\text{factorization}(p)$.
Nat.factorization_le_factorization_mul_left theorem
{a b : ℕ} (hb : b ≠ 0) : a.factorization ≤ (a * b).factorization
Full source 
theorem factorization_le_factorization_mul_left {a b : ℕ} (hb : b ≠ 0) :
    a.factorization ≤ (a * b).factorization := by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp
  rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]
  exact Dvd.intro b rfl
Monotonicity of Prime Factorization under Left Multiplication: $a.\text{factorization} \leq (a \times b).\text{factorization}$ for $b \neq 0$
Informal description
For any natural numbers $a$ and $b$ with $b \neq 0$, the prime factorization of $a$ is pointwise less than or equal to the prime factorization of $a \times b$, i.e., for every prime $p$, the multiplicity of $p$ in $a$ is at most its multiplicity in $a \times b$.
Nat.factorization_le_factorization_mul_right theorem
{a b : ℕ} (ha : a ≠ 0) : b.factorization ≤ (a * b).factorization
Full source 
theorem factorization_le_factorization_mul_right {a b : ℕ} (ha : a ≠ 0) :
    b.factorization ≤ (a * b).factorization := by
  rw [mul_comm]
  apply factorization_le_factorization_mul_left ha
Monotonicity of Prime Factorization under Right Multiplication: $b.\text{factorization} \leq (a \times b).\text{factorization}$ for $a \neq 0$
Informal description
For any natural numbers $a$ and $b$ with $a \neq 0$, the prime factorization of $b$ is pointwise less than or equal to the prime factorization of $a \times b$, i.e., for every prime $p$, the multiplicity of $p$ in $b$ is at most its multiplicity in $a \times b$.
Nat.Prime.pow_dvd_iff_le_factorization theorem
{p k n : ℕ} (pp : Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ k ≤ n.factorization p
Full source 
theorem Prime.pow_dvd_iff_le_factorization {p k n : ℕ} (pp : Prime p) (hn : n ≠ 0) :
    p ^ k ∣ np ^ k ∣ n ↔ k ≤ n.factorization p := by
  rw [← factorization_le_iff_dvd (pow_pos pp.pos k).ne' hn, pp.factorization_pow, single_le_iff]
Prime Power Divisibility Criterion: $p^k \mid n \leftrightarrow k \leq n.\text{factorization}(p)$ for $n \neq 0$
Informal description
For any prime natural number $p$, any natural number $k$, and any nonzero natural number $n$, the prime power $p^k$ divides $n$ if and only if the exponent $k$ is less than or equal to the multiplicity of $p$ in the prime factorization of $n$.
Nat.Prime.pow_dvd_iff_dvd_ordProj theorem
{p k n : ℕ} (pp : Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ p ^ k ∣ ordProj[p] n
Full source 
theorem Prime.pow_dvd_iff_dvd_ordProj {p k n : ℕ} (pp : Prime p) (hn : n ≠ 0) :
    p ^ k ∣ np ^ k ∣ n ↔ p ^ k ∣ ordProj[p] n := by
  rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]
Prime Power Divisibility via $p$-part: $p^k \mid n \leftrightarrow p^k \mid \text{ordProj}[p]\,n$ for $n \neq 0$
Informal description
For any prime natural number $p$, any natural number $k$, and any nonzero natural number $n$, the prime power $p^k$ divides $n$ if and only if $p^k$ divides the $p$-part of $n$ (denoted by $\text{ordProj}[p]\,n$).
Nat.Prime.dvd_iff_one_le_factorization theorem
{p n : ℕ} (pp : Prime p) (hn : n ≠ 0) : p ∣ n ↔ 1 ≤ n.factorization p
Full source 
theorem Prime.dvd_iff_one_le_factorization {p n : ℕ} (pp : Prime p) (hn : n ≠ 0) :
    p ∣ np ∣ n ↔ 1 ≤ n.factorization p :=
  Iff.trans (by simp) (pp.pow_dvd_iff_le_factorization hn)
Prime Divisibility Criterion: $p \mid n \leftrightarrow 1 \leq n.\text{factorization}(p)$ for $n \neq 0$
Informal description
For any prime natural number $p$ and any nonzero natural number $n$, $p$ divides $n$ if and only if the multiplicity of $p$ in the prime factorization of $n$ is at least 1, i.e., $p \mid n \leftrightarrow 1 \leq n.\text{factorization}(p)$.
Nat.exists_factorization_lt_of_lt theorem
{a b : ℕ} (ha : a ≠ 0) (hab : a < b) : ∃ p : ℕ, a.factorization p < b.factorization p
Full source 
theorem exists_factorization_lt_of_lt {a b : ℕ} (ha : a ≠ 0) (hab : a < b) :
    ∃ p : ℕ, a.factorization p < b.factorization p := by
  have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
  contrapose! hab
  rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab
  exact le_of_dvd ha.bot_lt hab
Existence of Prime with Strictly Greater Multiplicity in Larger Number
Informal description
For any nonzero natural numbers $a$ and $b$ such that $a < b$, there exists a prime $p$ such that the multiplicity of $p$ in the prime factorization of $a$ is strictly less than its multiplicity in the prime factorization of $b$.
Nat.factorization_div theorem
{d n : ℕ} (h : d ∣ n) : (n / d).factorization = n.factorization - d.factorization
Full source 
@[simp]
theorem factorization_div {d n : ℕ} (h : d ∣ n) :
    (n / d).factorization = n.factorization - d.factorization := by
  rcases eq_or_ne d 0 with (rfl | hd); · simp [zero_dvd_iff.mp h]
  rcases eq_or_ne n 0 with (rfl | hn); · simp [tsub_eq_zero_of_le]
  apply add_left_injective d.factorization
  simp only
  rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
    Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
    Nat.div_mul_cancel h]
Factorization of Quotient by Divisor: $(n/d).\text{factorization} = n.\text{factorization} - d.\text{factorization}$ for $d \mid n$
Informal description
For any natural numbers $d$ and $n$ such that $d$ divides $n$, the prime factorization of the quotient $n/d$ is equal to the difference between the prime factorization of $n$ and the prime factorization of $d$. That is, for every prime $p$, the multiplicity of $p$ in $n/d$ equals its multiplicity in $n$ minus its multiplicity in $d$.
Nat.dvd_ordProj_of_dvd theorem
{n p : ℕ} (hn : n ≠ 0) (pp : p.Prime) (h : p ∣ n) : p ∣ ordProj[p] n
Full source 
theorem dvd_ordProj_of_dvd {n p : ℕ} (hn : n ≠ 0) (pp : p.Prime) (h : p ∣ n) : p ∣ ordProj[p] n :=
  dvd_pow_self p (Prime.factorization_pos_of_dvd pp hn h).ne'
Divisibility of Prime Part by Prime Divisor
Informal description
For any nonzero natural number $n$ and any prime number $p$ dividing $n$, the prime $p$ also divides the $p$-part of $n$ (denoted $\text{ordProj}[p]\,n$).
Nat.not_dvd_ordCompl theorem
{n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : ¬p ∣ ordCompl[p] n
Full source 
theorem not_dvd_ordCompl {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : ¬p ∣ ordCompl[p] n := by
  rw [Nat.Prime.dvd_iff_one_le_factorization hp (ordCompl_pos p hn).ne']
  rw [Nat.factorization_div (Nat.ordProj_dvd n p)]
  simp [hp.factorization]
Non-divisibility of $p$-order complement by $p$ for nonzero $n$
Informal description
For any prime number $p$ and any nonzero natural number $n$, the $p$-order complement of $n$ (denoted $\text{ordCompl}[p]\,n$) is not divisible by $p$. Here, the $p$-order complement of $n$ is the largest divisor of $n$ that is coprime to $p$.
Nat.coprime_ordCompl theorem
{n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : Coprime p (ordCompl[p] n)
Full source 
theorem coprime_ordCompl {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : Coprime p (ordCompl[p] n) :=
  (or_iff_left (not_dvd_ordCompl hp hn)).mp <| coprime_or_dvd_of_prime hp _
Coprimality of Prime and Order Complement: $\text{Coprime}(p, \text{ordCompl}[p]\,n)$ for $n \neq 0$
Informal description
For any prime number $p$ and any nonzero natural number $n$, the $p$-order complement of $n$ (denoted $\text{ordCompl}[p]\,n$) is coprime to $p$. Here, the $p$-order complement of $n$ is the largest divisor of $n$ that is coprime to $p$.
Nat.factorization_ordCompl theorem
(n p : ℕ) : (ordCompl[p] n).factorization = n.factorization.erase p
Full source 
theorem factorization_ordCompl (n p : ℕ) :
    (ordCompl[p] n).factorization = n.factorization.erase p := by
  if hn : n = 0 then simp [hn] else
  if pp : p.Prime then ?_ else
    simp [pp]
  ext q
  rcases eq_or_ne q p with (rfl | hqp)
  · simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]
    simp
  · rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]
    simp [pp.factorization, hqp.symm]
Factorization of $p$-order complement: $(\text{ordCompl}[p]\,n).\text{factorization} = n.\text{factorization} \setminus p$
Informal description
For any natural numbers $n$ and $p$, the prime factorization of the $p$-order complement of $n$ (denoted $\text{ordCompl}[p]\,n$) is equal to the prime factorization of $n$ with the prime $p$ erased. That is, for every prime $q \neq p$, the multiplicity of $q$ in $\text{ordCompl}[p]\,n$ equals its multiplicity in $n$, and the multiplicity of $p$ in $\text{ordCompl}[p]\,n$ is zero.
Nat.dvd_ordCompl_of_dvd_not_dvd theorem
{p d n : ℕ} (hdn : d ∣ n) (hpd : ¬p ∣ d) : d ∣ ordCompl[p] n
Full source 
theorem dvd_ordCompl_of_dvd_not_dvd {p d n : ℕ} (hdn : d ∣ n) (hpd : ¬p ∣ d) :
    d ∣ ordCompl[p] n := by
  if hn0 : n = 0 then simp [hn0] else
  if hd0 : d = 0 then simp [hd0] at hpd else
  rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
  intro q
  if hqp : q = p then
    simp [factorization_eq_zero_iff, hqp, hpd]
  else
    simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]
Divisibility of Order Complement: $d \mid \text{ordCompl}[p]\,n$ when $d \mid n$ and $p \nmid d$
Informal description
For any natural numbers $p$, $d$, and $n$, if $d$ divides $n$ and $p$ does not divide $d$, then $d$ divides the $p$-order complement of $n$ (denoted $\text{ordCompl}[p]\,n$), which is the largest divisor of $n$ not divisible by $p$.
Nat.exists_eq_pow_mul_and_not_dvd theorem
{n : ℕ} (hn : n ≠ 0) (p : ℕ) (hp : p ≠ 1) : ∃ e n' : ℕ, ¬p ∣ n' ∧ n = p ^ e * n'
Full source 
/-- 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 exists_eq_pow_mul_and_not_dvd {n : ℕ} (hn : n ≠ 0) (p : ℕ) (hp : p ≠ 1) :
    ∃ e n' : ℕ, ¬p ∣ n' ∧ n = p ^ e * n' :=
  let ⟨a', h₁, h₂⟩ :=
    (Nat.finiteMultiplicity_iff.mpr ⟨hp, Nat.pos_of_ne_zero hn⟩).exists_eq_pow_mul_and_not_dvd
  ⟨_, a', h₂, h₁⟩
Existence of Prime Power Factorization for Nonzero Natural Numbers
Informal description
For any nonzero natural number $n$ and any natural number $p \neq 1$, there exist natural numbers $e$ and $n'$ such that $n'$ is not divisible by $p$ and $n = p^e \cdot n'$.
Nat.exists_eq_two_pow_mul_odd theorem
{n : ℕ} (hn : n ≠ 0) : ∃ k m : ℕ, Odd m ∧ n = 2 ^ k * m
Full source 
/-- Any nonzero natural number is the product of an odd part `m` and a power of
two `2 ^ k`. -/
theorem exists_eq_two_pow_mul_odd {n : ℕ} (hn : n ≠ 0) :
    ∃ k m : ℕ, Odd m ∧ n = 2 ^ k * m :=
  let ⟨k, m, hm, hn⟩ := exists_eq_pow_mul_and_not_dvd hn 2 (succ_ne_self 1)
  ⟨k, m, not_even_iff_odd.1 (mt Even.two_dvd hm), hn⟩
Decomposition of Natural Number into Power of Two and Odd Part
Informal description
For any nonzero natural number $n$, there exist natural numbers $k$ and $m$ such that $m$ is odd and $n = 2^k \cdot m$.
Nat.dvd_iff_div_factorization_eq_tsub theorem
{d n : ℕ} (hd : d ≠ 0) (hdn : d ≤ n) : d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization
Full source 
theorem dvd_iff_div_factorization_eq_tsub {d n : ℕ} (hd : d ≠ 0) (hdn : d ≤ n) :
    d ∣ nd ∣ n ↔ (n / d).factorization = n.factorization - d.factorization := by
  refine ⟨factorization_div, ?_⟩
  rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n); · simp
  have h1 : n / d ≠ 0 := by simp [*]
  intro h
  rw [dvd_iff_le_div_mul n d]
  by_contra h2
  obtain ⟨p, hp⟩ := exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2)
  rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
   lt_self_iff_false] at hp
Divisibility Criterion via Prime Factorization Differences
Informal description
For any nonzero natural numbers $d$ and $n$ with $d \leq n$, the number $d$ divides $n$ if and only if the prime factorization of $n/d$ equals the difference between the prime factorizations of $n$ and $d$. That is, for every prime $p$, the multiplicity of $p$ in $n/d$ equals its multiplicity in $n$ minus its multiplicity in $d$.
Nat.ordProj_dvd_ordProj_of_dvd theorem
{a b : ℕ} (hb0 : b ≠ 0) (hab : a ∣ b) (p : ℕ) : ordProj[p] a ∣ ordProj[p] b
Full source 
theorem ordProj_dvd_ordProj_of_dvd {a b : ℕ} (hb0 : b ≠ 0) (hab : a ∣ b) (p : ℕ) :
    ordProj[p] aordProj[p] a ∣ ordProj[p] b := by
  rcases em' p.Prime with (pp | pp); · simp [pp]
  rcases eq_or_ne a 0 with (rfl | ha0); · simp
  rw [pow_dvd_pow_iff_le_right pp.one_lt]
  exact (factorization_le_iff_dvd ha0 hb0).2 hab p
Divisibility of $p$-parts: $a \mid b$ implies $\text{ordProj}_p(a) \mid \text{ordProj}_p(b)$ for $b \neq 0$
Informal description
For any nonzero natural numbers $a$ and $b$ such that $a$ divides $b$, and for any prime $p$, the $p$-part of $a$ divides the $p$-part of $b$. Here, the $p$-part of a number is the largest power of $p$ dividing that number.
Nat.ordProj_dvd_ordProj_iff_dvd theorem
{a b : ℕ} (ha0 : a ≠ 0) (hb0 : b ≠ 0) : (∀ p : ℕ, ordProj[p] a ∣ ordProj[p] b) ↔ a ∣ b
Full source 
theorem ordProj_dvd_ordProj_iff_dvd {a b : ℕ} (ha0 : a ≠ 0) (hb0 : b ≠ 0) :
    (∀ p : ℕ, ordProj[p] a ∣ ordProj[p] b) ↔ a ∣ b := by
  refine ⟨fun h => ?_, fun hab p => ordProj_dvd_ordProj_of_dvd hb0 hab p⟩
  rw [← factorization_le_iff_dvd ha0 hb0]
  intro q
  rcases le_or_lt q 1 with (hq_le | hq1)
  · interval_cases q <;> simp
  exact (pow_dvd_pow_iff_le_right hq1).1 (h q)
Divisibility Criterion via $p$-parts: $a \mid b \leftrightarrow \forall p, \text{ordProj}_p(a) \mid \text{ordProj}_p(b)$ for $a, b \neq 0$
Informal description
For any nonzero natural numbers $a$ and $b$, the following are equivalent: 1. For every prime $p$, the $p$-part of $a$ divides the $p$-part of $b$. 2. $a$ divides $b$. Here, the $p$-part of a number is the largest power of $p$ dividing that number.
Nat.ordCompl_dvd_ordCompl_of_dvd theorem
{a b : ℕ} (hab : a ∣ b) (p : ℕ) : ordCompl[p] a ∣ ordCompl[p] b
Full source 
theorem ordCompl_dvd_ordCompl_of_dvd {a b : ℕ} (hab : a ∣ b) (p : ℕ) :
    ordCompl[p] aordCompl[p] a ∣ ordCompl[p] b := by
  rcases em' p.Prime with (pp | pp)
  · simp [pp, hab]
  rcases eq_or_ne b 0 with (rfl | hb0)
  · simp
  rcases eq_or_ne a 0 with (rfl | ha0)
  · cases hb0 (zero_dvd_iff.1 hab)
  have ha := (Nat.div_pos (ordProj_le p ha0) (ordProj_pos a p)).ne'
  have hb := (Nat.div_pos (ordProj_le p hb0) (ordProj_pos b p)).ne'
  rw [← factorization_le_iff_dvd ha hb, factorization_ordCompl a p, factorization_ordCompl b p]
  intro q
  rcases eq_or_ne q p with (rfl | hqp)
  · simp
  simp_rw [erase_ne hqp]
  exact (factorization_le_iff_dvd ha0 hb0).2 hab q
Divisibility of $p$-Order Complements: $a \mid b$ implies $\text{ordCompl}_p(a) \mid \text{ordCompl}_p(b)$
Informal description
For any natural numbers $a$ and $b$ such that $a$ divides $b$, and for any prime $p$, the $p$-order complement of $a$ divides the $p$-order complement of $b$. Here, the $p$-order complement of a number is the largest divisor of that number not divisible by $p$.
Nat.ordCompl_dvd_ordCompl_iff_dvd theorem
(a b : ℕ) : (∀ p : ℕ, ordCompl[p] a ∣ ordCompl[p] b) ↔ a ∣ b
Full source 
theorem ordCompl_dvd_ordCompl_iff_dvd (a b : ℕ) :
    (∀ p : ℕ, ordCompl[p] a ∣ ordCompl[p] b) ↔ a ∣ b := by
  refine ⟨fun h => ?_, fun hab p => ordCompl_dvd_ordCompl_of_dvd hab p⟩
  rcases eq_or_ne b 0 with (rfl | hb0)
  · simp
  if pa : a.Prime then ?_ else simpa [pa] using h a
  if pb : b.Prime then ?_ else simpa [pb] using h b
  rw [prime_dvd_prime_iff_eq pa pb]
  by_contra hab
  apply pa.ne_one
  rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_left hb0.bot_lt, mul_one]
  simpa [Prime.factorization_self pb, Prime.factorization pa, hab] using h b
Divisibility Criterion via $p$-Order Complements: $a \mid b \leftrightarrow \forall p, \text{ordCompl}_p(a) \mid \text{ordCompl}_p(b)$
Informal description
For any natural numbers $a$ and $b$, the following are equivalent: 1. For every prime $p$, the $p$-order complement of $a$ divides the $p$-order complement of $b$. 2. $a$ divides $b$. Here, the $p$-order complement of a number is the largest divisor of that number not divisible by $p$.
Nat.dvd_iff_prime_pow_dvd_dvd theorem
(n d : ℕ) : d ∣ n ↔ ∀ p k : ℕ, Prime p → p ^ k ∣ d → p ^ k ∣ n
Full source 
theorem dvd_iff_prime_pow_dvd_dvd (n d : ℕ) :
    d ∣ nd ∣ n ↔ ∀ p k : ℕ, Prime p → p ^ k ∣ d → p ^ k ∣ n := by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  rcases eq_or_ne d 0 with (rfl | hd)
  · simp only [zero_dvd_iff, hn, false_iff, not_forall]
    exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow_self).not_le⟩
  refine ⟨fun h p k _ hpkd => dvd_trans hpkd h, ?_⟩
  rw [← factorization_prime_le_iff_dvd hd hn]
  intro h p pp
  simp_rw [← pp.pow_dvd_iff_le_factorization hn]
  exact h p _ pp (ordProj_dvd _ _)
Divisibility Criterion via Prime Powers: $d \mid n \leftrightarrow \forall p^k \mid d, p^k \mid n$
Informal description
For any natural numbers $d$ and $n$, the following are equivalent: 1. $d$ divides $n$. 2. For every prime number $p$ and every natural number $k$, if $p^k$ divides $d$, then $p^k$ also divides $n$. In other words, $d \mid n$ if and only if every prime power dividing $d$ also divides $n$.
Nat.prod_primeFactors_dvd theorem
(n : ℕ) : ∏ p ∈ n.primeFactors, p ∣ n
Full source 
theorem prod_primeFactors_dvd (n : ℕ) : ∏ p ∈ n.primeFactors, p∏ p ∈ n.primeFactors, p ∣ n := by
  by_cases hn : n = 0
  · subst hn
    simp
  · simpa [prod_primeFactorsList hn] using (n.primeFactorsList : Multiset ℕ).toFinset_prod_dvd_prod
Product of Prime Factors Divides Original Number
Informal description
For any natural number $n$, the product of all prime factors of $n$ divides $n$. In other words, $\prod_{p \in \text{primeFactors}(n)} p$ divides $n$.
Nat.factorization_gcd theorem
{a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) : (gcd a b).factorization = a.factorization ⊓ b.factorization
Full source 
theorem factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) :
    (gcd a b).factorization = a.factorization ⊓ b.factorization := by
  let dfac := a.factorization ⊓ b.factorization
  let d := dfac.prod (· ^ ·)
  have dfac_prime : ∀ p : ℕ, p ∈ dfac.support → Prime p := by
    intro p hp
    have : p ∈ a.primeFactorsListp ∈ a.primeFactorsList ∧ p ∈ b.primeFactorsList := by simpa [dfac] using hp
    exact prime_of_mem_primeFactorsList this.1
  have h1 : d.factorization = dfac := prod_pow_factorization_eq_self dfac_prime
  have hd_pos : d ≠ 0 := (factorizationEquiv.invFun ⟨dfac, dfac_prime⟩).2.ne'
  suffices d = gcd a b by rwa [← this]
  apply gcd_greatest
  · rw [← factorization_le_iff_dvd hd_pos ha_pos, h1]
    exact inf_le_left
  · rw [← factorization_le_iff_dvd hd_pos hb_pos, h1]
    exact inf_le_right
  · intro e hea heb
    rcases Decidable.eq_or_ne e 0 with (rfl | he_pos)
    · simp only [zero_dvd_iff] at hea
      contradiction
    have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea
    have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb
    simp [dfac, ← factorization_le_iff_dvd he_pos hd_pos, h1, hea', heb']
Prime Factorization of GCD Equals Pointwise Minimum of Factorizations
Informal description
For any nonzero natural numbers $a$ and $b$, the prime factorization of their greatest common divisor $\gcd(a, b)$ is equal to the pointwise infimum of their prime factorizations. That is, for every prime $p$, the exponent of $p$ in $\gcd(a, b)$ is the minimum of its exponents in $a$ and $b$: $$(\gcd(a, b)).\text{factorization} = a.\text{factorization} \sqcap b.\text{factorization}.$$
Nat.factorization_lcm theorem
{a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a.lcm b).factorization = a.factorization ⊔ b.factorization
Full source 
theorem factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a.lcm b).factorization = a.factorization ⊔ b.factorization := by
  rw [← add_right_inj (a.gcd b).factorization, ←
    factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm,
    factorization_gcd ha hb, factorization_mul ha hb]
  ext1
  exact (min_add_max _ _).symm
Prime Factorization of LCM Equals Pointwise Maximum of Factorizations
Informal description
For any nonzero natural numbers $a$ and $b$, the prime factorization of their least common multiple $\text{lcm}(a, b)$ is equal to the pointwise supremum of their prime factorizations. That is, for every prime $p$, the exponent of $p$ in $\text{lcm}(a, b)$ is the maximum of its exponents in $a$ and $b$: $$\text{lcm}(a, b).\text{factorization} = a.\text{factorization} \sqcup b.\text{factorization}.$$
Nat.factorizationLCMLeft_zero_left theorem
: factorizationLCMLeft 0 b = 1
Full source 
@[simp]
lemma factorizationLCMLeft_zero_left : factorizationLCMLeft 0 b = 1 := by
  simp [factorizationLCMLeft]
Factorization LCM Left at Zero: $\text{factorizationLCMLeft}(0, b) = 1$
Informal description
For any natural number $b$, the left factor of the least common multiple (LCM) based on prime factor multiplicities evaluated at $a = 0$ is equal to $1$, i.e., $\text{factorizationLCMLeft}(0, b) = 1$.
Nat.factorizationLCMLeft_zero_right theorem
: factorizationLCMLeft a 0 = 1
Full source 
@[simp]
lemma factorizationLCMLeft_zero_right : factorizationLCMLeft a 0 = 1 := by
  simp [factorizationLCMLeft]
Factorization LCM Left with Zero Right Argument Yields One
Informal description
For any natural number $a$, the left factor of the least common multiple of $a$ and $0$ is $1$, i.e., $\text{factorizationLCMLeft}(a, 0) = 1$.
Nat.factorizationLCRight_zero_left theorem
: factorizationLCMRight 0 b = 1
Full source 
@[simp]
lemma factorizationLCRight_zero_left : factorizationLCMRight 0 b = 1 := by
  simp [factorizationLCMRight]
Factorization LCM Right at Zero Left Argument is One
Informal description
For any natural number $b$, the function `factorizationLCMRight` evaluated at $(0, b)$ equals $1$.
Nat.factorizationLCMRight_zero_right theorem
: factorizationLCMRight a 0 = 1
Full source 
@[simp]
lemma factorizationLCMRight_zero_right : factorizationLCMRight a 0 = 1 := by
  simp [factorizationLCMRight]
Factorization LCM Right Zero Right: $\text{factorizationLCMRight}(a, 0) = 1$
Informal description
For any natural number $a$, the product of primes in the LCM of $a$ and $0$ with strictly greater multiplicity in $0$ is equal to $1$.
Nat.factorizationLCMLeft_pos theorem
: 0 < factorizationLCMLeft a b
Full source 
lemma factorizationLCMLeft_pos :
    0 < factorizationLCMLeft a b := by
  apply Nat.pos_of_ne_zero
  rw [factorizationLCMLeft, Finsupp.prod_ne_zero_iff]
  intro p _ H
  by_cases h : b.factorization p ≤ a.factorization p
  · simp only [h, reduceIte, pow_eq_zero_iff', ne_eq] at H
    simpa [H.1] using H.2
  · simp only [h, reduceIte, one_ne_zero] at H
Positivity of Left LCM Factor in Prime Factorization
Informal description
For any natural numbers $a$ and $b$, the left factor of the LCM based on prime factor multiplicities is positive, i.e., $\text{factorizationLCMLeft}(a, b) > 0$.
Nat.factorizationLCMRight_pos theorem
: 0 < factorizationLCMRight a b
Full source 
lemma factorizationLCMRight_pos :
    0 < factorizationLCMRight a b := by
  apply Nat.pos_of_ne_zero
  rw [factorizationLCMRight, Finsupp.prod_ne_zero_iff]
  intro p _ H
  by_cases h : b.factorization p ≤ a.factorization p
  · simp only [h, reduceIte, pow_eq_zero_iff', ne_eq, reduceCtorEq] at H
  · simp only [h, ↓reduceIte, pow_eq_zero_iff', ne_eq] at H
    simpa [H.1] using H.2
Positivity of the Right LCM Factorization Product
Informal description
For any two natural numbers $a$ and $b$, the product of primes in the LCM of $a$ and $b$ with strictly greater multiplicity in $b$ is strictly positive, i.e., $\text{factorizationLCMRight}(a, b) > 0$.
Nat.coprime_factorizationLCMLeft_factorizationLCMRight theorem
: (factorizationLCMLeft a b).Coprime (factorizationLCMRight a b)
Full source 
lemma coprime_factorizationLCMLeft_factorizationLCMRight :
    (factorizationLCMLeft a b).Coprime (factorizationLCMRight a b) := by
  rw [factorizationLCMLeft, factorizationLCMRight]
  refine coprime_prod_left_iff.mpr fun p hp ↦ coprime_prod_right_iff.mpr fun q hq ↦ ?_
  dsimp only; split_ifs with h h'
  any_goals simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]
  refine coprime_pow_primes _ _ (prime_of_mem_primeFactors hp) (prime_of_mem_primeFactors hq) ?_
  contrapose! h'; rwa [← h']
Coprimality of Left and Right LCM Factorization Components: $\gcd(\text{left}(a,b), \text{right}(a,b)) = 1$
Informal description
For any natural numbers $a$ and $b$, the left and right LCM factorization components $\text{factorizationLCMLeft}(a, b)$ and $\text{factorizationLCMRight}(a, b)$ are coprime. That is, \[ \gcd(\text{factorizationLCMLeft}(a, b), \text{factorizationLCMRight}(a, b)) = 1. \] Here: - $\text{factorizationLCMLeft}(a, b)$ is the product of primes in $\text{lcm}(a, b)$ where the multiplicity in $b$ is $\leq$ the multiplicity in $a$, - $\text{factorizationLCMRight}(a, b)$ is the product of primes in $\text{lcm}(a, b)$ where the multiplicity in $b$ is $>$ the multiplicity in $a$.
Nat.factorizationLCMLeft_mul_factorizationLCMRight theorem
(ha : a ≠ 0) (hb : b ≠ 0) : (factorizationLCMLeft a b) * (factorizationLCMRight a b) = lcm a b
Full source 
lemma factorizationLCMLeft_mul_factorizationLCMRight (ha : a ≠ 0) (hb : b ≠ 0) :
    (factorizationLCMLeft a b) * (factorizationLCMRight a b) = lcm a b := by
  rw [← factorization_prod_pow_eq_self (lcm_ne_zero ha hb), factorizationLCMLeft,
    factorizationLCMRight, ← prod_mul]
  congr; ext p n; split_ifs <;> simp
Factorization Decomposition of LCM: $\text{left}(a,b) \times \text{right}(a,b) = \text{lcm}(a,b)$
Informal description
For any nonzero natural numbers $a$ and $b$, the product of the left and right LCM factorization components equals the least common multiple of $a$ and $b$, i.e., \[ \text{factorizationLCMLeft}(a, b) \times \text{factorizationLCMRight}(a, b) = \text{lcm}(a, b). \] Here: - $\text{factorizationLCMLeft}(a, b)$ is the product of primes in $\text{lcm}(a, b)$ where the multiplicity in $b$ is $\leq$ the multiplicity in $a$, - $\text{factorizationLCMRight}(a, b)$ is the product of primes in $\text{lcm}(a, b)$ where the multiplicity in $b$ is $>$ the multiplicity in $a$.
Nat.factorizationLCMLeft_dvd_left theorem
: factorizationLCMLeft a b ∣ a
Full source 
lemma factorizationLCMLeft_dvd_left : factorizationLCMLeftfactorizationLCMLeft a b ∣ a := by
  rcases eq_or_ne a 0 with rfl | ha
  · simp only [dvd_zero]
  rcases eq_or_ne b 0 with rfl | hb
  · simp [factorizationLCMLeft]
  nth_rewrite 2 [← factorization_prod_pow_eq_self ha]
  rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
  · apply prod_dvd_prod_of_dvd; rintro p -; dsimp only; split_ifs with le
    · rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le le_rfl le
    · apply one_dvd
  · intro p hp; rw [mem_support_iff] at hp ⊢
    rw [factorization_lcm ha hb]; exact (lt_sup_iff.mpr <| .inl <| Nat.pos_of_ne_zero hp).ne'
  · intros; rw [pow_zero]
Left LCM Factorization Component Divides First Argument
Informal description
For any natural numbers $a$ and $b$, the left LCM factorization component $\text{factorizationLCMLeft}(a, b)$ divides $a$.
Nat.factorizationLCMRight_dvd_right theorem
: factorizationLCMRight a b ∣ b
Full source 
lemma factorizationLCMRight_dvd_right : factorizationLCMRightfactorizationLCMRight a b ∣ b := by
  rcases eq_or_ne a 0 with rfl | ha
  · simp [factorizationLCMRight]
  rcases eq_or_ne b 0 with rfl | hb
  · simp only [dvd_zero]
  nth_rewrite 2 [← factorization_prod_pow_eq_self hb]
  rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
  · apply Finset.prod_dvd_prod_of_dvd; rintro p -; dsimp only; split_ifs with le
    · apply one_dvd
    · rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le (not_le.1 le).le le_rfl
  · intro p hp; rw [mem_support_iff] at hp ⊢
    rw [factorization_lcm ha hb]; exact (lt_sup_iff.mpr <| .inr <| Nat.pos_of_ne_zero hp).ne'
  · intros; rw [pow_zero]
Divisibility of Right LCM Factorization Component: $\text{factorizationLCMRight}(a, b) \mid b$
Informal description
For any natural numbers $a$ and $b$, the right LCM factorization component $\text{factorizationLCMRight}(a, b)$ divides $b$. Here, $\text{factorizationLCMRight}(a, b)$ is defined as the product of primes in $\text{lcm}(a, b)$ where the multiplicity in $b$ is strictly greater than the multiplicity in $a$, each raised to their respective multiplicity in $\text{lcm}(a, b)$.
Nat.prod_primeFactors_gcd_mul_prod_primeFactors_mul theorem
{β : Type*} [CommMonoid β] (m n : ℕ) (f : ℕ → β) : (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
Full source 
@[to_additive sum_primeFactors_gcd_add_sum_primeFactors_mul]
theorem prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type*} [CommMonoid β] (m n : ℕ)
    (f : ℕ → β) :
    (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f =
      m.primeFactors.prod f * n.primeFactors.prod f := by
  obtain rfl | hm₀ := eq_or_ne m 0
  · simp
  obtain rfl | hn₀ := eq_or_ne n 0
  · simp
  · rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]
Product of Prime Factors Identity for GCD and Product
Informal description
Let $β$ be a commutative monoid, and let $m, n$ be natural numbers. For any function $f : ℕ → β$, we have: \[ \prod_{p \in \text{primeFactors}(\gcd(m, n))} f(p) \cdot \prod_{p \in \text{primeFactors}(m \cdot n)} f(p) = \prod_{p \in \text{primeFactors}(m)} f(p) \cdot \prod_{p \in \text{primeFactors}(n)} f(p) \] where $\text{primeFactors}(k)$ denotes the set of prime factors of $k$.
Nat.setOf_pow_dvd_eq_Icc_factorization theorem
{n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) : {i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p)
Full source 
theorem setOf_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) :
    { i : ℕ | i ≠ 0 ∧ p ^ i ∣ n } = Set.Icc 1 (n.factorization p) := by
  ext
  simp [Nat.lt_succ_iff, one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]
Characterization of Prime Power Divisors: $\{i \neq 0 \mid p^i \mid n\} = [1, n.\text{factorization}(p)]$ for Prime $p$ and $n \neq 0$
Informal description
For any prime natural number $p$ and any nonzero natural number $n$, the set of positive integers $i$ such that $p^i$ divides $n$ is equal to the closed interval $[1, n.\text{factorization}(p)]$. In other words: \[ \{i \in \mathbb{N} \mid i \neq 0 \text{ and } p^i \mid n\} = [1, n.\text{factorization}(p)] \]
Nat.Icc_factorization_eq_pow_dvd theorem
(n : ℕ) {p : ℕ} (pp : Prime p) : Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}
Full source 
/-- 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 Icc_factorization_eq_pow_dvd (n : ℕ) {p : ℕ} (pp : Prime p) :
    Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n} := by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  ext x
  simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff,
    pp.pow_dvd_iff_le_factorization hn, iff_and_self]
  exact fun _ H => lt_of_le_of_lt H (factorization_lt p hn)
Characterization of Prime Power Divisors via Factorization Multiplicity: $[1, n.\text{factorization}(p)] = \{i \in [1, n) \mid p^i \mid n\}$
Informal description
For any natural number $n$ and prime number $p$, the closed interval of integers from $1$ to the multiplicity of $p$ in the prime factorization of $n$ (i.e., $[1, n.\text{factorization}(p)]$) is equal to the set of integers $i$ in the half-open interval $[1, n)$ for which $p^i$ divides $n$.
Nat.factorization_eq_card_pow_dvd theorem
(n : ℕ) {p : ℕ} (pp : p.Prime) : n.factorization p = #({i ∈ Ico 1 n | p ^ i ∣ n})
Full source 
theorem factorization_eq_card_pow_dvd (n : ℕ) {p : ℕ} (pp : p.Prime) :
    n.factorization p = #{i ∈ Ico 1 n | p ^ i ∣ n} := by
  simp [← Icc_factorization_eq_pow_dvd n pp]
Prime Multiplicity Equals Count of Prime Power Divisors in Interval $[1, n)$
Informal description
For any natural number $n$ and prime number $p$, the multiplicity of $p$ in the prime factorization of $n$ is equal to the cardinality of the set of integers $i$ in the half-open interval $[1, n)$ such that $p^i$ divides $n$. In other words: \[ n.\text{factorization}(p) = \#\{i \in [1, n) \mid p^i \mid n\}. \]
Nat.Ico_filter_pow_dvd_eq theorem
{n p b : ℕ} (pp : p.Prime) (hn : n ≠ 0) (hb : n ≤ p ^ b) : {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n}
Full source 
theorem Ico_filter_pow_dvd_eq {n p b : ℕ} (pp : p.Prime) (hn : n ≠ 0) (hb : n ≤ p ^ b) :
    {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n} := by
  ext x
  simp only [Finset.mem_filter, mem_Ico, mem_Icc, and_congr_left_iff, and_congr_right_iff]
  rintro h1 -
  exact iff_of_true (lt_of_pow_dvd_right hn pp.two_le h1) <|
    (Nat.pow_le_pow_iff_right pp.one_lt).1 <| (le_of_dvd hn.bot_lt h1).trans hb
Equality of Prime Power Divisibility Sets in Bounded Intervals
Informal description
For natural numbers $n$, $p$, and $b$, where $p$ is prime, $n \neq 0$, and $n \leq p^b$, the set of exponents $i$ in the half-open interval $[1, n)$ such that $p^i$ divides $n$ is equal to the set of exponents $i$ in the closed interval $[1, b]$ such that $p^i$ divides $n$. In other words: $$\{i \in [1, n) \mid p^i \mid n\} = \{i \in [1, b] \mid p^i \mid n\}.$$
Nat.factorization_eq_of_coprime_left theorem
{p a b : ℕ} (hab : Coprime a b) (hpa : p ∈ a.primeFactorsList) : (a * b).factorization p = a.factorization p
Full source 
/-- 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 factorization_eq_of_coprime_left {p a b : ℕ} (hab : Coprime a b)
    (hpa : p ∈ a.primeFactorsList) : (a * b).factorization p = a.factorization p := by
  rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq,
    ← primeFactorsList_count_eq,
    count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]
Preservation of Prime Multiplicity in Coprime Product (Left Factor)
Informal description
For any natural numbers $a$, $b$, and prime $p$, if $a$ and $b$ are coprime and $p$ is a prime factor of $a$, then the multiplicity of $p$ in the prime factorization of $a \cdot b$ is equal to the multiplicity of $p$ in the prime factorization of $a$, i.e., \[ (a \cdot b).\text{factorization}(p) = a.\text{factorization}(p). \]
Nat.factorization_eq_of_coprime_right theorem
{p a b : ℕ} (hab : Coprime a b) (hpb : p ∈ b.primeFactorsList) : (a * b).factorization p = b.factorization p
Full source 
/-- 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`. -/
theorem factorization_eq_of_coprime_right {p a b : ℕ} (hab : Coprime a b)
    (hpb : p ∈ b.primeFactorsList) : (a * b).factorization p = b.factorization p := by
  rw [mul_comm]
  exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb
Preservation of Prime Multiplicity in Coprime Product (Right Factor)
Informal description
For any natural numbers $a$, $b$, and prime $p$, if $a$ and $b$ are coprime and $p$ is a prime factor of $b$, then the multiplicity of $p$ in the prime factorization of $a \cdot b$ is equal to the multiplicity of $p$ in the prime factorization of $b$, i.e., \[ (a \cdot b).\text{factorization}(p) = b.\text{factorization}(p). \]
Nat.prod_pow_prime_padicValNat theorem
(n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n < m) : ∏ p ∈ range m with p.Prime, p ^ padicValNat p n = n
Full source 
theorem prod_pow_prime_padicValNat (n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n < m) :
    ∏ p ∈ range m with p.Prime, p ^ padicValNat p n = n := by
  nth_rw 2 [← factorization_prod_pow_eq_self hn]
  rw [eq_comm]
  apply Finset.prod_subset_one_on_sdiff
  · exact fun p hp => Finset.mem_filter.mpr ⟨Finset.mem_range.2 <| pr.trans_le' <|
      le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩
  · intro p hp
    obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp
    rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
    simp [Finsupp.not_mem_support_iff.mp hp2]
  · intro p hp
    simp [factorization_def n (prime_of_mem_primeFactors hp)]
Prime Factorization Product over Primes Less Than $m$ Equals $n$
Informal description
For any nonzero natural number $n$ and any natural number $m$ such that $n < m$, the product of the prime powers $p^{v_p(n)}$ over all primes $p < m$ equals $n$, i.e., \[ \prod_{\substack{p \text{ prime} \\ p < m}} p^{v_p(n)} = n, \] where $v_p(n)$ denotes the $p$-adic valuation of $n$.
Nat.card_multiples theorem
(n p : ℕ) : #({e ∈ range n | p ∣ e + 1}) = n / p
Full source 
/-- Exactly `n / p` naturals in `[1, n]` are multiples of `p`.
See `Nat.card_multiples'` for an alternative spelling of the statement. -/
theorem card_multiples (n p : ℕ) : #{e ∈ range n | p ∣ e + 1} = n / p := by
  induction' n with n hn
  · simp
  simp [Nat.succ_div, add_ite, add_zero, Finset.range_succ, filter_insert, apply_ite card,
    card_insert_of_not_mem, hn]
Count of Multiples in Range: $\#\{1 \leq e \leq n \mid p \mid e\} = \lfloor n/p \rfloor$
Informal description
For any natural numbers $n$ and $p$, the number of multiples of $p$ in the set $\{1, 2, \dots, n\}$ is equal to the integer division of $n$ by $p$, i.e., $$\#\{e \in \{1, \dots, n\} \mid p \mid e\} = \left\lfloor \frac{n}{p} \right\rfloor.$$
Nat.Ioc_filter_dvd_card_eq_div theorem
(n p : ℕ) : #({x ∈ Ioc 0 n | p ∣ x}) = n / p
Full source 
/-- Exactly `n / p` naturals in `(0, n]` are multiples of `p`. -/
theorem Ioc_filter_dvd_card_eq_div (n p : ℕ) : #{x ∈ Ioc 0 n | p ∣ x} = n / p := by
  induction' n with n IH
  · simp
  -- TODO: Golf away `h1` after Yaël PRs a lemma asserting this
  have h1 : Ioc 0 n.succ = insert n.succ (Ioc 0 n) := by
    rcases n.eq_zero_or_pos with (rfl | hn)
    · simp
    simp_rw [← Ico_succ_succ, Ico_insert_right (succ_le_succ hn.le), Ico_succ_right]
  simp [Nat.succ_div, add_ite, add_zero, h1, filter_insert, apply_ite card, card_insert_eq_ite, IH,
    Finset.mem_filter, mem_Ioc, not_le.2 (lt_add_one n)]
Count of Multiples in $(0, n]$: $\#\{x \in (0, n] \mid p \mid x\} = \lfloor n/p \rfloor$
Informal description
For any natural numbers $n$ and $p$, the number of multiples of $p$ in the open-closed interval $(0, n]$ is equal to the integer division of $n$ by $p$, i.e., $$\#\{x \in (0, n] \mid p \mid x\} = \left\lfloor \frac{n}{p} \right\rfloor.$$
Nat.card_multiples' theorem
(N n : ℕ) : #({k ∈ range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
Full source 
/-- There are exactly `⌊N/n⌋` positive multiples of `n` that are `≤ N`.
See `Nat.card_multiples` for a "shifted-by-one" version. -/
lemma card_multiples' (N n : ℕ) : #{k ∈ range N.succ | k ≠ 0 ∧ n ∣ k} = N / n := by
  induction N with
    | zero => simp [Finset.filter_false_of_mem]
    | succ N ih =>
        rw [Finset.range_succ, Finset.filter_insert]
        by_cases h : n ∣ N.succ
        · simp [h, succ_div_of_dvd, ih]
        · simp [h, succ_div_of_not_dvd, ih]
Count of Positive Multiples: $\#\{1 \leq k \leq N \mid n \mid k\} = \lfloor N/n \rfloor$
Informal description
For any natural numbers $N$ and $n$, the number of positive multiples of $n$ in the set $\{1, 2, \dots, N\}$ is equal to the integer division of $N$ by $n$, i.e., $$\#\{k \in \{1, \dots, N\} \mid n \mid k\} = \left\lfloor \frac{N}{n} \right\rfloor.$$