Mathlib.NumberTheory.Divisors

Nat.divisors definition

: Finset ℕ

Full source

/-- `divisors n` is the `Finset` of divisors of `n`. By convention, we set `divisors 0 = ∅`. -/
def divisors : Finset ℕ := {d ∈ Ico 1 (n + 1) | d ∣ n}

Set of divisors of a natural number

Informal description

For a natural number $ n $, the finset `Nat.divisors n` consists of all natural numbers $ d $ such that $ 1 \leq d \leq n $ and $ d $ divides $ n $. By convention, this finset is empty when $ n = 0 $.

Nat.properDivisors definition

: Finset ℕ

Full source

/-- `properDivisors n` is the `Finset` of divisors of `n`, other than `n`.
By convention, we set `properDivisors 0 = ∅`. -/
def properDivisors : Finset ℕ := {d ∈ Ico 1 n | d ∣ n}

Proper divisors of a natural number

Informal description

For a natural number $ n $, the finset `Nat.properDivisors n` consists of all natural numbers $ d $ such that $ 1 \leq d < n $ and $ d $ divides $ n $. By convention, this finset is empty when $ n = 0 $.

Nat.divisorsAntidiagonal definition

: Finset (ℕ × ℕ)

Full source

/-- Pairs of divisors of a natural number as a finset.

`n.divisorsAntidiagonal` is the finset of pairs `(a, b) : ℕ × ℕ` such that `a * b = n`.
By convention, we set `Nat.divisorsAntidiagonal 0 = ∅`.

O(n). -/
def divisorsAntidiagonal : Finset (ℕℕ × ℕ) :=
  (Icc 1 n).filterMap (fun x ↦ let y := n / x; if x * y = n then some (x, y) else none)
    fun x₁ x₂ (x, y) hx₁ hx₂ ↦ by aesop

Finset of divisor pairs for a natural number

Informal description

For a natural number $ n $, the finset `Nat.divisorsAntidiagonal n` consists of all pairs $(a, b)$ of natural numbers such that $a \times b = n$. By convention, this finset is empty when $n = 0$.

Nat.divisorsAntidiagonalList definition

(n : ℕ) : List (ℕ × ℕ)

Full source

/-- Pairs of divisors of a natural number, as a list.

`n.divisorsAntidiagonalList` is the list of pairs `(a, b) : ℕ × ℕ` such that `a * b = n`, ordered
by increasing `a`. By convention, we set `Nat.divisorsAntidiagonalList 0 = []`.
-/
def divisorsAntidiagonalList (n : ℕ) : List (ℕℕ × ℕ) :=
  (List.range' 1 n).filterMap
    (fun x ↦ let y := n / x; if x * y = n then some (x, y) else none)

List of divisor pairs for a natural number

Informal description

For a natural number $ n $, the list `Nat.divisorsAntidiagonalList n` consists of all pairs $(a, b)$ of natural numbers such that $a \times b = n$, ordered by increasing $a$. By convention, the list is empty when $n = 0$.

Nat.filter_dvd_eq_divisors theorem

(h : n ≠ 0) : {d ∈ range n.succ | d ∣ n} = n.divisors

Full source

@[simp]
theorem filter_dvd_eq_divisors (h : n ≠ 0) : {d ∈ range n.succ | d ∣ n} = n.divisors := by
  ext
  simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
  exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Characterization of Divisors via Range Filtering

Informal description

For any nonzero natural number $n$, the set of natural numbers $d$ in the range $[0, n+1)$ that divide $n$ is equal to the set of divisors of $n$. In other words, $\{d \in [0, n+1) \mid d \mid n\} = \text{divisors}(n)$.

Nat.filter_dvd_eq_properDivisors theorem

(h : n ≠ 0) : {d ∈ range n | d ∣ n} = n.properDivisors

Full source

@[simp]
theorem filter_dvd_eq_properDivisors (h : n ≠ 0) : {d ∈ range n | d ∣ n} = n.properDivisors := by
  ext
  simp only [properDivisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
  exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Characterization of Proper Divisors via Range and Divisibility

Informal description

For any nonzero natural number $n$, the set of natural numbers $d$ in the range $[0, n)$ that divide $n$ is equal to the set of proper divisors of $n$. In other words, $\{d \in \mathbb{N} \mid d < n \text{ and } d \mid n\} = \text{properDivisors}(n)$.

Nat.properDivisors.not_self_mem theorem

: ¬n ∈ properDivisors n

Full source

theorem properDivisors.not_self_mem : ¬n ∈ properDivisors n := by simp [properDivisors]

Proper Divisors Exclude the Number Itself

Informal description

For any natural number $n$, the number $n$ itself is not an element of its proper divisors, i.e., $n \notin \text{properDivisors}(n)$.

Nat.mem_properDivisors theorem

{m : ℕ} : n ∈ properDivisors m ↔ n ∣ m ∧ n < m

Full source

@[simp]
theorem mem_properDivisors {m : ℕ} : n ∈ properDivisors mn ∈ properDivisors m ↔ n ∣ m ∧ n < m := by
  rcases eq_or_ne m 0 with (rfl | hm); · simp [properDivisors]
  simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range]

Characterization of Proper Divisors: $n \in \text{properDivisors}(m) \leftrightarrow n \mid m \land n < m$

Informal description

For any natural numbers $n$ and $m$, $n$ is a proper divisor of $m$ if and only if $n$ divides $m$ and $n < m$. In other words, $n \in \text{properDivisors}(m) \leftrightarrow (n \mid m) \land (n < m)$.

Nat.insert_self_properDivisors theorem

(h : n ≠ 0) : insert n (properDivisors n) = divisors n

Full source

theorem insert_self_properDivisors (h : n ≠ 0) : insert n (properDivisors n) = divisors n := by
  rw [divisors, properDivisors, Ico_succ_right_eq_insert_Ico (one_le_iff_ne_zero.2 h),
    Finset.filter_insert, if_pos (dvd_refl n)]

Union of Proper Divisors with Self Equals Divisors for Nonzero Natural Numbers

Informal description

For any nonzero natural number $n$, the set of divisors of $n$ is equal to the union of $\{n\}$ and the set of proper divisors of $n$, i.e., $$ \{n\} \cup \text{properDivisors}(n) = \text{divisors}(n). $$

Nat.cons_self_properDivisors theorem

(h : n ≠ 0) : cons n (properDivisors n) properDivisors.not_self_mem = divisors n

Full source

theorem cons_self_properDivisors (h : n ≠ 0) :
    cons n (properDivisors n) properDivisors.not_self_mem = divisors n := by
  rw [cons_eq_insert, insert_self_properDivisors h]

Construction of Divisors from Proper Divisors for Nonzero Natural Numbers

Informal description

For any nonzero natural number $n$, the finset of divisors of $n$ is equal to the finset obtained by inserting $n$ into the finset of proper divisors of $n$, i.e., $$ \text{cons}(n, \text{properDivisors}(n), \text{properDivisors.not\_self\_mem}) = \text{divisors}(n). $$

Nat.mem_divisors theorem

{m : ℕ} : n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0

Full source

@[simp]
theorem mem_divisors {m : ℕ} : n ∈ divisors mn ∈ divisors m ↔ n ∣ m ∧ m ≠ 0 := by
  rcases eq_or_ne m 0 with (rfl | hm); · simp [divisors]
  simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter,
    mem_range, and_iff_right_iff_imp, Nat.lt_succ_iff]
  exact le_of_dvd hm.bot_lt

Characterization of Membership in the Set of Divisors of a Natural Number

Informal description

For any natural numbers $n$ and $m$, $n$ is an element of the set of divisors of $m$ if and only if $n$ divides $m$ and $m$ is nonzero, i.e., $n \in \text{divisors}(m) \leftrightarrow (n \mid m) \wedge (m \neq 0)$.

Nat.one_mem_divisors theorem

: 1 ∈ divisors n ↔ n ≠ 0

Full source

theorem one_mem_divisors : 1 ∈ divisors n1 ∈ divisors n ↔ n ≠ 0 := by simp

One is a Divisor if and only if Nonzero

Informal description

The natural number $1$ is an element of the set of divisors of $n$ if and only if $n$ is nonzero, i.e., $1 \in \text{divisors}(n) \leftrightarrow n \neq 0$.

Nat.mem_divisors_self theorem

(n : ℕ) (h : n ≠ 0) : n ∈ n.divisors

Full source

theorem mem_divisors_self (n : ℕ) (h : n ≠ 0) : n ∈ n.divisors :=
  mem_divisors.2 ⟨dvd_rfl, h⟩

Self-Divisibility Property for Nonzero Natural Numbers

Informal description

For any nonzero natural number $n$, $n$ is an element of its own set of divisors, i.e., $n \in \text{divisors}(n)$.

Nat.dvd_of_mem_divisors theorem

{m : ℕ} (h : n ∈ divisors m) : n ∣ m

Full source

theorem dvd_of_mem_divisors {m : ℕ} (h : n ∈ divisors m) : n ∣ m := by
  cases m
  · apply dvd_zero
  · simp [mem_divisors.1 h]

Membership in Divisors Implies Divisibility

Informal description

For any natural numbers $n$ and $m$, if $n$ is an element of the set of divisors of $m$, then $n$ divides $m$.

Nat.mem_divisorsAntidiagonal theorem

{x : ℕ × ℕ} : x ∈ divisorsAntidiagonal n ↔ x.fst * x.snd = n ∧ n ≠ 0

Full source

@[simp]
theorem mem_divisorsAntidiagonal {x : ℕℕ × ℕ} :
    x ∈ divisorsAntidiagonal nx ∈ divisorsAntidiagonal n ↔ x.fst * x.snd = n ∧ n ≠ 0 := by
  obtain ⟨a, b⟩ := x
  simp only [divisorsAntidiagonal, mul_div_eq_iff_dvd, mem_filterMap, mem_Icc, one_le_iff_ne_zero,
    Option.ite_none_right_eq_some, Option.some.injEq, Prod.ext_iff, and_left_comm, exists_eq_left]
  constructor
  · rintro ⟨han, ⟨ha, han'⟩, rfl⟩
    simp [Nat.mul_div_eq_iff_dvd, han]
    omega
  · rintro ⟨rfl, hab⟩
    rw [mul_ne_zero_iff] at hab
    simpa [hab.1, hab.2] using Nat.le_mul_of_pos_right _ hab.2.bot_lt

Characterization of Divisor Pairs for Nonzero Natural Numbers

Informal description

For any pair of natural numbers $(a, b)$ and a natural number $n$, the pair $(a, b)$ belongs to the finset of divisor pairs of $n$ if and only if $a \times b = n$ and $n \neq 0$.

Nat.divisorsAntidiagonalList_zero theorem

: divisorsAntidiagonalList 0 = []

Full source

@[simp] lemma divisorsAntidiagonalList_zero : divisorsAntidiagonalList 0 = [] := rfl

Empty List of Divisor Pairs for Zero

Informal description

The list of divisor pairs for the natural number $0$ is empty, i.e., $\text{divisorsAntidiagonalList}(0) = []$.

Nat.divisorsAntidiagonalList_one theorem

: divisorsAntidiagonalList 1 = [(1, 1)]

Full source

@[simp] lemma divisorsAntidiagonalList_one : divisorsAntidiagonalList 1 = [(1, 1)] := rfl

Divisor pairs list for 1 is [(1, 1)]

Informal description

For the natural number $1$, the list of divisor pairs consists of the single pair $(1, 1)$, i.e., $\text{divisorsAntidiagonalList}(1) = [(1, 1)]$.

Nat.toFinset_divisorsAntidiagonalList theorem

{n : ℕ} : n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal

Full source

@[simp]
lemma toFinset_divisorsAntidiagonalList {n : ℕ} :
    n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal := by
  rw [divisorsAntidiagonalList, divisorsAntidiagonal, List.toFinset_filterMap (f_inj := by aesop),
    List.toFinset_range'_1_1]

Equality of Finset Conversion and Divisor Pairs Finset for Natural Numbers

Informal description

For any natural number $n$, the finset obtained by converting the list of divisor pairs $(a, b)$ (where $a \times b = n$) to a finset is equal to the finset of all such divisor pairs, i.e., $\text{toFinset}(\text{divisorsAntidiagonalList}(n)) = \text{divisorsAntidiagonal}(n)$.

Nat.sorted_divisorsAntidiagonalList_fst theorem

{n : ℕ} : n.divisorsAntidiagonalList.Sorted (·.fst < ·.fst)

Full source

lemma sorted_divisorsAntidiagonalList_fst {n : ℕ} :
    n.divisorsAntidiagonalList.Sorted (·.fst < ·.fst) := by
  refine (List.sorted_lt_range' _ _ Nat.one_ne_zero).filterMap fun a b c d h h' ha => ?_
  rw [Option.ite_none_right_eq_some, Option.some.injEq] at h h'
  simpa [← h.right, ← h'.right]

Strictly Increasing Order of First Components in Divisor Pairs List

Informal description

For any natural number $n$, the list of pairs $(a, b)$ such that $a \times b = n$ is sorted in strictly increasing order with respect to the first component $a$.

Nat.sorted_divisorsAntidiagonalList_snd theorem

{n : ℕ} : n.divisorsAntidiagonalList.Sorted (·.snd > ·.snd)

Full source

lemma sorted_divisorsAntidiagonalList_snd {n : ℕ} :
    n.divisorsAntidiagonalList.Sorted (·.snd > ·.snd) := by
  obtain rfl | hn := eq_or_ne n 0
  · simp
  refine (List.sorted_lt_range' _ _ Nat.one_ne_zero).filterMap ?_
  simp only [Option.ite_none_right_eq_some, Option.some.injEq, gt_iff_lt, and_imp, Prod.forall,
    Prod.mk.injEq]
  rintro a b _ _ _ _ ha rfl rfl hb rfl rfl hab
  rwa [Nat.div_lt_div_left hn ⟨_, hb.symm⟩ ⟨_, ha.symm⟩]

Strictly Decreasing Order of Second Components in Divisor Pairs List

Informal description

For any natural number $n$, the list of pairs $(a, b)$ such that $a \times b = n$ is sorted in strictly decreasing order with respect to the second component $b$.

Nat.nodup_divisorsAntidiagonalList theorem

{n : ℕ} : n.divisorsAntidiagonalList.Nodup

Full source

lemma nodup_divisorsAntidiagonalList {n : ℕ} : n.divisorsAntidiagonalList.Nodup :=
  have : IsIrrefl (ℕℕ × ℕ) (·.fst < ·.fst) := ⟨by simp⟩
  sorted_divisorsAntidiagonalList_fst.nodup

No Duplicates in Divisor Pairs List for Natural Numbers

Informal description

For any natural number $n$, the list of pairs $(a, b)$ such that $a \times b = n$ has no duplicate elements.

Nat.val_divisorsAntidiagonal theorem

(n : ℕ) : (divisorsAntidiagonal n).val = divisorsAntidiagonalList n

Full source

/-- The `Finset` and `List` versions agree by definition. -/
@[simp]
theorem val_divisorsAntidiagonal (n : ℕ) :
    (divisorsAntidiagonal n).val = divisorsAntidiagonalList n :=
  rfl

Equality of Finset and List Representations of Divisor Pairs for Natural Numbers

Informal description

For any natural number $n$, the underlying list of the finset `Nat.divisorsAntidiagonal n` is equal to the list `Nat.divisorsAntidiagonalList n`, which consists of all pairs $(a, b)$ of natural numbers such that $a \times b = n$ (and is empty when $n = 0$).

Nat.mem_divisorsAntidiagonalList theorem

{n : ℕ} {a : ℕ × ℕ} : a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0

Full source

@[simp]
lemma mem_divisorsAntidiagonalList {n : ℕ} {a : ℕℕ × ℕ} :
    a ∈ n.divisorsAntidiagonalLista ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0 := by
  rw [← List.mem_toFinset, toFinset_divisorsAntidiagonalList, mem_divisorsAntidiagonal]

Characterization of Divisor Pairs in List Form for Nonzero Natural Numbers

Informal description

For any natural number $n$ and any pair of natural numbers $(a, b)$, the pair $(a, b)$ belongs to the list of divisor pairs of $n$ if and only if $a \times b = n$ and $n \neq 0$.

Nat.swap_mem_divisorsAntidiagonalList theorem

{a : ℕ × ℕ} : a.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList

Full source

@[simp high]
lemma swap_mem_divisorsAntidiagonalList {a : ℕℕ × ℕ} :
    a.swap ∈ n.divisorsAntidiagonalLista.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList := by simp [mul_comm]

Swapped Pair Membership in Divisor Pairs List: $(b, a) \in \text{divisorsAntidiagonalList}(n) \leftrightarrow (a, b) \in \text{divisorsAntidiagonalList}(n)$

Informal description

For any pair of natural numbers $(a, b)$ and any natural number $n$, the swapped pair $(b, a)$ belongs to the list of divisor pairs of $n$ if and only if the original pair $(a, b)$ belongs to the list of divisor pairs of $n$.

Nat.reverse_divisorsAntidiagonalList theorem

(n : ℕ) : n.divisorsAntidiagonalList.reverse = n.divisorsAntidiagonalList.map .swap

Full source

lemma reverse_divisorsAntidiagonalList (n : ℕ) :
    n.divisorsAntidiagonalList.reverse = n.divisorsAntidiagonalList.map .swap := by
  have : IsAsymm (ℕℕ × ℕ) (·.snd < ·.snd) := ⟨fun _ _ ↦ lt_asymm⟩
  refine List.eq_of_perm_of_sorted ?_ sorted_divisorsAntidiagonalList_snd.reverse <|
    sorted_divisorsAntidiagonalList_fst.map _ fun _ _ ↦ id
  simp [List.reverse_perm', List.perm_ext_iff_of_nodup nodup_divisorsAntidiagonalList
    (nodup_divisorsAntidiagonalList.map Prod.swap_injective), mul_comm]

Reversed Divisor Pairs List Equals Swapped Pairs List

Informal description

For any natural number $n$, the reverse of the list of pairs $(a, b)$ such that $a \times b = n$ is equal to the list obtained by swapping the components of each pair in the original list. That is, $\text{reverse}(\text{divisorsAntidiagonalList}(n)) = \text{map}(\text{swap}, \text{divisorsAntidiagonalList}(n))$.

Nat.ne_zero_of_mem_divisorsAntidiagonal theorem

{p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) : p.1 ≠ 0 ∧ p.2 ≠ 0

Full source

lemma ne_zero_of_mem_divisorsAntidiagonal {p : ℕℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) :
    p.1 ≠ 0p.1 ≠ 0 ∧ p.2 ≠ 0 := by
  obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp
  exact mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)

Nonzero Components of Divisor Pairs

Informal description

For any pair of natural numbers $(a, b)$ in the divisor pairs finset of a natural number $n$, both $a$ and $b$ are nonzero, i.e., $a \neq 0$ and $b \neq 0$.

Nat.left_ne_zero_of_mem_divisorsAntidiagonal theorem

{p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) : p.1 ≠ 0

Full source

lemma left_ne_zero_of_mem_divisorsAntidiagonal {p : ℕℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) :
    p.1 ≠ 0 :=
  (ne_zero_of_mem_divisorsAntidiagonal hp).1

Nonzero First Component in Divisor Pairs

Informal description

For any pair of natural numbers $(a, b)$ in the divisor pairs finset of a natural number $n$, the first component $a$ is nonzero, i.e., $a \neq 0$.

Nat.right_ne_zero_of_mem_divisorsAntidiagonal theorem

{p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) : p.2 ≠ 0

Full source

lemma right_ne_zero_of_mem_divisorsAntidiagonal {p : ℕℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) :
    p.2 ≠ 0 :=
  (ne_zero_of_mem_divisorsAntidiagonal hp).2

Nonzero Right Component in Divisor Pairs

Informal description

For any pair of natural numbers $(a, b)$ in the divisor pairs finset of a natural number $n$, the second component $b$ is nonzero, i.e., $b \neq 0$.

Nat.divisor_le theorem

{m : ℕ} : n ∈ divisors m → n ≤ m

Full source

theorem divisor_le {m : ℕ} : n ∈ divisors m → n ≤ m := by
  rcases m with - | m
  · simp
  · simp only [mem_divisors, Nat.succ_ne_zero m, and_true, Ne, not_false_iff]
    exact Nat.le_of_dvd (Nat.succ_pos m)

Divisor Bound: $n \mid m \implies n \leq m$

Informal description

For any natural numbers $n$ and $m$, if $n$ is a divisor of $m$ (i.e., $n \in \text{divisors}(m)$), then $n \leq m$.

Nat.divisors_subset_of_dvd theorem

{m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) : divisors m ⊆ divisors n

Full source

theorem divisors_subset_of_dvd {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) : divisorsdivisors m ⊆ divisors n :=
  Finset.subset_iff.2 fun _x hx => Nat.mem_divisors.mpr ⟨(Nat.mem_divisors.mp hx).1.trans h, hzero⟩

Divisor Set Inclusion under Divisibility: $\text{divisors}(m) \subseteq \text{divisors}(n)$ when $m \mid n$ and $n \neq 0$

Informal description

For any nonzero natural number $n$ and any natural number $m$ such that $m$ divides $n$, the set of divisors of $m$ is a subset of the set of divisors of $n$.

Nat.card_divisors_le_self theorem

(n : ℕ) : #n.divisors ≤ n

Full source

theorem card_divisors_le_self (n : ℕ) : #n.divisors ≤ n := calc
  _ ≤ #(Ico 1 (n + 1)) := by
    apply card_le_card
    simp only [divisors, filter_subset]
  _ = n := by rw [card_Ico, add_tsub_cancel_right]

Cardinality of Divisors Set is Bounded by the Number Itself: $|\text{divisors}(n)| \leq n$

Informal description

For any natural number $n$, the number of divisors of $n$ is less than or equal to $n$, i.e., $|\text{divisors}(n)| \leq n$.

Nat.divisors_subset_properDivisors theorem

{m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) : divisors m ⊆ properDivisors n

Full source

theorem divisors_subset_properDivisors {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) :
    divisorsdivisors m ⊆ properDivisors n := by
  apply Finset.subset_iff.2
  intro x hx
  exact
    Nat.mem_properDivisors.2
      ⟨(Nat.mem_divisors.1 hx).1.trans h,
        lt_of_le_of_lt (divisor_le hx)
          (lt_of_le_of_ne (divisor_le (Nat.mem_divisors.2 ⟨h, hzero⟩)) hdiff)⟩

Divisor Subset Property: $\text{divisors}(m) \subseteq \text{properDivisors}(n)$ under $m \mid n \neq 0$ and $m \neq n$

Informal description

For any natural numbers $n$ and $m$ such that $n \neq 0$, $m$ divides $n$, and $m \neq n$, the set of divisors of $m$ is a subset of the proper divisors of $n$. In other words, if $d$ divides $m$, then $d$ is a proper divisor of $n$.

Nat.divisors_filter_dvd_of_dvd theorem

{n m : ℕ} (hn : n ≠ 0) (hm : m ∣ n) : {d ∈ n.divisors | d ∣ m} = m.divisors

Full source

lemma divisors_filter_dvd_of_dvd {n m : ℕ} (hn : n ≠ 0) (hm : m ∣ n) :
    {d ∈ n.divisors | d ∣ m} = m.divisors := by
  ext k
  simp_rw [mem_filter, mem_divisors]
  exact ⟨fun ⟨_, hkm⟩ ↦ ⟨hkm, ne_zero_of_dvd_ne_zero hn hm⟩, fun ⟨hk, _⟩ ↦ ⟨⟨hk.trans hm, hn⟩, hk⟩⟩

Divisor Filtering under Divisibility: $\{d \mid d \mid n \text{ and } d \mid m\} = \text{divisors}(m)$ when $m \mid n \neq 0$

Informal description

For any nonzero natural numbers $n$ and $m$ such that $m$ divides $n$, the set of divisors of $n$ that also divide $m$ is equal to the set of divisors of $m$. In other words: $$\{d \in \text{divisors}(n) \mid d \mid m\} = \text{divisors}(m)$$

Nat.divisors_zero theorem

: divisors 0 = ∅

Full source

@[simp]
theorem divisors_zero : divisors 0 = ∅ := by
  ext
  simp

Empty Divisor Set for Zero

Informal description

The set of divisors of the natural number $0$ is empty, i.e., $\text{divisors}(0) = \emptyset$.

Nat.properDivisors_zero theorem

: properDivisors 0 = ∅

Full source

@[simp]
theorem properDivisors_zero : properDivisors 0 = ∅ := by
  ext
  simp

Empty Proper Divisors Set for Zero

Informal description

The set of proper divisors of the natural number $0$ is empty, i.e., $\text{properDivisors}(0) = \emptyset$.

Nat.nonempty_divisors theorem

: (divisors n).Nonempty ↔ n ≠ 0

Full source

@[simp]
lemma nonempty_divisors : (divisors n).Nonempty ↔ n ≠ 0 :=
  ⟨fun ⟨m, hm⟩ hn ↦ by simp [hn] at hm, fun hn ↦ ⟨1, one_mem_divisors.2 hn⟩⟩

Nonempty Divisor Set Criterion for Nonzero Natural Numbers

Informal description

The set of divisors of a natural number $n$ is nonempty if and only if $n$ is nonzero, i.e., $\text{divisors}(n) \neq \emptyset \leftrightarrow n \neq 0$.

Nat.divisors_eq_empty theorem

: divisors n = ∅ ↔ n = 0

Full source

@[simp]
lemma divisors_eq_empty : divisorsdivisors n = ∅ ↔ n = 0 :=
  not_nonempty_iff_eq_empty.symm.trans nonempty_divisors.not_left

Empty Divisors Set Criterion for Zero

Informal description

For any natural number $n$, the set of divisors $\text{divisors}(n)$ is empty if and only if $n = 0$.

Nat.properDivisors_subset_divisors theorem

: properDivisors n ⊆ divisors n

Full source

theorem properDivisors_subset_divisors : properDivisorsproperDivisors n ⊆ divisors n :=
  filter_subset_filter _ <| Ico_subset_Ico_right n.le_succ

Proper Divisors are Subset of All Divisors

Informal description

For any natural number $n$, the set of proper divisors of $n$ is a subset of the set of all divisors of $n$, i.e., $\text{properDivisors}(n) \subseteq \text{divisors}(n)$.

Nat.divisors_one theorem

: divisors 1 = { 1 }

Full source

@[simp]
theorem divisors_one : divisors 1 = {1} := by
  ext
  simp

Divisors of One: $\text{divisors}(1) = \{1\}$

Informal description

The set of divisors of the natural number $1$ is the singleton set $\{1\}$.

Nat.properDivisors_one theorem

: properDivisors 1 = ∅

Full source

@[simp]
theorem properDivisors_one : properDivisors 1 = ∅ := by rw [properDivisors, Ico_self, filter_empty]

Proper Divisors of One are Empty

Informal description

The set of proper divisors of the natural number $1$ is empty, i.e., $\text{properDivisors}(1) = \emptyset$.

Nat.pos_of_mem_divisors theorem

{m : ℕ} (h : m ∈ n.divisors) : 0 < m

Full source

theorem pos_of_mem_divisors {m : ℕ} (h : m ∈ n.divisors) : 0 < m := by
  cases m
  · rw [mem_divisors, zero_dvd_iff (a := n)] at h
    cases h.2 h.1
  apply Nat.succ_pos

Divisors are Positive: $m \in \text{divisors}(n) \Rightarrow 0 < m$

Informal description

For any natural numbers $n$ and $m$, if $m$ is a divisor of $n$ (i.e., $m \in \text{divisors}(n)$), then $m$ is positive, i.e., $0 < m$.

Nat.pos_of_mem_properDivisors theorem

{m : ℕ} (h : m ∈ n.properDivisors) : 0 < m

Full source

theorem pos_of_mem_properDivisors {m : ℕ} (h : m ∈ n.properDivisors) : 0 < m :=
  pos_of_mem_divisors (properDivisors_subset_divisors h)

Proper Divisors are Positive: $m \in \text{properDivisors}(n) \Rightarrow 0 < m$

Informal description

For any natural numbers $n$ and $m$, if $m$ is a proper divisor of $n$ (i.e., $m \in \text{properDivisors}(n)$), then $m$ is positive, i.e., $0 < m$.

Nat.one_mem_properDivisors_iff_one_lt theorem

: 1 ∈ n.properDivisors ↔ 1 < n

Full source

theorem one_mem_properDivisors_iff_one_lt : 1 ∈ n.properDivisors1 ∈ n.properDivisors ↔ 1 < n := by
  rw [mem_properDivisors, and_iff_right (one_dvd _)]

One is a Proper Divisor if and only if Number is Greater Than One

Informal description

For any natural number $n$, the number $1$ is a proper divisor of $n$ if and only if $1 < n$. In other words, $1 \in \text{properDivisors}(n) \leftrightarrow 1 < n$.

Nat.sup_divisors_id theorem

(n : ℕ) : n.divisors.sup id = n

Full source

@[simp]
lemma sup_divisors_id (n : ℕ) : n.divisors.sup id = n := by
  refine le_antisymm (Finset.sup_le fun _ ↦ divisor_le) ?_
  rcases Decidable.eq_or_ne n 0 with rfl | hn
  · apply zero_le
  · exact Finset.le_sup (f := id) <| mem_divisors_self n hn

Supremum of Divisors Equals the Number Itself

Informal description

For any natural number $n$, the supremum of the set of divisors of $n$ (with respect to the identity function) is equal to $n$ itself, i.e., $\sup(\text{divisors}(n)) = n$.

Nat.one_lt_of_mem_properDivisors theorem

{m n : ℕ} (h : m ∈ n.properDivisors) : 1 < n

Full source

lemma one_lt_of_mem_properDivisors {m n : ℕ} (h : m ∈ n.properDivisors) : 1 < n :=
  lt_of_le_of_lt (pos_of_mem_properDivisors h) (mem_properDivisors.1 h).2

Proper Divisor Implies Number Greater Than One: $m \in \text{properDivisors}(n) \Rightarrow 1 < n$

Informal description

For any natural numbers $m$ and $n$, if $m$ is a proper divisor of $n$ (i.e., $m \in \text{properDivisors}(n)$), then $n$ is greater than $1$, i.e., $1 < n$.

Nat.one_lt_div_of_mem_properDivisors theorem

{m n : ℕ} (h : m ∈ n.properDivisors) : 1 < n / m

Full source

lemma one_lt_div_of_mem_properDivisors {m n : ℕ} (h : m ∈ n.properDivisors) :
    1 < n / m := by
  obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h
  rwa [Nat.lt_div_iff_mul_lt' h_dvd, mul_one]

Quotient Greater Than One for Proper Divisors

Informal description

For any natural numbers $m$ and $n$, if $m$ is a proper divisor of $n$ (i.e., $m \mid n$ and $m < n$), then the quotient $n / m$ is greater than $1$.

Nat.mem_properDivisors_iff_exists theorem

{m n : ℕ} (hn : n ≠ 0) : m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k

Full source

/-- See also `Nat.mem_properDivisors`. -/
lemma mem_properDivisors_iff_exists {m n : ℕ} (hn : n ≠ 0) :
    m ∈ n.properDivisorsm ∈ n.properDivisors ↔ ∃ k > 1, n = m * k := by
  refine ⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩
  · exact (Nat.mul_div_cancel' (mem_properDivisors.mp h).1).symm
  · rintro ⟨k, hk, rfl⟩
    rw [mul_ne_zero_iff] at hn
    exact mem_properDivisors.mpr ⟨⟨k, rfl⟩, lt_mul_of_one_lt_right (Nat.pos_of_ne_zero hn.1) hk⟩

Existence of Multiplier for Proper Divisors: $m \in \text{properDivisors}(n) \leftrightarrow \exists k > 1, n = m \cdot k$

Informal description

For any natural numbers $m$ and $n$ with $n \neq 0$, $m$ is a proper divisor of $n$ if and only if there exists a natural number $k > 1$ such that $n = m \cdot k$.

Nat.nonempty_properDivisors theorem

: n.properDivisors.Nonempty ↔ 1 < n

Full source

@[simp]
lemma nonempty_properDivisors : n.properDivisors.Nonempty ↔ 1 < n :=
  ⟨fun ⟨_m, hm⟩ ↦ one_lt_of_mem_properDivisors hm, fun hn ↦
    ⟨1, one_mem_properDivisors_iff_one_lt.2 hn⟩⟩

Nonempty Proper Divisors if and only if Greater Than One

Informal description

For any natural number $n$, the set of proper divisors of $n$ is nonempty if and only if $n > 1$.

Nat.properDivisors_eq_empty theorem

: n.properDivisors = ∅ ↔ n ≤ 1

Full source

@[simp]
lemma properDivisors_eq_empty : n.properDivisors = ∅ ↔ n ≤ 1 := by
  rw [← not_nonempty_iff_eq_empty, nonempty_properDivisors, not_lt]

Proper Divisors Empty if and only if $n \leq 1$

Informal description

For any natural number $n$, the set of proper divisors of $n$ is empty if and only if $n \leq 1$.

Nat.divisorsAntidiagonal_zero theorem

: divisorsAntidiagonal 0 = ∅

Full source

@[simp]
theorem divisorsAntidiagonal_zero : divisorsAntidiagonal 0 = ∅ := by
  ext
  simp

Empty Divisor Antidiagonal for Zero

Informal description

The set of pairs of natural numbers whose product is 0 is empty, i.e., $\text{divisorsAntidiagonal}(0) = \emptyset$.

Nat.divisorsAntidiagonal_one theorem

: divisorsAntidiagonal 1 = {(1, 1)}

Full source

@[simp]
theorem divisorsAntidiagonal_one : divisorsAntidiagonal 1 = {(1, 1)} := by
  ext
  simp [mul_eq_one, Prod.ext_iff]

Divisor Antidiagonal of 1 is Singleton $(1, 1)$

Informal description

The set of pairs of natural numbers whose product is 1 consists exactly of the single pair $(1, 1)$, i.e., $\text{divisorsAntidiagonal}(1) = \{(1, 1)\}$.

Nat.swap_mem_divisorsAntidiagonal theorem

{x : ℕ × ℕ} : x.swap ∈ divisorsAntidiagonal n ↔ x ∈ divisorsAntidiagonal n

Full source

@[simp high]
theorem swap_mem_divisorsAntidiagonal {x : ℕℕ × ℕ} :
    x.swap ∈ divisorsAntidiagonal nx.swap ∈ divisorsAntidiagonal n ↔ x ∈ divisorsAntidiagonal n := by
  rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]

Swapped Pair Membership in Divisor Antidiagonal Finset

Informal description

For any pair of natural numbers $(a, b)$ and any natural number $n$, the swapped pair $(b, a)$ belongs to the finset of divisor pairs of $n$ if and only if the original pair $(a, b)$ belongs to the finset.

Nat.swap_mem_divisorsAntidiagonal_aux theorem

{x : ℕ × ℕ} : x.snd * x.fst = n ∧ ¬n = 0 ↔ x ∈ divisorsAntidiagonal n

Full source

/-- `Nat.swap_mem_divisorsAntidiagonal` with the LHS in simp normal form. -/
@[deprecated swap_mem_divisorsAntidiagonal (since := "2025-02-17")]
theorem swap_mem_divisorsAntidiagonal_aux {x : ℕℕ × ℕ} :
    x.snd * x.fst = n ∧ ¬n = 0x.snd * x.fst = n ∧ ¬n = 0 ↔ x ∈ divisorsAntidiagonal n := by
  rw [mem_divisorsAntidiagonal, mul_comm]

Characterization of Divisor Pairs via Swapped Product: $(b \times a = n) \land (n \neq 0) \leftrightarrow (a, b) \in \text{divisorsAntidiagonal}(n)$

Informal description

For any pair of natural numbers $(a, b)$ and a natural number $n$, the product $b \times a$ equals $n$ and $n$ is nonzero if and only if $(a, b)$ belongs to the finset of divisor pairs of $n$.

Nat.prodMk_mem_divisorsAntidiag theorem

{x y : ℕ} (hn : n ≠ 0) : (x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n

Full source

lemma prodMk_mem_divisorsAntidiag {x y : ℕ} (hn : n ≠ 0) :
    (x, y)(x, y) ∈ n.divisorsAntidiagonal(x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n := by simp [hn]

Characterization of Divisor Pairs: $(x, y) \in \text{divisorsAntidiagonal}(n) \leftrightarrow x \cdot y = n$ for $n \neq 0$

Informal description

For any natural numbers $x$ and $y$, and for any nonzero natural number $n$, the pair $(x, y)$ belongs to the finset of divisor pairs of $n$ if and only if $x \times y = n$.

Nat.fst_mem_divisors_of_mem_antidiagonal theorem

{x : ℕ × ℕ} (h : x ∈ divisorsAntidiagonal n) : x.fst ∈ divisors n

Full source

theorem fst_mem_divisors_of_mem_antidiagonal {x : ℕℕ × ℕ} (h : x ∈ divisorsAntidiagonal n) :
    x.fst ∈ divisors n := by
  rw [mem_divisorsAntidiagonal] at h
  simp [Dvd.intro _ h.1, h.2]

First Component of Divisor Pair is a Divisor

Informal description

For any pair of natural numbers $(a, b)$ in the divisor antidiagonal of a nonzero natural number $n$ (i.e., $a \times b = n$), the first component $a$ is a divisor of $n$.

Nat.snd_mem_divisors_of_mem_antidiagonal theorem

{x : ℕ × ℕ} (h : x ∈ divisorsAntidiagonal n) : x.snd ∈ divisors n

Full source

theorem snd_mem_divisors_of_mem_antidiagonal {x : ℕℕ × ℕ} (h : x ∈ divisorsAntidiagonal n) :
    x.snd ∈ divisors n := by
  rw [mem_divisorsAntidiagonal] at h
  simp [Dvd.intro_left _ h.1, h.2]

Second Component of Divisor Pair is a Divisor

Informal description

For any pair of natural numbers $(a, b)$ in the divisor pairs finset of $n$ (i.e., $(a, b) \in \text{divisorsAntidiagonal}(n)$), the second component $b$ is a divisor of $n$ (i.e., $b \in \text{divisors}(n)$).

Nat.map_swap_divisorsAntidiagonal theorem

: (divisorsAntidiagonal n).map (Equiv.prodComm _ _).toEmbedding = divisorsAntidiagonal n

Full source

@[simp]
theorem map_swap_divisorsAntidiagonal :
    (divisorsAntidiagonal n).map (Equiv.prodComm _ _).toEmbedding = divisorsAntidiagonal n := by
  rw [← coe_inj, coe_map, Equiv.coe_toEmbedding, Equiv.coe_prodComm,
    Set.image_swap_eq_preimage_swap]
  ext
  exact swap_mem_divisorsAntidiagonal

Invariance of Divisor Pairs Finset under Swap Operation

Informal description

For any natural number $n$, the image of the finset of divisor pairs $(a, b)$ (where $a \times b = n$) under the swap operation $(a, b) \mapsto (b, a)$ is equal to the original finset of divisor pairs. In other words, the map $(a, b) \mapsto (b, a)$ is a bijection on the finset $\text{divisorsAntidiagonal}(n)$.

Nat.image_fst_divisorsAntidiagonal theorem

: (divisorsAntidiagonal n).image Prod.fst = divisors n

Full source

@[simp]
theorem image_fst_divisorsAntidiagonal : (divisorsAntidiagonal n).image Prod.fst = divisors n := by
  ext
  simp [Dvd.dvd, @eq_comm _ n (_ * _)]

First Projection of Divisor Pairs Equals Divisors

Informal description

For any natural number $n$, the image of the first projection on the finset of divisor pairs $(a, b)$ such that $a \times b = n$ is equal to the finset of divisors of $n$. In other words, $\{a \mid \exists b, (a, b) \in \text{divisorsAntidiagonal}(n)\} = \text{divisors}(n)$.

Nat.image_snd_divisorsAntidiagonal theorem

: (divisorsAntidiagonal n).image Prod.snd = divisors n

Full source

@[simp]
theorem image_snd_divisorsAntidiagonal : (divisorsAntidiagonal n).image Prod.snd = divisors n := by
  rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]
  exact image_fst_divisorsAntidiagonal

Second Projection of Divisor Pairs Equals Divisors

Informal description

For any natural number $n$, the image of the second projection on the finset of divisor pairs $(a, b)$ such that $a \times b = n$ is equal to the finset of divisors of $n$. In other words, $\{b \mid \exists a, (a, b) \in \text{divisorsAntidiagonal}(n)\} = \text{divisors}(n)$.

Nat.map_div_right_divisors theorem

: n.divisors.map ⟨fun d => (d, n / d), fun _ _ => congr_arg Prod.fst⟩ = n.divisorsAntidiagonal

Full source

theorem map_div_right_divisors :
    n.divisors.map ⟨fun d => (d, n / d), fun _ _ => congr_arg Prod.fst⟩ =
      n.divisorsAntidiagonal := by
  ext ⟨d, nd⟩
  simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors,
    Prod.ext_iff, exists_prop, and_left_comm, exists_eq_left]
  constructor
  · rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩
    rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]
    exact ⟨rfl, hn⟩
  · rintro ⟨rfl, hn⟩
    exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩

Bijection between Divisors and Divisor Pairs via Division

Informal description

For any natural number $n$, the map that sends each divisor $d$ of $n$ to the pair $(d, n/d)$ is a bijection between the set of divisors of $n$ and the set of pairs $(a,b)$ such that $a \times b = n$. Formally, the image of the map $\lambda d \mapsto (d, n/d)$ on the finset of divisors of $n$ is equal to the finset of divisor pairs of $n$.

Nat.map_div_left_divisors theorem

: n.divisors.map ⟨fun d => (n / d, d), fun _ _ => congr_arg Prod.snd⟩ = n.divisorsAntidiagonal

Full source

theorem map_div_left_divisors :
    n.divisors.map ⟨fun d => (n / d, d), fun _ _ => congr_arg Prod.snd⟩ =
      n.divisorsAntidiagonal := by
  apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding
  ext
  rw [map_swap_divisorsAntidiagonal, ← map_div_right_divisors, Finset.map_map]
  simp

Bijection between Divisors and Divisor Pairs via Division (Reversed)

Informal description

For any natural number $n$, the map that sends each divisor $d$ of $n$ to the pair $(n/d, d)$ is a bijection between the set of divisors of $n$ and the set of pairs $(a,b)$ such that $a \times b = n$. Formally, the image of the map $\lambda d \mapsto (n/d, d)$ on the finset of divisors of $n$ is equal to the finset of divisor pairs of $n$.

Nat.sum_divisors_eq_sum_properDivisors_add_self theorem

: ∑ i ∈ divisors n, i = (∑ i ∈ properDivisors n, i) + n

Full source

theorem sum_divisors_eq_sum_properDivisors_add_self :
    ∑ i ∈ divisors n, i = (∑ i ∈ properDivisors n, i) + n := by
  rcases Decidable.eq_or_ne n 0 with (rfl | hn)
  · simp
  · rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]

Sum of Divisors Equals Sum of Proper Divisors Plus Number Itself

Informal description

For any natural number $n$, the sum of all divisors of $n$ equals the sum of the proper divisors of $n$ plus $n$ itself. That is, \[ \sum_{d \in \text{divisors}(n)} d = \left(\sum_{d \in \text{properDivisors}(n)} d\right) + n. \]

Nat.Perfect definition

(n : ℕ) : Prop

Full source

/-- `n : ℕ` is perfect if and only the sum of the proper divisors of `n` is `n` and `n`
  is positive. -/
def Perfect (n : ℕ) : Prop :=
  ∑ i ∈ properDivisors n, i∑ i ∈ properDivisors n, i = n ∧ 0 < n

Perfect number

Informal description

A natural number $ n $ is called *perfect* if it is positive and the sum of its proper divisors equals $ n $. Here, the proper divisors of $ n $ are all natural numbers $ d $ such that $ 1 \leq d < n $ and $ d $ divides $ n $.

Nat.perfect_iff_sum_properDivisors theorem

(h : 0 < n) : Perfect n ↔ ∑ i ∈ properDivisors n, i = n

Full source

theorem perfect_iff_sum_properDivisors (h : 0 < n) : PerfectPerfect n ↔ ∑ i ∈ properDivisors n, i = n :=
  and_iff_left h

Characterization of Perfect Numbers via Proper Divisors Sum

Informal description

For a positive natural number $n$, $n$ is perfect if and only if the sum of its proper divisors equals $n$. That is, \[ \text{Perfect}(n) \leftrightarrow \sum_{d \in \text{properDivisors}(n)} d = n. \]

Nat.perfect_iff_sum_divisors_eq_two_mul theorem

(h : 0 < n) : Perfect n ↔ ∑ i ∈ divisors n, i = 2 * n

Full source

theorem perfect_iff_sum_divisors_eq_two_mul (h : 0 < n) :
    PerfectPerfect n ↔ ∑ i ∈ divisors n, i = 2 * n := by
  rw [perfect_iff_sum_properDivisors h, sum_divisors_eq_sum_properDivisors_add_self, two_mul]
  constructor <;> intro h
  · rw [h]
  · apply add_right_cancel h

Characterization of Perfect Numbers via Sum of Divisors: $\sum d = 2n$

Informal description

For any positive natural number $n$, $n$ is perfect if and only if the sum of all its divisors equals twice $n$. That is, \[ \text{Perfect}(n) \leftrightarrow \sum_{d \in \text{divisors}(n)} d = 2n. \]

Nat.mem_divisors_prime_pow theorem

{p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} : x ∈ divisors (p ^ k) ↔ ∃ j ≤ k, x = p ^ j

Full source

theorem mem_divisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} :
    x ∈ divisors (p ^ k)x ∈ divisors (p ^ k) ↔ ∃ j ≤ k, x = p ^ j := by
  rw [mem_divisors, Nat.dvd_prime_pow pp, and_iff_left (ne_of_gt (pow_pos pp.pos k))]

Characterization of Divisors of Prime Powers: $x \mid p^k \leftrightarrow x = p^j$ for some $j \leq k$

Informal description

For a prime natural number $p$ and natural numbers $k$ and $x$, $x$ belongs to the set of divisors of $p^k$ if and only if there exists a natural number $j \leq k$ such that $x = p^j$. In other words: \[ x \in \text{divisors}(p^k) \leftrightarrow \exists j \leq k, x = p^j. \]

Nat.Prime.divisors theorem

{p : ℕ} (pp : p.Prime) : divisors p = { 1, p }

Full source

theorem Prime.divisors {p : ℕ} (pp : p.Prime) : divisors p = {1, p} := by
  ext
  rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]

Divisors of a Prime Number

Informal description

For any prime natural number $p$, the set of divisors of $p$ is exactly $\{1, p\}$.

Nat.Prime.properDivisors theorem

{p : ℕ} (pp : p.Prime) : properDivisors p = { 1 }

Full source

theorem Prime.properDivisors {p : ℕ} (pp : p.Prime) : properDivisors p = {1} := by
  rw [← erase_insert properDivisors.not_self_mem, insert_self_properDivisors pp.ne_zero,
    pp.divisors, pair_comm, erase_insert fun con => pp.ne_one (mem_singleton.1 con)]

Proper Divisors of a Prime Number

Informal description

For any prime natural number $p$, the set of proper divisors of $p$ is exactly $\{1\}$.

Nat.divisors_prime_pow theorem

 {p : ℕ} (pp : p.Prime) (k : ℕ) :
  divisors (p ^ k) = (Finset.range (k + 1)).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩

Full source

theorem divisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
    divisors (p ^ k) = (Finset.range (k + 1)).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩ := by
  ext a
  rw [mem_divisors_prime_pow pp]
  simp [Nat.lt_succ, eq_comm]

Divisors of Prime Powers: $\text{divisors}(p^k) = \{p^j \mid j \leq k\}$

Informal description

For any prime natural number $p$ and natural number $k$, the set of divisors of $p^k$ is equal to the image of the function $j \mapsto p^j$ applied to the finite set $\{0, \dots, k\}$. That is: \[ \text{divisors}(p^k) = \{p^j \mid 0 \leq j \leq k\}. \]

Nat.divisors_injective theorem

: Function.Injective divisors

Full source

theorem divisors_injective : Function.Injective divisors :=
  Function.LeftInverse.injective sup_divisors_id

Injectivity of the Divisor Set Function

Informal description

The function mapping a natural number $n$ to its set of divisors $\text{divisors}(n)$ is injective. That is, for any natural numbers $a$ and $b$, if $\text{divisors}(a) = \text{divisors}(b)$, then $a = b$.

Nat.divisors_inj theorem

{a b : ℕ} : a.divisors = b.divisors ↔ a = b

Full source

@[simp]
theorem divisors_inj {a b : ℕ} : a.divisors = b.divisors ↔ a = b :=
  divisors_injective.eq_iff

Divisor Set Equality Characterizes Natural Number Equality

Informal description

For any natural numbers $a$ and $b$, the set of divisors of $a$ is equal to the set of divisors of $b$ if and only if $a = b$.

Nat.sum_properDivisors_dvd theorem

(h : (∑ x ∈ n.properDivisors, x) ∣ n) : ∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n

Full source

theorem sum_properDivisors_dvd (h : (∑ x ∈ n.properDivisors, x) ∣ n) :
    ∑ x ∈ n.properDivisors, x∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n := by
  rcases n with - | n
  · simp
  · rcases n with - | n
    · simp at h
    · rw [or_iff_not_imp_right]
      intro ne_n
      have hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ :=
        lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n
      symm
      rw [← mem_singleton, eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
        (mem_properDivisors.2 ⟨h, hlt⟩)) (sum_singleton _ _), mem_properDivisors]
      exact ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩

Sum of Proper Divisors Divides Implies Sum is 1 or n

Informal description

For any natural number $n$, if the sum of its proper divisors divides $n$, then this sum is either $1$ or $n$. In other words, if $\sum_{d \in \text{properDivisors}(n)} d$ divides $n$, then $\sum_{d \in \text{properDivisors}(n)} d = 1$ or $\sum_{d \in \text{properDivisors}(n)} d = n$.

Nat.Prime.prod_properDivisors theorem

{α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : p.Prime) : ∏ x ∈ p.properDivisors, f x = f 1

Full source

@[to_additive (attr := simp)]
theorem Prime.prod_properDivisors {α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : p.Prime) :
    ∏ x ∈ p.properDivisors, f x = f 1 := by simp [h.properDivisors]

Product over Proper Divisors of a Prime Number Equals $f(1)$

Informal description

For any prime natural number $p$ and any commutative monoid $\alpha$ with a function $f : \mathbb{N} \to \alpha$, the product of $f$ over the proper divisors of $p$ is equal to $f(1)$. In other words, $\prod_{x \in \text{properDivisors}(p)} f(x) = f(1)$.

Nat.Prime.prod_divisors theorem

{α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : p.Prime) : ∏ x ∈ p.divisors, f x = f p * f 1

Full source

@[to_additive (attr := simp)]
theorem Prime.prod_divisors {α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : p.Prime) :
    ∏ x ∈ p.divisors, f x = f p * f 1 := by
  rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]

Product over Divisors of a Prime Number Equals $f(p) \cdot f(1)$

Informal description

For any prime natural number $p$ and any commutative monoid $\alpha$ with a function $f : \mathbb{N} \to \alpha$, the product of $f$ over all divisors of $p$ is equal to $f(p) \cdot f(1)$. In other words, $$ \prod_{x \in \text{divisors}(p)} f(x) = f(p) \cdot f(1). $$

Nat.properDivisors_eq_singleton_one_iff_prime theorem

: n.properDivisors = { 1 } ↔ n.Prime

Full source

theorem properDivisors_eq_singleton_one_iff_prime : n.properDivisors = {1} ↔ n.Prime := by
  refine ⟨?_, ?_⟩
  · intro h
    refine Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩
    · match n with
      | 0 => contradiction
      | 1 => contradiction
      | Nat.succ (Nat.succ n) => simp [succ_le_succ]
    · rw [← mem_singleton, ← h, mem_properDivisors]
      have := Nat.le_of_dvd ?_ hdvd
      · simpa [hdvd, this] using (le_iff_eq_or_lt.mp this).symm
      · by_contra!
        simp only [nonpos_iff_eq_zero.mp this, this] at h
        contradiction
  · exact fun h => Prime.properDivisors h

Characterization of Primes via Proper Divisors: $\text{properDivisors}(n) = \{1\} \leftrightarrow \text{Prime}(n)$

Informal description

For a natural number $n$, the set of proper divisors of $n$ is exactly $\{1\}$ if and only if $n$ is prime.

Nat.sum_properDivisors_eq_one_iff_prime theorem

: ∑ x ∈ n.properDivisors, x = 1 ↔ n.Prime

Full source

theorem sum_properDivisors_eq_one_iff_prime : ∑ x ∈ n.properDivisors, x∑ x ∈ n.properDivisors, x = 1 ↔ n.Prime := by
  rcases n with - | n
  · simp [Nat.not_prime_zero]
  · cases n
    · simp [Nat.not_prime_one]
    · rw [← properDivisors_eq_singleton_one_iff_prime]
      refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
      rw [@eq_comm (Finset ℕ) _ _]
      apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2
            (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

Sum of Proper Divisors Equals One if and only if Prime

Informal description

For a natural number $n$, the sum of its proper divisors equals $1$ if and only if $n$ is prime.

Nat.mem_properDivisors_prime_pow theorem

{p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} : x ∈ properDivisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j

Full source

theorem mem_properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} :
    x ∈ properDivisors (p ^ k)x ∈ properDivisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j := by
  rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]
  simp only [exists_prop, and_assoc]
  apply exists_congr
  intro a
  constructor <;> intro h
  · rcases h with ⟨_h_left, rfl, h_right⟩
    rw [Nat.pow_lt_pow_iff_right pp.one_lt] at h_right
    exact ⟨h_right, rfl⟩
  · rcases h with ⟨h_left, rfl⟩
    rw [Nat.pow_lt_pow_iff_right pp.one_lt]
    simp [h_left, le_of_lt]

Characterization of Proper Divisors of Prime Powers: $x \in \text{properDivisors}(p^k) \leftrightarrow \exists j < k, x = p^j$

Informal description

Let $p$ be a prime natural number and $k$ a natural number. For any natural number $x$, $x$ is a proper divisor of $p^k$ if and only if there exists a natural number $j < k$ such that $x = p^j$.

Nat.properDivisors_prime_pow theorem

 {p : ℕ} (pp : p.Prime) (k : ℕ) :
  properDivisors (p ^ k) = (Finset.range k).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩

Full source

theorem properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
    properDivisors (p ^ k) = (Finset.range k).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩ := by
  ext a
  simp only [mem_properDivisors, Nat.isUnit_iff, mem_map, mem_range, Function.Embedding.coeFn_mk,
    pow_eq]
  have := mem_properDivisors_prime_pow pp k (x := a)
  rw [mem_properDivisors] at this
  rw [this]
  refine ⟨?_, ?_⟩
  · intro h; rcases h with ⟨j, hj, hap⟩; use j; tauto
  · tauto

Proper Divisors of Prime Powers: $\text{properDivisors}(p^k) = \{p^j \mid 0 \leq j < k\}$

Informal description

Let $p$ be a prime natural number and $k$ a natural number. The set of proper divisors of $p^k$ is equal to the image of the range $\{0, \dots, k-1\}$ under the injective function $j \mapsto p^j$. In other words, \[ \text{properDivisors}(p^k) = \{p^j \mid 0 \leq j < k\}. \]

Nat.prod_properDivisors_prime_pow theorem

 {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : p.Prime) :
  (∏ x ∈ (p ^ k).properDivisors, f x) = ∏ x ∈ range k, f (p ^ x)

Full source

@[to_additive (attr := simp)]
theorem prod_properDivisors_prime_pow {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α}
    (h : p.Prime) : (∏ x ∈ (p ^ k).properDivisors, f x) = ∏ x ∈ range k, f (p ^ x) := by
  simp [h, properDivisors_prime_pow]

Product over Proper Divisors of a Prime Power: $\prod_{x \in \text{properDivisors}(p^k)} f(x) = \prod_{x=0}^{k-1} f(p^x)$

Informal description

Let $\alpha$ be a commutative monoid, $p$ a prime natural number, $k$ a natural number, and $f \colon \mathbb{N} \to \alpha$ a function. The product of $f(x)$ over all proper divisors $x$ of $p^k$ is equal to the product of $f(p^x)$ over all $x$ in the range $\{0, \dots, k-1\}$. In other words, \[ \prod_{x \in \text{properDivisors}(p^k)} f(x) = \prod_{x=0}^{k-1} f(p^x). \]

Nat.prod_divisors_prime_pow theorem

 {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : p.Prime) :
  (∏ x ∈ (p ^ k).divisors, f x) = ∏ x ∈ range (k + 1), f (p ^ x)

Full source

@[to_additive (attr := simp) sum_divisors_prime_pow]
theorem prod_divisors_prime_pow {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : p.Prime) :
    (∏ x ∈ (p ^ k).divisors, f x) = ∏ x ∈ range (k + 1), f (p ^ x) := by
  simp [h, divisors_prime_pow]

Product over Divisors of a Prime Power: $\prod_{d \mid p^k} f(d) = \prod_{x=0}^k f(p^x)$

Informal description

Let $\alpha$ be a commutative monoid, $p$ a prime natural number, $k$ a natural number, and $f \colon \mathbb{N} \to \alpha$ a function. Then the product of $f(x)$ over all divisors $x$ of $p^k$ is equal to the product of $f(p^x)$ over all $x$ in the range $\{0, \dots, k\}$. In other words, \[ \prod_{x \in \text{divisors}(p^k)} f(x) = \prod_{x=0}^k f(p^x). \]

Nat.prod_divisorsAntidiagonal theorem

 {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
  ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)

Full source

@[to_additive]
theorem prod_divisorsAntidiagonal {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
    ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i) := by
  rw [← map_div_right_divisors, Finset.prod_map]
  rfl

Product over Divisor Pairs Equals Product over Divisors with Complementary Factor

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \times \mathbb{N} \to M$ be a function. For any natural number $n$, the product of $f(a,b)$ over all pairs $(a,b)$ in the divisor antidiagonal of $n$ (i.e., pairs where $a \times b = n$) is equal to the product of $f(d, n/d)$ over all divisors $d$ of $n$.

Nat.prod_divisorsAntidiagonal' theorem

 {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
  ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i

Full source

@[to_additive]
theorem prod_divisorsAntidiagonal' {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
    ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i := by
  rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]
  exact prod_divisorsAntidiagonal fun i j => f j i

Product over Divisor Pairs Equals Product over Divisors with Swapped Complementary Factor

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \times \mathbb{N} \to M$ be a function. For any natural number $n$, the product of $f(a,b)$ over all pairs $(a,b)$ in the divisor antidiagonal of $n$ (i.e., pairs where $a \times b = n$) is equal to the product of $f(n/d, d)$ over all divisors $d$ of $n$.

Nat.primeFactors_eq_to_filter_divisors_prime theorem

(n : ℕ) : n.primeFactors = {p ∈ divisors n | p.Prime}

Full source

/-- The factors of `n` are the prime divisors -/
theorem primeFactors_eq_to_filter_divisors_prime (n : ℕ) :
    n.primeFactors = {p ∈ divisors n | p.Prime} := by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  · ext q
    simpa [hn, hn.ne', mem_primeFactorsList] using and_comm

Prime Factors as Prime Divisors

Informal description

For any natural number $n$, the set of prime factors of $n$ is equal to the subset of divisors of $n$ that are prime numbers. In other words, $\mathrm{primeFactors}(n) = \{p \in \mathrm{divisors}(n) \mid p \text{ is prime}\}$.

Nat.primeFactors_filter_dvd_of_dvd theorem

{m n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n) : {p ∈ n.primeFactors | p ∣ m} = m.primeFactors

Full source

lemma primeFactors_filter_dvd_of_dvd {m n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n) :
    {p ∈ n.primeFactors | p ∣ m} = m.primeFactors := by
  simp_rw [primeFactors_eq_to_filter_divisors_prime, filter_comm,
    divisors_filter_dvd_of_dvd hn hmn]

Prime Factor Filtering under Divisibility: $\{p \mid p \mid n \text{ and } p \mid m\} = \mathrm{primeFactors}(m)$ when $m \mid n \neq 0$

Informal description

For any nonzero natural numbers $n$ and $m$ such that $m$ divides $n$, the set of prime factors of $n$ that also divide $m$ is equal to the set of prime factors of $m$. In other words: $$\{p \in \mathrm{primeFactors}(n) \mid p \mid m\} = \mathrm{primeFactors}(m)$$

Nat.image_div_divisors_eq_divisors theorem

(n : ℕ) : image (fun x : ℕ => n / x) n.divisors = n.divisors

Full source

@[simp]
theorem image_div_divisors_eq_divisors (n : ℕ) :
    image (fun x : ℕ => n / x) n.divisors = n.divisors := by
  by_cases hn : n = 0
  · simp [hn]
  ext a
  constructor
  · rw [mem_image]
    rintro ⟨x, hx1, hx2⟩
    rw [mem_divisors] at *
    refine ⟨?_, hn⟩
    rw [← hx2]
    exact div_dvd_of_dvd hx1.1
  · rw [mem_divisors, mem_image]
    rintro ⟨h1, -⟩
    exact ⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩

Divisors are Closed under Division Inversion: $\{n/d \mid d \mid n\} = \text{divisors}(n)$

Informal description

For any natural number $n$, the image of the function $x \mapsto n/x$ applied to the set of divisors of $n$ is equal to the set of divisors of $n$ itself. In other words: $$\left\{\frac{n}{d} \mid d \in \text{divisors}(n)\right\} = \text{divisors}(n)$$

Nat.prod_div_divisors theorem

{α : Type*} [CommMonoid α] (n : ℕ) (f : ℕ → α) : (∏ d ∈ n.divisors, f (n / d)) = n.divisors.prod f

Full source

@[to_additive sum_div_divisors]
theorem prod_div_divisors {α : Type*} [CommMonoid α] (n : ℕ) (f : ℕ → α) :
    (∏ d ∈ n.divisors, f (n / d)) = n.divisors.prod f := by
  by_cases hn : n = 0; · simp [hn]
  rw [← prod_image]
  · exact prod_congr (image_div_divisors_eq_divisors n) (by simp)
  · intro x hx y hy h
    rw [mem_divisors] at hx hy
    exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

Product over Divisors Invariance under Division Inversion: $\prod_{d \mid n} f(n/d) = \prod_{d \mid n} f(d)$

Informal description

Let $\alpha$ be a commutative monoid and $n$ be a natural number. For any function $f \colon \mathbb{N} \to \alpha$, the product of $f(n/d)$ over all divisors $d$ of $n$ equals the product of $f(d)$ over all divisors $d$ of $n$. In other words: $$\prod_{d \in \text{divisors}(n)} f\left(\frac{n}{d}\right) = \prod_{d \in \text{divisors}(n)} f(d)$$

Nat.disjoint_divisors_filter_isPrimePow theorem

{a b : ℕ} (hab : a.Coprime b) : Disjoint (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow)

Full source

theorem disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.Coprime b) :
    Disjoint (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow) := by
  simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
  rintro n han _ha hn hbn _hb -
  exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)

Disjointness of Prime Power Divisors for Coprime Numbers

Informal description

For any two coprime natural numbers $a$ and $b$, the sets of prime power divisors of $a$ and $b$ are disjoint. In other words, if $\gcd(a, b) = 1$, then $\{d \in \text{divisors}(a) \mid \text{IsPrimePow}(d)\} \cap \{d \in \text{divisors}(b) \mid \text{IsPrimePow}(d)\} = \emptyset$.

Int.divisorsAntidiag definition

: (z : ℤ) → Finset (ℤ × ℤ)

Full source

/-- Pairs of divisors of an integer as a finset.

`z.divisorsAntidiag` is the finset of pairs `(a, b) : ℤ × ℤ` such that `a * b = z`.
By convention, we set `Int.divisorsAntidiag 0 = ∅`.

O(|z|). Computed from `Nat.divisorsAntidiagonal`. -/
def divisorsAntidiag : (z : ℤ) → Finset (ℤℤ × ℤ)
  | (n : ℕ) =>
    let s : Finset (ℕ × ℕ) := n.divisorsAntidiagonal
    (s.map <| .prodMap natCast natCast).disjUnion (s.map <| .prodMap negNatCast negNatCast) <| by
      simp +contextual [s, disjoint_left, eq_comm]
  | negSucc n =>
    let s : Finset (ℕ × ℕ) := (n + 1).divisorsAntidiagonal
    (s.map <| .prodMap natCast negNatCast).disjUnion (s.map <| .prodMap negNatCast natCast) <| by
      simp +contextual [s, disjoint_left, eq_comm, forall_swap (α := _ * _ = _)]

Finset of integer divisor pairs

Informal description

For an integer $ z $, the finset `Int.divisorsAntidiag z` consists of all pairs $(a, b)$ of integers such that $a \times b = z$. By convention, this finset is empty when $z = 0$. The computation is based on the corresponding finset of natural numbers via `Nat.divisorsAntidiagonal`.

Int.mem_divisorsAntidiag theorem

: ∀ {z} {xy : ℤ × ℤ}, xy ∈ divisorsAntidiag z ↔ xy.fst * xy.snd = z ∧ z ≠ 0

Full source

@[simp]
lemma mem_divisorsAntidiag :
    ∀ {z} {xy : ℤℤ × ℤ}, xy ∈ divisorsAntidiag zxy ∈ divisorsAntidiag z ↔ xy.fst * xy.snd = z ∧ z ≠ 0
  | (n : ℕ), ((x : ℕ), (y : ℕ)) => by
    simp [divisorsAntidiag]
    norm_cast
    simp +contextual [eq_comm]
  | (n : ℕ), (negSucc x, negSucc y) => by
    simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
    norm_cast
    simp +contextual [eq_comm]
  | (n : ℕ), ((x : ℕ), negSucc y) => by
    simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
    norm_cast
    aesop
  | (n : ℕ), (negSucc x, (y : ℕ)) => by
    suffices (∃ a, (n = a * y ∧ ¬n = 0) ∧ (a:ℤ) = -1 + -↑x) ↔ (n:ℤ) = (-1 + -↑x) * ↑y ∧ ¬n = 0 by
      simpa [divisorsAntidiag, eq_comm, negSucc_eq]
    simp only [← Int.neg_add, Int.add_comm 1, Int.neg_mul, Int.add_mul]
    norm_cast
    match n with
    | 0 => simp
    | n + 1 => simp
  | .negSucc n, ((x : ℕ), (y : ℕ)) => by
    simp [divisorsAntidiag]
    norm_cast
  | .negSucc n, (negSucc x, negSucc y) => by
    simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
    norm_cast
    simp +contextual [eq_comm]
  | .negSucc n, ((x : ℕ), negSucc y) => by
    simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
    norm_cast
    aesop
  | .negSucc n, (negSucc x, (y : ℕ)) => by
    simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
    norm_cast
    simp +contextual [eq_comm]

Characterization of Integer Divisor Pairs: $(x, y) \in \text{divisorsAntidiag}(z) \leftrightarrow x \times y = z \land z \neq 0$

Informal description

For any integer $z$ and any pair of integers $(x, y)$, the pair $(x, y)$ belongs to the finset of divisor pairs of $z$ if and only if $x \times y = z$ and $z \neq 0$.

Int.divisorsAntidiag_zero theorem

: divisorsAntidiag 0 = ∅

Full source

@[simp] lemma divisorsAntidiag_zero : divisorsAntidiag 0 = ∅ := rfl

Empty Divisor Antidiagonal for Zero

Informal description

The set of integer pairs $(a, b)$ such that $a \times b = 0$ is empty, i.e., $\text{divisorsAntidiag}(0) = \emptyset$.

Int.divisorsAntidiagonal_one theorem

: Int.divisorsAntidiag 1 = {(1, 1), (-1, -1)}

Full source

@[simp]
theorem divisorsAntidiagonal_one :
    Int.divisorsAntidiag 1 = {(1, 1), (-1, -1)} :=
  rfl

Integer divisor pairs for 1: $\{(1, 1), (-1, -1)\}$

Informal description

The set of integer pairs $(a, b)$ such that $a \times b = 1$ is exactly $\{(1, 1), (-1, -1)\}$.

Int.divisorsAntidiagonal_two theorem

: Int.divisorsAntidiag 2 = {(1, 2), (2, 1), (-1, -2), (-2, -1)}

Full source

@[simp]
theorem divisorsAntidiagonal_two :
    Int.divisorsAntidiag 2 = {(1, 2), (2, 1), (-1, -2), (-2, -1)} :=
  rfl

Integer divisor pairs for 2: $\{(1, 2), (2, 1), (-1, -2), (-2, -1)\}$

Informal description

The set of integer pairs $(a, b)$ such that $a \times b = 2$ is precisely $\{(1, 2), (2, 1), (-1, -2), (-2, -1)\}$.

Int.divisorsAntidiagonal_three theorem

: Int.divisorsAntidiag 3 = {(1, 3), (3, 1), (-1, -3), (-3, -1)}

Full source

@[simp]
theorem divisorsAntidiagonal_three :
    Int.divisorsAntidiag 3 = {(1, 3), (3, 1), (-1, -3), (-3, -1)} :=
  rfl

Integer divisor pairs of 3

Informal description

The set of integer pairs $(x, y)$ such that $x \times y = 3$ is equal to $\{(1, 3), (3, 1), (-1, -3), (-3, -1)\}$.

Int.divisorsAntidiagonal_four theorem

: Int.divisorsAntidiag 4 = {(1, 4), (2, 2), (4, 1), (-1, -4), (-2, -2), (-4, -1)}

Full source

@[simp]
theorem divisorsAntidiagonal_four :
    Int.divisorsAntidiag 4 = {(1, 4), (2, 2), (4, 1), (-1, -4), (-2, -2), (-4, -1)} :=
  rfl

Integer Divisor Pairs of 4

Informal description

The set of integer pairs $(a, b)$ such that $a \times b = 4$ is given by $\{(1, 4), (2, 2), (4, 1), (-1, -4), (-2, -2), (-4, -1)\}$.

Int.prodMk_mem_divisorsAntidiag theorem

(hz : z ≠ 0) : (x, y) ∈ z.divisorsAntidiag ↔ x * y = z

Full source

lemma prodMk_mem_divisorsAntidiag (hz : z ≠ 0) : (x, y)(x, y) ∈ z.divisorsAntidiag(x, y) ∈ z.divisorsAntidiag ↔ x * y = z := by
  simp [hz]

Characterization of Integer Divisor Pairs: $(x,y) \in \text{divisorsAntidiag}(z) \leftrightarrow x \times y = z$ for $z \neq 0$

Informal description

For any nonzero integer $z$, a pair of integers $(x, y)$ belongs to the finset of divisor pairs of $z$ if and only if their product equals $z$, i.e., $x \times y = z$.

Int.swap_mem_divisorsAntidiag theorem

: xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Full source

@[simp high]
lemma swap_mem_divisorsAntidiag : xy.swap ∈ z.divisorsAntidiagxy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag := by
  simp [mul_comm]

Symmetry of Divisor Pairs: $(y, x) \in \text{divisorsAntidiag}(z) \leftrightarrow (x, y) \in \text{divisorsAntidiag}(z)$

Informal description

For any integer $z$ and any pair of integers $(x, y)$, the swapped pair $(y, x)$ belongs to the finset of divisor pairs of $z$ if and only if the original pair $(x, y)$ belongs to the finset. In other words, $(y, x) \in \text{divisorsAntidiag}(z) \leftrightarrow (x, y) \in \text{divisorsAntidiag}(z)$.

Int.neg_mem_divisorsAntidiag theorem

: -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Full source

lemma neg_mem_divisorsAntidiag : -xy ∈ z.divisorsAntidiag-xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag := by simp

Negation Invariance of Divisor Pairs: $(-x, -y) \in \text{divisorsAntidiag}(z) \leftrightarrow (x, y) \in \text{divisorsAntidiag}(z)$

Informal description

For any integer $z$ and any pair of integers $(x, y)$, the pair $(-x, -y)$ belongs to the finset of divisor pairs of $z$ if and only if the original pair $(x, y)$ belongs to the finset. In other words, $(-x, -y) \in \text{divisorsAntidiag}(z) \leftrightarrow (x, y) \in \text{divisorsAntidiag}(z)$.

Int.map_prodComm_divisorsAntidiag theorem

: z.divisorsAntidiag.map (Equiv.prodComm _ _).toEmbedding = z.divisorsAntidiag

Full source

@[simp]
lemma map_prodComm_divisorsAntidiag :
    z.divisorsAntidiag.map (Equiv.prodComm _ _).toEmbedding = z.divisorsAntidiag := by
  ext; simp [mem_divisorsAntidiag, mul_comm]

Invariance of Divisor Pairs under Swap: $\text{divisorsAntidiag}(z).map (x, y) \mapsto (y, x) = \text{divisorsAntidiag}(z)$

Informal description

For any integer $z$, the image of the finset of divisor pairs $\text{divisorsAntidiag}(z)$ under the swap equivalence $(x, y) \mapsto (y, x)$ is equal to $\text{divisorsAntidiag}(z)$ itself. In other words, mapping each pair $(x, y)$ in $\text{divisorsAntidiag}(z)$ to $(y, x)$ preserves the finset.

Int.map_neg_divisorsAntidiag theorem

: z.divisorsAntidiag.map (Equiv.neg _).toEmbedding = z.divisorsAntidiag

Full source

@[simp]
lemma map_neg_divisorsAntidiag :
    z.divisorsAntidiag.map (Equiv.neg _).toEmbedding = z.divisorsAntidiag := by
  ext; simp [mem_divisorsAntidiag, mul_comm]

Invariance of Divisor Pairs under Negation

Informal description

For any integer $z$, the image of the finset of divisor pairs $(a, b)$ under the negation map $(a, b) \mapsto (-a, -b)$ is equal to the original finset of divisor pairs, i.e., $\{(-a, -b) \mid (a, b) \in \text{divisorsAntidiag}(z)\} = \text{divisorsAntidiag}(z)$.

Int.divisorsAntidiag_neg theorem

: (-z).divisorsAntidiag = z.divisorsAntidiag.map (.prodMap (.refl _) (Equiv.neg _).toEmbedding)

Full source

lemma divisorsAntidiag_neg :
    (-z).divisorsAntidiag =
      z.divisorsAntidiag.map (.prodMap (.refl _) (Equiv.neg _).toEmbedding) := by
  ext; simp [mem_divisorsAntidiag, Prod.ext_iff, neg_eq_iff_eq_neg]

Negation of Integer Divisor Pairs: $(-z).divisorsAntidiag = \{(x, -y) \mid (x, y) \in z.divisorsAntidiag\}$

Informal description

For any integer $z$, the set of pairs $(x, y)$ such that $x \cdot y = -z$ is equal to the set of pairs $(x, -y)$ where $(x, y)$ satisfies $x \cdot y = z$.

Int.divisorsAntidiag_natCast theorem

 (n : ℕ) :
  divisorsAntidiag n =
    (n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion
      (n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by simp +contextual [disjoint_left, eq_comm])

Full source

lemma divisorsAntidiag_natCast (n : ℕ) :
    divisorsAntidiag n =
      (n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion
        (n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by
          simp +contextual [disjoint_left, eq_comm]) := rfl

Characterization of Integer Divisor Pairs for Natural Numbers

Informal description

For any natural number $n$, the set of integer pairs $(a,b)$ such that $a \times b = n$ is equal to the disjoint union of: 1. The image of the set of natural number pairs $(x,y)$ with $x \times y = n$ under the map $(x,y) \mapsto (x,y)$, and 2. The image of the same set under the map $(x,y) \mapsto (-x,-y)$.

Int.divisorsAntidiag_neg_natCast theorem

 (n : ℕ) :
  divisorsAntidiag (-n) =
    (n.divisorsAntidiagonal.map <| .prodMap natCast negNatCast).disjUnion
      (n.divisorsAntidiagonal.map <| .prodMap negNatCast natCast) (by simp +contextual [disjoint_left, eq_comm])

Full source

lemma divisorsAntidiag_neg_natCast (n : ℕ) :
    divisorsAntidiag (-n) =
      (n.divisorsAntidiagonal.map <| .prodMap natCast negNatCast).disjUnion
        (n.divisorsAntidiagonal.map <| .prodMap negNatCast natCast) (by
          simp +contextual [disjoint_left, eq_comm]) := by cases n <;> rfl

Characterization of Integer Divisor Pairs for Negative Natural Numbers

Informal description

For any natural number $n$, the set of integer pairs $(a, b)$ such that $a \times b = -n$ is equal to the disjoint union of two sets: 1. The image of the set of natural number pairs $(x, y)$ with $x \times y = n$ under the map $(x, y) \mapsto (x, -y)$, and 2. The image of the same set under the map $(x, y) \mapsto (-x, y)$.

Int.divisorsAntidiag_ofNat theorem

 (n : ℕ) :
  divisorsAntidiag ofNat(n) =
    (n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion
      (n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by simp +contextual [disjoint_left, eq_comm])

Full source

lemma divisorsAntidiag_ofNat (n : ℕ) :
    divisorsAntidiag ofNat(n) =
      (n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion
        (n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by
          simp +contextual [disjoint_left, eq_comm]) := rfl

Characterization of Integer Divisor Pairs for Natural Numbers

Informal description

For any natural number $n$, the set of integer pairs $(a,b)$ such that $a \times b = n$ is equal to the disjoint union of two sets: the image of the natural number divisor pairs $(x,y)$ under the map $(x,y) \mapsto (x,y)$, and the image of the same pairs under the map $(x,y) \mapsto (-x,-y)$. More precisely, the set $\text{divisorsAntidiag}(n)$ is given by: $$\text{divisorsAntidiag}(n) = \{(x,y) \mid x,y \in \mathbb{N}, x \times y = n\} \sqcup \{(-x,-y) \mid x,y \in \mathbb{N}, x \times y = n\}$$ where $\sqcup$ denotes disjoint union.

Int.mul_mem_one_two_three_iff theorem

 {a b : ℤ} :
  a * b ∈ ({ 1, 2, 3 } : Set ℤ) ↔
    (a, b) ∈ ({(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)} : Set (ℤ × ℤ))

Full source

/-- This lemma justifies its existence from its utility in crystallographic root system theory. -/
lemma mul_mem_one_two_three_iff {a b : ℤ} :
    a * b ∈ ({1, 2, 3} : Set ℤ)a * b ∈ ({1, 2, 3} : Set ℤ) ↔ (a, b) ∈ ({
      (1, 1), (-1, -1),
      (1, 2), (2, 1), (-1, -2), (-2, -1),
      (1, 3), (3, 1), (-1, -3), (-3, -1)} : Set (ℤ × ℤ)) := by
  simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]
  aesop

Characterization of Integer Pairs with Product in $\{1, 2, 3\}$

Informal description

For any integers $a$ and $b$, the product $a \times b$ belongs to the set $\{1, 2, 3\}$ if and only if the pair $(a, b)$ is one of the following: $$(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1).$$

Int.mul_mem_zero_one_two_three_four_iff theorem

 {a b : ℤ} (h₀ : a = 0 ↔ b = 0) :
  a * b ∈ ({0, 1, 2, 3, 4} : Set ℤ) ↔
    (a, b) ∈
      ({(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1),
          (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)} :
        Set (ℤ × ℤ))

Full source

/-- This lemma justifies its existence from its utility in crystallographic root system theory. -/
lemma mul_mem_zero_one_two_three_four_iff {a b : ℤ} (h₀ : a = 0 ↔ b = 0) :
    a * b ∈ ({0, 1, 2, 3, 4} : Set ℤ)a * b ∈ ({0, 1, 2, 3, 4} : Set ℤ) ↔ (a, b) ∈ ({
      (0, 0),
      (1, 1), (-1, -1),
      (1, 2), (2, 1), (-1, -2), (-2, -1),
      (1, 3), (3, 1), (-1, -3), (-3, -1),
      (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)} : Set (ℤ × ℤ)) := by
  simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]
  aesop

Characterization of Integer Pairs with Product in $\{0,1,2,3,4\}$

Informal description

For any integers $a$ and $b$ such that $a = 0$ if and only if $b = 0$, the product $a \times b$ belongs to the set $\{0, 1, 2, 3, 4\}$ if and only if the pair $(a, b)$ is in the set $\{(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)\}$.

Mathlib.NumberTheory.Divisors

Main Definitions

Conventions

Tags