doc-next-gen

Mathlib.Data.Nat.PrimeFin

Module docstring

{"# Prime numbers

This file contains some results about prime numbers which depend on finiteness of sets. "}

Nat.primeFactors definition
(n : ℕ) : Finset ℕ
Full source 
/-- The prime factors of a natural number as a finset. -/
def primeFactors (n : ℕ) : Finset ℕ := n.primeFactorsList.toFinset
Set of prime factors of a natural number
Informal description
The function maps a natural number \( n \) to the finite set of its prime factors. For \( n = 0 \) or \( n = 1 \), the result is the empty set. For \( n \geq 2 \), the result is the set of distinct prime numbers dividing \( n \).
Nat.toFinset_factors theorem
(n : ℕ) : n.primeFactorsList.toFinset = n.primeFactors
Full source 
@[simp] lemma toFinset_factors (n : ℕ) : n.primeFactorsList.toFinset = n.primeFactors := rfl
Equality of Prime Factor Set and List-to-Set Conversion
Informal description
For any natural number $n$, the finite set obtained from the list of its prime factors (in increasing order) is equal to the set of its prime factors. That is, $\mathrm{toFinset}(\mathrm{primeFactorsList}(n)) = \mathrm{primeFactors}(n)$.
Nat.mem_primeFactors theorem
: p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0
Full source 
@[simp] lemma mem_primeFactors : p ∈ n.primeFactorsp ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
  simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']
Characterization of Prime Factors Membership
Informal description
For any natural numbers $p$ and $n$, the prime number $p$ belongs to the set of prime factors of $n$ if and only if $p$ is prime, $p$ divides $n$, and $n$ is nonzero. That is, $p \in \mathrm{primeFactors}(n) \leftrightarrow (p \text{ is prime}) \land (p \mid n) \land (n \neq 0)$.
Nat.mem_primeFactors_of_ne_zero theorem
(hn : n ≠ 0) : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n
Full source 
lemma mem_primeFactors_of_ne_zero (hn : n ≠ 0) : p ∈ n.primeFactorsp ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n := by
  simp [hn]
Characterization of Prime Factors for Nonzero Natural Numbers
Informal description
For any natural number $n \neq 0$, a prime number $p$ belongs to the set of prime factors of $n$ if and only if $p$ is prime and $p$ divides $n$. In other words, $p \in \mathrm{primeFactors}(n) \leftrightarrow (p \text{ is prime}) \land (p \mid n)$.
Nat.primeFactors_mono theorem
(hmn : m ∣ n) (hn : n ≠ 0) : primeFactors m ⊆ primeFactors n
Full source 
lemma primeFactors_mono (hmn : m ∣ n) (hn : n ≠ 0) : primeFactorsprimeFactors m ⊆ primeFactors n := by
  simp only [subset_iff, mem_primeFactors, and_imp]
  exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩
Monotonicity of Prime Factors under Divisibility
Informal description
For any natural numbers $m$ and $n$ such that $m$ divides $n$ and $n \neq 0$, the set of prime factors of $m$ is a subset of the set of prime factors of $n$.
Nat.mem_primeFactors_iff_mem_primeFactorsList theorem
: p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList
Full source 
lemma mem_primeFactors_iff_mem_primeFactorsList : p ∈ n.primeFactorsp ∈ n.primeFactors ↔ p ∈ n.primeFactorsList := by
  simp only [primeFactors, List.mem_toFinset]
Equivalence of Prime Factor Membership in Set and List Representations
Informal description
A prime number $p$ belongs to the set of prime factors of a natural number $n$ if and only if $p$ appears in the list of prime factors of $n$.
Nat.prime_of_mem_primeFactors theorem
(hp : p ∈ n.primeFactors) : p.Prime
Full source 
lemma prime_of_mem_primeFactors (hp : p ∈ n.primeFactors) : p.Prime := (mem_primeFactors.1 hp).1
Prime Factor Implies Prime
Informal description
For any natural numbers $p$ and $n$, if $p$ belongs to the set of prime factors of $n$, then $p$ is a prime number.
Nat.dvd_of_mem_primeFactors theorem
(hp : p ∈ n.primeFactors) : p ∣ n
Full source 
lemma dvd_of_mem_primeFactors (hp : p ∈ n.primeFactors) : p ∣ n := (mem_primeFactors.1 hp).2.1
Prime Factor Divides Number
Informal description
For any natural numbers $p$ and $n$, if $p$ belongs to the set of prime factors of $n$, then $p$ divides $n$. That is, $p \in \mathrm{primeFactors}(n) \implies p \mid n$.
Nat.pos_of_mem_primeFactors theorem
(hp : p ∈ n.primeFactors) : 0 < p
Full source 
lemma pos_of_mem_primeFactors (hp : p ∈ n.primeFactors) : 0 < p :=
  (prime_of_mem_primeFactors hp).pos
Positivity of Prime Factors
Informal description
For any natural numbers $p$ and $n$, if $p$ belongs to the set of prime factors of $n$, then $p$ is positive, i.e., $0 < p$.
Nat.le_of_mem_primeFactors theorem
(h : p ∈ n.primeFactors) : p ≤ n
Full source 
lemma le_of_mem_primeFactors (h : p ∈ n.primeFactors) : p ≤ n :=
  le_of_dvd (mem_primeFactors.1 h).2.2.bot_lt <| dvd_of_mem_primeFactors h
Prime Factor Bound: $p \leq n$ for $p \in \mathrm{primeFactors}(n)$
Informal description
For any natural numbers $p$ and $n$, if $p$ belongs to the set of prime factors of $n$, then $p$ is less than or equal to $n$, i.e., $p \in \mathrm{primeFactors}(n) \implies p \leq n$.
Nat.primeFactors_zero theorem
: primeFactors 0 = ∅
Full source 
@[simp] lemma primeFactors_zero : primeFactors 0 = ∅ := by
  ext
  simp
Prime factors of zero are empty
Informal description
The set of prime factors of the natural number $0$ is empty, i.e., $\mathrm{primeFactors}(0) = \emptyset$.
Nat.primeFactors_one theorem
: primeFactors 1 = ∅
Full source 
@[simp] lemma primeFactors_one : primeFactors 1 = ∅ := by
  ext
  simpa using Prime.ne_one
Prime Factors of One are Empty
Informal description
The set of prime factors of the natural number $1$ is empty, i.e., $\mathrm{primeFactors}(1) = \emptyset$.
Nat.primeFactors_eq_empty theorem
: n.primeFactors = ∅ ↔ n = 0 ∨ n = 1
Full source 
@[simp] lemma primeFactors_eq_empty : n.primeFactors = ∅ ↔ n = 0 ∨ n = 1 := by
  constructor
  · contrapose!
    rintro hn
    obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2
    exact Nonempty.ne_empty <| ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩
  · rintro (rfl | rfl) <;> simp
Characterization of Natural Numbers with Empty Prime Factors: $\mathrm{primeFactors}(n) = \emptyset \leftrightarrow n = 0 \lor n = 1$
Informal description
For any natural number $n$, the set of prime factors of $n$ is empty if and only if $n = 0$ or $n = 1$. That is, $\mathrm{primeFactors}(n) = \emptyset \leftrightarrow (n = 0 \lor n = 1)$.
Nat.nonempty_primeFactors theorem
{n : ℕ} : n.primeFactors.Nonempty ↔ 1 < n
Full source 
@[simp]
lemma nonempty_primeFactors {n : ℕ} : n.primeFactors.Nonempty ↔ 1 < n := by
  rw [← not_iff_not, Finset.not_nonempty_iff_eq_empty, primeFactors_eq_empty, not_lt,
    Nat.le_one_iff_eq_zero_or_eq_one]
Nonempty Prime Factors Characterization: $\mathrm{primeFactors}(n) \neq \emptyset \leftrightarrow n > 1$
Informal description
For any natural number $n$, the set of prime factors of $n$ is nonempty if and only if $n > 1$.
Nat.Prime.primeFactors theorem
(hp : p.Prime) : p.primeFactors = { p }
Full source 
@[simp] protected lemma Prime.primeFactors (hp : p.Prime) : p.primeFactors = {p} := by
  simp [Nat.primeFactors, primeFactorsList_prime hp]
Prime Factors of a Prime Number Form a Singleton Set
Informal description
For any prime natural number $p$, the set of prime factors of $p$ is the singleton set $\{p\}$.
Nat.primeFactors_mul theorem
(ha : a ≠ 0) (hb : b ≠ 0) : (a * b).primeFactors = a.primeFactors ∪ b.primeFactors
Full source 
lemma primeFactors_mul (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b).primeFactors = a.primeFactors ∪ b.primeFactors := by
  ext; simp only [Finset.mem_union, mem_primeFactors_iff_mem_primeFactorsList,
    mem_primeFactorsList_mul ha hb]
Prime Factorization of Product: $\text{primeFactors}(a \cdot b) = \text{primeFactors}(a) \cup \text{primeFactors}(b)$
Informal description
For any nonzero natural numbers $a$ and $b$, the set of prime factors of the product $a \cdot b$ is equal to the union of the sets of prime factors of $a$ and $b$. In symbols: \[ \text{primeFactors}(a \cdot b) = \text{primeFactors}(a) \cup \text{primeFactors}(b). \]
Nat.Coprime.primeFactors_mul theorem
{a b : ℕ} (hab : Coprime a b) : (a * b).primeFactors = a.primeFactors ∪ b.primeFactors
Full source 
lemma Coprime.primeFactors_mul {a b : ℕ} (hab : Coprime a b) :
    (a * b).primeFactors = a.primeFactors ∪ b.primeFactors :=
  (List.toFinset.ext <| mem_primeFactorsList_mul_of_coprime hab).trans <| List.toFinset_union _ _
Prime Factorization of Coprime Product: $\text{primeFactors}(a \cdot b) = \text{primeFactors}(a) \cup \text{primeFactors}(b)$ for coprime $a, b$
Informal description
For any two coprime natural numbers $a$ and $b$, the set of prime factors of their product $a \cdot b$ is equal to the union of the sets of prime factors of $a$ and $b$. In symbols: \[ \text{primeFactors}(a \cdot b) = \text{primeFactors}(a) \cup \text{primeFactors}(b). \]
Nat.primeFactors_gcd theorem
(ha : a ≠ 0) (hb : b ≠ 0) : (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors
Full source 
lemma primeFactors_gcd (ha : a ≠ 0) (hb : b ≠ 0) :
    (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors := by
  ext; simp [dvd_gcd_iff, ha, hb, gcd_ne_zero_left ha]; aesop
Prime Factors of GCD Equals Intersection of Prime Factors
Informal description
For any nonzero natural numbers $a$ and $b$, the set of prime factors of the greatest common divisor of $a$ and $b$ is equal to the intersection of the sets of prime factors of $a$ and $b$. In other words, $\text{primeFactors}(\gcd(a, b)) = \text{primeFactors}(a) \cap \text{primeFactors}(b)$.
Nat.disjoint_primeFactors theorem
(ha : a ≠ 0) (hb : b ≠ 0) : Disjoint a.primeFactors b.primeFactors ↔ Coprime a b
Full source 
@[simp] lemma disjoint_primeFactors (ha : a ≠ 0) (hb : b ≠ 0) :
    DisjointDisjoint a.primeFactors b.primeFactors ↔ Coprime a b := by
  simp [disjoint_iff_inter_eq_empty, coprime_iff_gcd_eq_one, ← primeFactors_gcd, gcd_ne_zero_left,
    ha, hb]
Disjoint Prime Factors Characterize Coprime Numbers
Informal description
For any nonzero natural numbers $a$ and $b$, the prime factors of $a$ and $b$ are disjoint if and only if $a$ and $b$ are coprime.
Nat.Coprime.disjoint_primeFactors theorem
(hab : Coprime a b) : Disjoint a.primeFactors b.primeFactors
Full source 
protected lemma Coprime.disjoint_primeFactors (hab : Coprime a b) :
    Disjoint a.primeFactors b.primeFactors :=
  List.disjoint_toFinset_iff_disjoint.2 <| coprime_primeFactorsList_disjoint hab
Disjoint Prime Factors for Coprime Numbers
Informal description
For any two coprime natural numbers $a$ and $b$, the sets of their prime factors are disjoint. That is, if $a$ and $b$ are coprime, then $\text{primeFactors}(a) \cap \text{primeFactors}(b) = \emptyset$.
Nat.primeFactors_pow_succ theorem
(n k : ℕ) : (n ^ (k + 1)).primeFactors = n.primeFactors
Full source 
lemma primeFactors_pow_succ (n k : ℕ) : (n ^ (k + 1)).primeFactors = n.primeFactors := by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  induction' k with k ih
  · simp
  · rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
Prime Factors of Power: $\mathrm{primeFactors}(n^{k+1}) = \mathrm{primeFactors}(n)$
Informal description
For any natural numbers $n$ and $k$, the set of prime factors of $n^{k+1}$ is equal to the set of prime factors of $n$. That is, \[ \mathrm{primeFactors}(n^{k+1}) = \mathrm{primeFactors}(n). \]
Nat.primeFactors_pow theorem
(n : ℕ) (hk : k ≠ 0) : (n ^ k).primeFactors = n.primeFactors
Full source 
lemma primeFactors_pow (n : ℕ) (hk : k ≠ 0) : (n ^ k).primeFactors = n.primeFactors := by
  cases k
  · simp at hk
  rw [primeFactors_pow_succ]
Prime Factors of Power: $\mathrm{primeFactors}(n^k) = \mathrm{primeFactors}(n)$ for $k \neq 0$
Informal description
For any natural number $n$ and any nonzero natural number $k$, the set of prime factors of $n^k$ is equal to the set of prime factors of $n$. That is, \[ \mathrm{primeFactors}(n^k) = \mathrm{primeFactors}(n). \]
Nat.primeFactors_prime_pow theorem
(hk : k ≠ 0) (hp : Prime p) : (p ^ k).primeFactors = { p }
Full source 
/-- The only prime divisor of positive prime power `p^k` is `p` itself -/
lemma primeFactors_prime_pow (hk : k ≠ 0) (hp : Prime p) :
    (p ^ k).primeFactors = {p} := by simp [primeFactors_pow p hk, hp]
Prime Factors of Prime Power: $\mathrm{primeFactors}(p^k) = \{p\}$ for $k \neq 0$
Informal description
For any prime natural number $p$ and any nonzero natural number $k$, the set of prime factors of $p^k$ is the singleton set $\{p\}$. That is, \[ \mathrm{primeFactors}(p^k) = \{p\}. \]