Mathlib.NumberTheory.Divisors._auxLemma.15
theorem Mathlib.NumberTheory.Divisors._auxLemma.15 :
∀ {n : ℕ} {x : ℕ × ℕ}, (x ∈ n.divisorsAntidiagonal) = (x.1 * x.2 = n ∧ n ≠ 0)
The theorem `Mathlib.NumberTheory.Divisors._auxLemma.15` states that for every natural number `n` and every pair of natural numbers `x`, the pair `x` is in the set of divisors antidiagonal of `n` if and only if the product of the elements of `x` equals `n` and `n` is not equal to zero. The "divisors antidiagonal" of a number `n` is defined as the set of all pairs of natural numbers `(x, y)` such that `x * y = n`.
More concisely: The theorem `Mathlib.NumberTheory.Divisors._auxLemma.15` asserts that a pair `(x, y)` of natural numbers is in the set of divisors antidiagonal of a natural number `n` if and only if `x * y = n` and `n` is non-zero.
|
Nat.map_div_right_divisors
theorem Nat.map_div_right_divisors :
∀ {n : ℕ}, Finset.map { toFun := fun d => (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal
The theorem `Nat.map_div_right_divisors` states that for every natural number `n`, if we map each divisor `d` of `n` to a pair `(d, n / d)`, we get exactly the same set as the set of pairs `(x, y)` with `x * y = n`. This uses the function `Finset.map`, which takes an injective function and applies it to each element of a set without adding duplicates, and `Nat.divisors`, which gives the set of divisors of a number. The equality is between two sets of pairs of natural numbers, and it shows a relationship between the divisors of a number and the pairs of numbers that multiply to give that number.
More concisely: The set of pairs (d, n/d) where d is a divisor of natural number n is equal to the set of pairs (x, y) with x * y = n.
|
Mathlib.NumberTheory.Divisors._auxLemma.12
theorem Mathlib.NumberTheory.Divisors._auxLemma.12 : ∀ {n m : ℕ}, (n ∈ m.divisors) = (n ∣ m ∧ m ≠ 0)
The theorem `Mathlib.NumberTheory.Divisors._auxLemma.12` states that for any two natural numbers `n` and `m`, `n` is a divisor of `m` (i.e., `n` is in the set of divisors of `m`) if and only if `n` divides `m` and `m` is not equal to zero. This theorem essentially provides a criterion to test whether a number is a divisor of another number.
More concisely: A natural number `n` is a divisor of another natural number `m` if and only if `n` divides `m` and `m` is nonzero.
|
Nat.dvd_of_mem_divisors
theorem Nat.dvd_of_mem_divisors : ∀ {n m : ℕ}, n ∈ m.divisors → n ∣ m
This theorem states that for any two natural numbers `n` and `m`, if `n` is an element of the set of divisors of `m` (i.e., `n` is in `Nat.divisors m`), then `n` divides `m`. The set of divisors of a number, as defined above, is a set of numbers that can divide that number without leaving a remainder. In mathematical terms, this theorem is saying that if `n` is a divisor of `m`, then `m` is a multiple of `n`.
More concisely: For any natural numbers `n` and `m`, if `n` is a divisor of `m` then `m` is a multiple of `n`.
|
Nat.mem_properDivisors
theorem Nat.mem_properDivisors : ∀ {n m : ℕ}, n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
This theorem states that for any two natural numbers `n` and `m`, `n` is a member of the proper divisors of `m` if and only if `n` not only divides `m`, but `n` is also less than `m`. In other words, the proper divisors of a number `m` are exactly those numbers which divide `m` and are strictly smaller than `m`.
More concisely: The proper divisors of a natural number `m` are those natural numbers `n` that divide `m` and satisfy `n < m`.
|
Nat.map_swap_divisorsAntidiagonal
theorem Nat.map_swap_divisorsAntidiagonal :
∀ {n : ℕ}, Finset.map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal
This theorem states that for any natural number `n`, if you map the elements of the finset `Nat.divisorsAntidiagonal n` (which consists of pairs `(x, y)` such that `x * y = n`) under the equivalence `Equiv.prodComm ℕ ℕ` (which swaps the elements of the pair), you get the same set `Nat.divisorsAntidiagonal n`. In other words, swapping the elements in each pair of the `divisorsAntidiagonal` of a number does not change the set of divisor pairs of that number.
More concisely: For any natural number `n`, the set of pairs `(x, y)` such that `x * y = n` is equal to its image under the swapping operation of `Equiv.prodComm ℕ ℕ`.
|
Nat.divisors_prime_pow
theorem Nat.divisors_prime_pow :
∀ {p : ℕ} (pp : p.Prime) (k : ℕ),
(p ^ k).divisors = Finset.map { toFun := fun x => p ^ x, inj' := ⋯ } (Finset.range (k + 1))
The theorem `Nat.divisors_prime_pow` states that for any natural number `p` that is prime (as defined by `Nat.Prime p`) and any natural number `k`, the set of divisors of `p ^ k` (as defined by `Nat.divisors`) is equal to the set obtained by mapping the function `p ^ x` over the set of natural numbers less than `k + 1` (as defined by `Finset.range`). In other words, if `p` is a prime number and `k` is any natural number, the divisors of `p` raised to the power of `k` are precisely the numbers `p` raised to the power of every natural number less than `k + 1`.
More concisely: For any prime number $p$ and natural number $k$, the divisors of $p^k$ are the numbers $p^x$ for $x$ in the range $0$ to $k$.
|
Nat.mem_divisors
theorem Nat.mem_divisors : ∀ {n m : ℕ}, n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
The theorem `Nat.mem_divisors` states that for any two natural numbers `n` and `m`, `n` is a member of the set of divisors of `m` if and only if `n` is a divisor of `m` and `m` is not equal to 0. In other words, a natural number `n` is in the finset of divisors of another natural number `m` precisely when `n` divides `m` and `m` is not zero.
More concisely: A natural number is a divisor of another natural number if and only if it divides that number and the second number is non-zero.
|
Mathlib.NumberTheory.Divisors._auxLemma.2
theorem Mathlib.NumberTheory.Divisors._auxLemma.2 : ∀ {n m : ℕ}, (m ∈ Finset.range n) = (m < n)
This theorem states that for any two natural numbers `n` and `m`, `m` is an element in the set of natural numbers less than `n` (denoted as `Finset.range n`), if and only if `m` is less than `n`. This is essentially a characterization of the set of natural numbers less than a given natural number.
More concisely: For any natural numbers `n` and `m`, `m` is in the set of natural numbers less than `n` if and only if `m < n`.
|
Nat.mem_divisors_self
theorem Nat.mem_divisors_self : ∀ (n : ℕ), n ≠ 0 → n ∈ n.divisors
The theorem `Nat.mem_divisors_self` states that for any natural number `n` that is not zero, `n` is a member of its own set of divisors. That is, a natural number `n` (except for 0) divides itself. In the language of set theory, this means `n` belongs to the set of its own divisors.
More concisely: For any non-zero natural number `n`, `n` is a divisor of itself.
|
Nat.Prime.properDivisors
theorem Nat.Prime.properDivisors : ∀ {p : ℕ}, p.Prime → p.properDivisors = {1}
This theorem states that for every natural number `p`, if `p` is a prime number, then the set of proper divisors of `p` is the set that contains only the number `1`. In mathematical terms, it establishes that the proper divisors of a prime number `p` are only `1`, since prime numbers are defined as those natural numbers greater than 1 that have no other divisors besides `1` and themselves.
More concisely: The theorem asserts that the set of proper divisors of a prime number is empty or, equivalently, that a prime number's only proper divisor is 1.
|
Nat.properDivisors.not_self_mem
theorem Nat.properDivisors.not_self_mem : ∀ {n : ℕ}, n ∉ n.properDivisors
This theorem states that for any natural number 'n', 'n' is not a member of its own proper divisors set. In other words, a natural number 'n' cannot be a proper divisor of itself. Proper divisors are those divisors of 'n' that are less than 'n' and greater than 1, excluding 'n' itself.
More concisely: For any natural number n, n is not a divisor of itself when considering only proper divisors (i.e., divisors strictly less than and greater than n).
|
Nat.divisors_zero
theorem Nat.divisors_zero : Nat.divisors 0 = ∅
The theorem `Nat.divisors_zero` states that the set of divisors of 0, as given by the function `Nat.divisors`, is the empty set. In other words, there are no natural numbers that divide 0.
More concisely: The set of divisors of 0, as defined in Lean's Nat.divisors function, is the empty set.
|
Nat.one_mem_properDivisors_iff_one_lt
theorem Nat.one_mem_properDivisors_iff_one_lt : ∀ {n : ℕ}, 1 ∈ n.properDivisors ↔ 1 < n
The theorem `Nat.one_mem_properDivisors_iff_one_lt` states that for all natural numbers `n`, the number 1 is a proper divisor of `n` if and only if `n` is greater than 1. Here, a "proper divisor" of a number is defined as a divisor of the number that is not equal to the number itself. In the special case where `n` is 0, the set of proper divisors is empty, as defined by the function `Nat.properDivisors`.
More concisely: For all natural numbers $n$, $1$ is a proper divisor of $n$ if and only if $n$ is a positive integer.
|
Nat.cons_self_properDivisors
theorem Nat.cons_self_properDivisors : ∀ {n : ℕ}, n ≠ 0 → Finset.cons n n.properDivisors ⋯ = n.divisors
The theorem `Nat.cons_self_properDivisors` states that for every non-zero natural number `n`, adding `n` (using the `Finset.cons` function) to its own set of proper divisors (which are divisors excluding `n` itself) will yield the full set of its divisors. In other words, if we take the set of proper divisors of `n` and add `n` to this set, we get the same set as if we had started with the set of all divisors of `n`.
More concisely: For every non-zero natural number `n`, the set of proper divisors of `n` and the set of divisors of `n` including `n` itself are equal.
|
Nat.properDivisors_zero
theorem Nat.properDivisors_zero : Nat.properDivisors 0 = ∅
The theorem `Nat.properDivisors_zero` states that the set of proper divisors of zero is empty. In the context of natural numbers, a proper divisor of a number is any divisor other than the number itself. However, zero doesn't have any proper divisors, hence the proper divisors of zero forms an empty set.
More concisely: The set of proper divisors of zero is empty.
|
Nat.mem_divisorsAntidiagonal
theorem Nat.mem_divisorsAntidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0 := by
sorry
This theorem states that for any natural numbers `n` and `x` (which is a pair of natural numbers), `x` belongs to `n`'s divisor antidiagonal if and only if the product of the elements of the pair `x` equals `n` and `n` is not equal to zero. In other words, a pair of natural numbers is in the set of pairs whose product equals `n` (the so-called divisor antidiagonal of `n`) exactly when this product is indeed `n` and `n` is not zero.
More concisely: The pair of natural numbers `(x, y)` is in the divisor antidiagonal of `n` if and only if `x * y = n` and `n` is non-zero.
|
Nat.pos_of_mem_divisors
theorem Nat.pos_of_mem_divisors : ∀ {n m : ℕ}, m ∈ n.divisors → 0 < m
The theorem `Nat.pos_of_mem_divisors` states that for any two natural numbers `n` and `m`, if `m` is a member of the set of divisors of `n` (as defined by `Nat.divisors n`), then `m` is greater than zero. In other words, any divisor of a natural number, excluding zero itself, is always a positive natural number.
More concisely: For all natural numbers `n` and `m`, if `m` is in the set of divisors of `n` (`m ∈ Nat.divisors n`), then `m` is a positive natural number (`m > 0`).
|
Nat.pos_of_mem_properDivisors
theorem Nat.pos_of_mem_properDivisors : ∀ {n m : ℕ}, m ∈ n.properDivisors → 0 < m
The theorem `Nat.pos_of_mem_properDivisors` states that for all natural numbers `n` and `m`, if `m` is a member of the set of proper divisors of `n`, then `m` is greater than 0. In other words, every element `m` in the proper divisors of a natural number `n` (as defined by `Nat.properDivisors`) is a positive natural number.
More concisely: For all natural numbers `n` and `m`, if `m` is a proper divisor of `n`, then `m` is a positive natural number.
|
Mathlib.NumberTheory.Divisors._auxLemma.1
theorem Mathlib.NumberTheory.Divisors._auxLemma.1 :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α},
(a ∈ Finset.filter p s) = (a ∈ s ∧ p a)
This theorem states that for any type `α`, predicate `p` (a property of `α`), and finite set `s` of elements of `α`, and any element `a` of `α`, the membership of `a` in the filtered set of `s` (i.e., `Finset.filter p s`) is equivalent to `a` being a member of `s` and `a` satisfying the predicate `p`. In other words, an element belongs to the filtered set if and only if it belongs to the original set and meets the condition specified by the predicate.
More concisely: For any type `α`, finite set `s` of `α`, predicate `p` on `α`, and `a` in `α`, `a` is in the filtered set `Finset.filter p s` if and only if `a` is in `s` and satisfies `p(a)`.
|
Nat.sum_divisorsAntidiagonal
theorem Nat.sum_divisorsAntidiagonal :
∀ {M : Type u_1} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ},
(n.divisorsAntidiagonal.sum fun i => f i.1 i.2) = n.divisors.sum fun i => f i (n / i)
The theorem `Nat.sum_divisorsAntidiagonal` states that for any natural number `n` and any function `f` from pairs of natural numbers to a type `M` that has an addition operation, the sum of `f` applied to each pair in the divisor antidiagonal of `n` is equal to the sum of `f` applied to each divisor of `n` and `n` divided by that divisor. In other words, it expresses a relationship between the sum over the divisors of a number and the sum over its divisor pairs, under a given function `f`.
More concisely: For any natural number `n` and function `f` from pairs of natural numbers to a type with addition, the sum of `f` applied to each divisor pair in the antidiagonal of `n` equals the sum of `f` applied to each divisor of `n` and the quotient of `n` by that divisor.
|
Nat.prime_divisors_eq_to_filter_divisors_prime
theorem Nat.prime_divisors_eq_to_filter_divisors_prime :
∀ (n : ℕ), n.factors.toFinset = Finset.filter Nat.Prime n.divisors
This theorem states that the prime factors of a natural number 'n' are equivalent to the set of divisors of 'n' that satisfy the property of being prime. In other words, when we collect all factors of 'n' and filter them to only include those that are prime, we get the same set as the prime factors of 'n'. This statement holds true for any natural number 'n'.
More concisely: The set of prime divisors of a natural number equals the set of prime factors of that number.
|
Nat.mem_properDivisors_iff_exists
theorem Nat.mem_properDivisors_iff_exists : ∀ {m n : ℕ}, n ≠ 0 → (m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k)
This theorem states that for any two natural numbers `m` and `n`, if `n` is not zero, then `m` is a proper divisor of `n` if and only if there exists a natural number `k` greater than 1 such that `n` equals `m` times `k`. In other words, a number `m` is a proper divisor of `n` if there is another number `k` that can multiply `m` to give `n`, with the restriction that `k` should be greater than 1.
More concisely: For natural numbers `m` and `n`, `m` is a proper divisor of `n` if and only if there exists `k` greater than 1 such that `n = m * k`.
|
Nat.divisor_le
theorem Nat.divisor_le : ∀ {n m : ℕ}, n ∈ m.divisors → n ≤ m
The theorem `Nat.divisor_le` states that for any natural numbers `n` and `m`, if `n` is a divisor of `m` (i.e., `n` is in the set of divisors of `m`), then `n` is less than or equal to `m`. This is a fundamental property of division in the set of natural numbers, which states that a divisor cannot be larger than the number it divides.
More concisely: If `n` is a divisor of `m` in the natural numbers, then `n` is less than or equal to `m`.
|
Mathlib.NumberTheory.Divisors._auxLemma.3
theorem Mathlib.NumberTheory.Divisors._auxLemma.3 :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
(x ∈ Finset.Ico a b) = (a ≤ x ∧ x < b)
This theorem states that for any type `α` equipped with a preorder and a locally finite order, and for any elements `a`, `b`, and `x` of type `α`, `x` is in the finite set of elements that are greater than or equal to `a` and less than `b` (represented as `Finset.Ico a b`), if and only if `x` is greater than or equal to `a` and less than `b`. This result formalizes the idea that membership in the set defined by an interval is equivalent to satisfying the inequalities that define the interval.
More concisely: For any preorder and locally finite type `α`, an element `x` belongs to the interval `[a, b]` if and only if `a ≤ x` and `x < b`.
|