Nat.Prime.pow_inj
theorem Nat.Prime.pow_inj : ∀ {p q m n : ℕ}, p.Prime → q.Prime → p ^ (m + 1) = q ^ (n + 1) → p = q ∧ m = n
The theorem states that for any two prime numbers `p` and `q`, and any two natural numbers `m` and `n`, if `p` and `q` are primes and the `(m+1)`-th power of `p` equals the `(n+1)`-th power of `q`, then `p` must be equal to `q` and `m` must be equal to `n`. In other words, two prime powers with positive exponents can only be equal when both the base primes and the exponents themselves are equal.
More concisely: If two distinct prime numbers raised to distinct positive powers are equal, then both the bases and the exponents are equal.
|
Prime.nat_prime
theorem Prime.nat_prime : ∀ {p : ℕ}, Prime p → p.Prime
This theorem states that for any natural number `p`, if `p` is prime according to the custom definition of primality given for a commutative monoid with zero (namely, that `p` is nonzero, not a unit, and that whenever `p` divides the product of `a` and `b`, it divides at least one of `a` or `b`), then `p` is also prime according to the native Lean 4 definition of primality for natural numbers.
More concisely: If a natural number `p` is prime according to the commutative monoid definition, then it is prime according to the native Lean 4 definition for natural numbers.
|
Nat.Prime.one_lt
theorem Nat.Prime.one_lt : ∀ {p : ℕ}, p.Prime → 1 < p
The theorem `Nat.Prime.one_lt` states that for all natural numbers `p`, if `p` is a prime number, then `p` is greater than 1. In other words, if a natural number is prime, it must be strictly larger than 1.
More concisely: If a natural number `p` is prime, then `p` is a positive integer greater than 1.
|
Nat.eq_prime_pow_of_dvd_least_prime_pow
theorem Nat.eq_prime_pow_of_dvd_least_prime_pow :
∀ {a p k : ℕ}, p.Prime → ¬a ∣ p ^ k → a ∣ p ^ (k + 1) → a = p ^ (k + 1)
This theorem states that for any natural numbers `a`, `p`, and `k`, if `p` is prime, `a` does not divide `p` to the power of `k`, but `a` does divide `p` to the power of `k+1`, then `a` must be equal to `p` to the power of `k+1`. In other words, if a prime number `p` raised to an exponent `k+1` is divisible by `a`, but `p` raised to the lower exponent `k` is not, then `a` is exactly that higher power of `p`, denoted as `p^(k+1)`.
More concisely: If a prime number `p` raises to `k+1` is divisible by `a`, but `p` raises to the power `k` is not, then `a` equals `p` raised to the power `k+1`.
|
Nat.coprime_or_dvd_of_prime
theorem Nat.coprime_or_dvd_of_prime : ∀ {p : ℕ}, p.Prime → ∀ (i : ℕ), p.Coprime i ∨ p ∣ i
The theorem `Nat.coprime_or_dvd_of_prime` states that for any prime number `p` and any natural number `i`, `p` and `i` are either coprime, meaning their greatest common divisor (gcd) is 1, or `p` divides `i`. In other words, if `p` is a prime number and `i` is any natural number, then `p` and `i` either have no common factors other than 1, or `p` is a factor of `i`.
More concisely: For any prime number p and natural number i, p and i are coprime or p divides i.
|
Nat.minFac_le
theorem Nat.minFac_le : ∀ {n : ℕ}, 0 < n → n.minFac ≤ n
The theorem `Nat.minFac_le` states that for every natural number `n` that is greater than zero, the smallest prime factor of `n` (represented by the function `Nat.minFac n`) is less than or equal to `n` itself. This means if you find the least prime number that divides `n`, this number will always be less than or equal to `n`.
More concisely: For every natural number $n > 0$, the smallest prime factor of $n$ (denoted as $\operatorname{minFac}(n)$ in Lean) is less than or equal to $n$.
|
Nat.Prime.dvd_of_dvd_pow
theorem Nat.Prime.dvd_of_dvd_pow : ∀ {p m n : ℕ}, p.Prime → p ∣ m ^ n → p ∣ m
The theorem `Nat.Prime.dvd_of_dvd_pow` states that for any natural numbers `p`, `m` and `n`, if `p` is a prime number and `p` divides `m` raised to the power `n`, then `p` also divides `m`. In mathematical terms, if $p$ is a prime number and $p | m^n$, then $p | m$. This is a fundamental property of prime numbers related to divisibility and exponentiation.
More concisely: If a prime number `p` divides `m` raised to the power `n`, then `p` divides `m` (i.e., `p | m => p | m^n`).
|
Nat.prime_iff_prime_int
theorem Nat.prime_iff_prime_int : ∀ {p : ℕ}, p.Prime ↔ Prime ↑p
This theorem states that for every natural number `p`, `p` is a prime number if and only if the integer equivalent of `p` is a prime element of a commutative monoid with zero. In other words, a natural number `p` is prime (i.e., it is at least 2 and its only divisors are `p` and `1`) if and only if when `p` is considered as an integer, it satisfies the properties of being a prime element in the context of a Commutative Monoid with Zero (i.e., `p` is not zero, is not a unit, and if `p` divides the product of two integers, then `p` must divide at least one of them).
More concisely: A natural number `p` is prime if and only if the integer `p` is a prime element in a commutative monoid with zero.
|
Nat.Prime.pos
theorem Nat.Prime.pos : ∀ {p : ℕ}, p.Prime → 0 < p
The theorem `Nat.Prime.pos` states that for every natural number `p`, if `p` is prime, then `p` is greater than 0. In other words, any prime number is positive.
More concisely: Every prime natural number is positive.
|
Nat.Prime.odd_of_ne_two
theorem Nat.Prime.odd_of_ne_two : ∀ {p : ℕ}, p.Prime → p ≠ 2 → Odd p
The theorem `Nat.Prime.odd_of_ne_two` states that for every natural number `p`, if `p` is a prime number and `p` is not equal to 2, then `p` is an odd number. In other words, any prime number other than 2 is odd. This follows from the definition of odd numbers in a semiring, where a number is considered odd if it can be expressed as `2*k + 1` for some integer `k`, and the definition of prime numbers, where a prime is a natural number greater than 1 that has no divisors other than 1 and itself.
More concisely: If a natural number `p` is prime and not equal to 2, then `p` is an odd number.
|
Nat.minFac_le_of_dvd
theorem Nat.minFac_le_of_dvd : ∀ {n m : ℕ}, 2 ≤ m → m ∣ n → n.minFac ≤ m
The theorem `Nat.minFac_le_of_dvd` states that for any two natural numbers `n` and `m`, where `m` is greater than or equal to 2, if `m` divides `n`, then the smallest prime factor of `n` is less than or equal to `m`. In other words, no divisor of `n` that is greater than or equal to 2 can be smaller than the smallest prime factor of `n`.
More concisely: If `m` divides `n` and `m` is greater than or equal to 2, then the smallest prime factor of `n` is less than or equal to `m`.
|
Nat.minFac_sq_le_self
theorem Nat.minFac_sq_le_self : ∀ {n : ℕ}, 0 < n → ¬n.Prime → n.minFac ^ 2 ≤ n
The theorem `Nat.minFac_sq_le_self` states that for any natural number `n` that is greater than zero and is not a prime number, the square of its smallest prime factor (`n.minFac ^ 2`) is always less than or equal to `n` itself. In other words, this theorem says that the square of the smallest prime factor of a composite number can never exceed the number itself.
More concisely: For any composite natural number `n` greater than 1, the square of its smallest prime factor is less than or equal to `n`.
|
Nat.exists_prime_and_dvd
theorem Nat.exists_prime_and_dvd : ∀ {n : ℕ}, n ≠ 1 → ∃ p, p.Prime ∧ p ∣ n
The theorem `Nat.exists_prime_and_dvd` states that for any natural number `n` that is not equal to 1, there exists a prime number `p` such that `p` is a divisor of `n`. In other words, every natural number greater than 1 has at least one prime number as a divisor.
More concisely: For every natural number `n` greater than 1, there exists a prime number `p` such that `p` divides `n`.
|
Nat.minFac_pos
theorem Nat.minFac_pos : ∀ (n : ℕ), 0 < n.minFac
The theorem `Nat.minFac_pos` states that for any natural number `n`, the smallest prime factor of `n` is greater than zero. This means that every natural number `n` has at least one prime factor which is strictly positive.
More concisely: For every natural number `n`, there exists a prime number `p` such that `n` is divisible by `p` and `p` is greater than zero.
|
Nat.Prime.dvd_iff_eq
theorem Nat.Prime.dvd_iff_eq : ∀ {p a : ℕ}, p.Prime → a ≠ 1 → (a ∣ p ↔ p = a)
The theorem `Nat.Prime.dvd_iff_eq` states that for any natural numbers `p` and `a`, where `p` is a prime number and `a` is not equal to 1, `a` is a divisor of `p` if and only if `p` equals `a`. In other words, a prime number is only divisible by itself and 1, and this theorem reinforces that by stating if a prime number is divisible by a number that's not 1, then that number must be the prime number itself.
More concisely: A natural number `p` is a prime if and only if for all `a` with `a ≠ 1`, `a` does not divide `p` if and only if `p` equals `a`.
|
Nat.not_bddAbove_setOf_prime
theorem Nat.not_bddAbove_setOf_prime : ¬BddAbove {p | p.Prime}
This theorem, `Nat.not_bddAbove_setOf_prime`, states that the set of prime numbers is not bounded above. In other words, there is no maximum prime number; for any given prime number, there is always another prime number that is larger. This is a variant of the traditional theorem stating the infiniteness of the set of prime numbers, here formalized using the `BddAbove` predicate.
More concisely: The set of prime numbers is unbounded.
|
Nat.Prime.not_coprime_iff_dvd
theorem Nat.Prime.not_coprime_iff_dvd : ∀ {m n : ℕ}, ¬m.Coprime n ↔ ∃ p, p.Prime ∧ p ∣ m ∧ p ∣ n
This theorem states that for any two natural numbers `m` and `n`, `m` and `n` are not coprime (or their greatest common divisor is not 1) if and only if there exists a prime number `p` such that `p` divides both `m` and `n`. In other words, the lack of coprimality between `m` and `n` is equivalent to the existence of a common prime divisor.
More concisely: m and n are not coprime if and only if there exists a prime p that divides both m and n.
|
Nat.prime_iff
theorem Nat.prime_iff : ∀ {p : ℕ}, p.Prime ↔ Prime p
This theorem establishes an equivalence between the two definitions of primality for a natural number `p`: `Nat.Prime p` and `Prime p`. Specifically, it states that for any natural number `p`, `p` is a prime number according to the `Nat.Prime` definition if and only if `p` is a prime element according to the `Prime` definition in the context of a `CommMonoidWithZero`. In other words, a natural number `p` is prime (i.e., it is at least 2 and its only divisors are `p` and `1`) if and only if `p` is a non-zero, non-unit element of a `CommMonoidWithZero` that divides the product of any two elements `a` and `b` only if it divides `a` or `b`.
More concisely: For any natural number `p`, `p` is a prime number according to the `Nat.Prime` definition in Lean if and only if `p` is a prime element in the multiplicative monoid of natural numbers under multiplication.
|
Nat.Prime.prime
theorem Nat.Prime.prime : ∀ {p : ℕ}, p.Prime → Prime p
The theorem `Nat.Prime.prime` states that for every natural number `p`, if `p` is a prime number (according to the `Nat.Prime` definition which means `p` is a natural number at least 2 and the only divisors are `p` and `1`), then `p` is also a prime element in the context of a `CommMonoidWithZero` (according to the `Prime` definition which means `p` is not zero, is not a unit, and if `p` divides the product of `a` and `b`, then `p` must divide either `a` or `b`). This is essentially a translation between two different definitions of primality, each applicable in different mathematical settings.
More concisely: For every natural number `p` that is a prime number according to the `Nat.Prime` definition, it is also a prime element in the context of a `CommMonoidWithZero`.
|
Nat.Prime.two_le
theorem Nat.Prime.two_le : ∀ {p : ℕ}, p.Prime → 2 ≤ p
The theorem `Nat.Prime.two_le` states that for any natural number `p`, if `p` is prime, then `p` is greater than or equal to 2. In other words, it says that all prime numbers are at least 2.
More concisely: If a natural number `p` is prime, then `p ≥ 2`.
|
Nat.Prime.mod_two_eq_one_iff_ne_two
theorem Nat.Prime.mod_two_eq_one_iff_ne_two : ∀ {p : ℕ} [inst : Fact p.Prime], p % 2 = 1 ↔ p ≠ 2
This theorem states that for any natural number `p` which is prime, `p` gives a remainder of 1 when divided by 2 if and only if `p` is not equal to 2. In other words, a prime number `p` is odd (since it gives a remainder of 1 when divided by 2) if and only if it is not the number 2 (which is the only even prime number).
More concisely: A prime number is odd if and only if it is not 2. (In other words, a prime number gives a remainder of 1 when divided by 2 if and only if it is not 2.)
|
Nat.exists_infinite_primes
theorem Nat.exists_infinite_primes : ∀ (n : ℕ), ∃ p, n ≤ p ∧ p.Prime
This is Euclid's theorem on the infinitude of primes. The theorem states that for every natural number `n`, there exists a prime number `p` such that `p` is greater than or equal to `n`. In other words, there are infinitely many prime numbers, and for any given natural number, there will always be a prime number that is greater than or equal to that number.
More concisely: For every natural number `n`, there exists a prime number `p` such that `p > n`.
|
Nat.dvd_prime_pow
theorem Nat.dvd_prime_pow : ∀ {p : ℕ}, p.Prime → ∀ {m i : ℕ}, i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k
This theorem states that for any natural number `p` which is prime, and for any natural numbers `m` and `i`, `i` divides `p` raised to the power of `m` if and only if there exists a natural number `k` that is less than or equal to `m` such that `i` is equal to `p` raised to the power of `k`. In mathematical terms, for a prime number $p$ and natural numbers $m$ and $i$, $i$ divides $p^m$ exactly when $i$ is equal to $p^k$ for some $k$ satisfying $k \leq m$.
More concisely: For a prime number p and natural numbers m and i, i divides p^m if and only if i is p raised to some power k with k <= m.
|
Nat.Prime.coprime_iff_not_dvd
theorem Nat.Prime.coprime_iff_not_dvd : ∀ {p n : ℕ}, p.Prime → (p.Coprime n ↔ ¬p ∣ n)
The theorem `Nat.Prime.coprime_iff_not_dvd` states that for any two natural numbers `p` and `n`, if `p` is a prime number, then `p` and `n` are coprime (their greatest common divisor is `1`) if and only if `p` does not divide `n`. In other words, a prime number `p` and another number `n` share no common divisors other than `1` exactly when `p` is not a divisor of `n`.
More concisely: A prime number is coprime with another natural number if and only if it does not divide that number.
|
Nat.coprime_primes
theorem Nat.coprime_primes : ∀ {p q : ℕ}, p.Prime → q.Prime → (p.Coprime q ↔ p ≠ q)
The theorem `Nat.coprime_primes` states that for every two natural numbers `p` and `q`, if `p` and `q` are both prime (i.e., they are natural numbers that are at least 2 and their only divisors are themselves and 1), then `p` and `q` are coprime (i.e., their greatest common divisor is 1) if and only if `p` is not equal to `q`. This reflects the fundamental property of prime numbers, where two different prime numbers do not share any common divisor apart from 1.
More concisely: If two natural numbers `p` and `q` are both prime, then they are coprime if and only if `p` is not equal to `q`.
|
Nat.not_prime_one
theorem Nat.not_prime_one : ¬Nat.Prime 1
The theorem `Nat.not_prime_one` states that the number 1 is not a prime number. In the context of natural numbers, a prime number is defined as a number greater than or equal to 2 whose only divisors are itself and 1. Therefore, 1 does not meet the criteria to be considered prime.
More concisely: The number 1 is not a prime number in the natural numbers.
|
Nat.Prime.minFac_eq
theorem Nat.Prime.minFac_eq : ∀ {p : ℕ}, p.Prime → p.minFac = p
This theorem states that for any natural number `p`, if `p` is a prime number, then the smallest prime factor of `p` is `p` itself. In mathematical terms, this is saying that if `p` is a prime number (meaning it has no divisors other than `p` and `1`), then the smallest factor of `p` that is also a prime number is `p`.
More concisely: For any prime number p, p is its own smallest prime factor.
|
Nat.Prime.ne_one
theorem Nat.Prime.ne_one : ∀ {p : ℕ}, p.Prime → p ≠ 1
The theorem `Nat.Prime.ne_one` states that for every natural number `p`, if `p` is a prime number, then `p` cannot be equal to 1. In other words, no prime number can be 1. This is consistent with the definition of a prime number as a natural number at least 2 whose only divisors are itself and 1.
More concisely: A prime number in Lean 4 cannot be equal to 1.
|
Nat.prime_dvd_prime_iff_eq
theorem Nat.prime_dvd_prime_iff_eq : ∀ {p q : ℕ}, p.Prime → q.Prime → (p ∣ q ↔ p = q)
The theorem `Nat.prime_dvd_prime_iff_eq` states that for any two natural numbers `p` and `q`, if `p` and `q` are both prime numbers, then `p` divides `q` if and only if `p` is equal to `q`. In other words, a prime number can only divide another prime number if they are the same. This captures a key property of prime numbers in number theory, which are numbers that have exactly two positive divisors: 1 and the number itself.
More concisely: If two natural numbers `p` and `q` are both prime, then `p` divides `q` if and only if `p` equals `q`.
|
Nat.prime_def_minFac
theorem Nat.prime_def_minFac : ∀ {p : ℕ}, p.Prime ↔ 2 ≤ p ∧ p.minFac = p
The theorem `Nat.prime_def_minFac` states that for every natural number `p`, `p` is a prime number if and only if `p` is greater than or equal to 2 and the smallest prime factor of `p` is `p` itself. In other words, a natural number `p` is prime exactly when it is not less than 2 and it does not have any prime factor smaller than itself.
More concisely: A natural number `p` is prime if and only if `p` is greater than or equal to 2 and the smallest prime factor of `p` is `p`.
|
Nat.factors_lemma
theorem Nat.factors_lemma : ∀ {k : ℕ}, (k + 2) / (k + 2).minFac < k + 2
The theorem `Nat.factors_lemma` states that for every natural number `k`, the quotient of `k + 2` divided by the smallest prime factor of `k + 2` is strictly less than `k + 2`. In other words, if you take any natural number, add 2 to it, and then divide by the smallest prime factor of the resulting number, the result will always be less than the original number plus 2.
More concisely: For every natural number `k`, the quotient of `k + 2` by the smallest prime factor of `k + 2` is strictly less than `k + 2`.
|
Nat.Prime.dvd_iff_not_coprime
theorem Nat.Prime.dvd_iff_not_coprime : ∀ {p n : ℕ}, p.Prime → (p ∣ n ↔ ¬p.Coprime n)
The theorem `Nat.Prime.dvd_iff_not_coprime` states that for all natural numbers `p` and `n`, if `p` is a prime number, then `p` divides `n` if and only if `p` and `n` are not coprime. Here, "divides" means that `n` divided by `p` leaves no remainder, and "not coprime" means that the greatest common divisor (gcd) of `p` and `n` is not equal to 1.
More concisely: For a natural number `n` and a prime number `p`, `p` divides `n` if and only if `p` and `n` have a common divisor other than 1.
|
Nat.prime_three
theorem Nat.prime_three : Nat.Prime 3
The theorem `Nat.prime_three` asserts that the natural number 3 is a prime number. In other words, 3 is a natural number which is at least 2 and its only divisors are 3 and 1.
More concisely: The theorem `Nat.prime_three` asserts that 3 is a prime natural number. (Equivalently, 3 has exactly two positive divisors: 1 and 3.)
|
Nat.Prime.dvd_mul
theorem Nat.Prime.dvd_mul : ∀ {p m n : ℕ}, p.Prime → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n)
The theorem `Nat.Prime.dvd_mul` states that for any natural numbers `p`, `m`, and `n`, if `p` is prime, then `p` divides the product `m * n` if and only if `p` divides `m` or `p` divides `n`. In mathematical terms, this is expressing the fundamental property of prime numbers that if a prime number divides a product, it must divide at least one of the factors.
More concisely: If a prime number `p` divides the product `m * n`, then `p` divides `m` or `p` divides `n`.
|
Nat.dvd_prime
theorem Nat.dvd_prime : ∀ {p m : ℕ}, p.Prime → (m ∣ p ↔ m = 1 ∨ m = p)
The theorem `Nat.dvd_prime` states that for every two natural numbers `p` and `m`, if `p` is a prime number, then `m` divides `p` if and only if `m` is either 1 or `p`. In mathematical terms, this says that if `p` is a prime number, its only divisors are 1 and `p` itself.
More concisely: If `p` is a prime number, then the divisors of `p` are exactly 1 and `p`.
|
Nat.minFac_dvd
theorem Nat.minFac_dvd : ∀ (n : ℕ), n.minFac ∣ n
The theorem `Nat.minFac_dvd` states that for all natural numbers `n`, the smallest prime factor of `n` (obtained using the `Nat.minFac` function) will always divide `n` without leaving a remainder. This is equivalent to saying that the natural number `n` is divisible by its smallest prime factor.
More concisely: The smallest prime factor of a natural number `n` (as given by `Nat.minFac`) divides `n`.
|
Nat.Prime.ne_zero
theorem Nat.Prime.ne_zero : ∀ {n : ℕ}, n.Prime → n ≠ 0
The theorem `Nat.Prime.ne_zero` states that for all natural numbers `n`, if `n` is prime, then `n` is not equal to zero. In mathematical terms, for any prime number `n`, it holds that `n ≠ 0`. This is consistent with the definition of a prime number, as a prime number is a natural number greater than 1 that has no positive divisors other than 1 and itself.
More concisely: A prime natural number is not equal to zero.
|
Nat.minFac_prime
theorem Nat.minFac_prime : ∀ {n : ℕ}, n ≠ 1 → n.minFac.Prime
The theorem `Nat.minFac_prime` states that for any natural number `n` that is not equal to 1, the smallest prime factor of `n`, as determined by the `Nat.minFac` function, is indeed a prime number, as defined by the `Nat.Prime` property. In other words, the `Nat.minFac` function always returns a prime number, provided that the input is not 1.
More concisely: For any natural number `n` not equal to 1, the prime number returned by `Nat.minFac` is indeed a prime factor of `n`.
|
Nat.Prime.not_dvd_one
theorem Nat.Prime.not_dvd_one : ∀ {p : ℕ}, p.Prime → ¬p ∣ 1
The theorem `Nat.Prime.not_dvd_one` states that for all natural numbers `p`, if `p` is a prime number, then `p` does not divide `1`. In other words, no prime number can be a divisor of 1.
More concisely: A prime number does not divide 1.
|
Nat.prime_def_lt''
theorem Nat.prime_def_lt'' : ∀ {p : ℕ}, p.Prime ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
The theorem `Nat.prime_def_lt''` states that for any natural number `p`, `p` is a prime number if and only if `p` is greater than or equal to 2 and for every natural number `m` that divides `p`, `m` is either equal to 1 or `p`. In mathematical terms, this theorem provides an equivalent definition for a natural number to be prime: a natural number `p` is prime if it is at least 2 and the only divisors of `p` are `1` and `p` itself.
More concisely: A natural number `p` is prime if and only if `p` is greater than 1 and has no divisors other than 1 and `p`.
|
Nat.coprime_of_dvd
theorem Nat.coprime_of_dvd : ∀ {m n : ℕ}, (∀ (k : ℕ), k.Prime → k ∣ m → ¬k ∣ n) → m.Coprime n
The theorem `Nat.coprime_of_dvd` states that for any natural numbers `m` and `n`, if all prime numbers `k` that divide `m` do not divide `n`, then `m` and `n` are coprime. In other words, if every prime number that is a factor of `m` is not a factor of `n`, then the greatest common divisor (gcd) of `m` and `n` is 1, which by definition means that `m` and `n` are relatively prime.
More concisely: If all prime divisors of natural numbers `m` and `n` are distinct, then `m` and `n` are coprime.
|
Nat.Prime.eq_one_or_self_of_dvd
theorem Nat.Prime.eq_one_or_self_of_dvd : ∀ {p : ℕ}, p.Prime → ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
This theorem states that for any natural number `p` that is prime, and any other natural number `m`, if `m` divides `p` then `m` must be either `1` or `p` itself. This is a property of prime numbers, which are defined as natural numbers greater than or equal to 2 that have no other divisors except for `1` and themselves.
More concisely: For any prime natural number `p` and any natural number `m` dividing `p`, `m` is equal to 1 or `p`.
|
Nat.coprime_two_left
theorem Nat.coprime_two_left : ∀ {n : ℕ}, Nat.Coprime 2 n ↔ Odd n
The theorem `Nat.coprime_two_left` states that for any natural number `n`, `n` and `2` are coprime (or relatively prime, meaning their greatest common divisor is `1`) if and only if `n` is odd. In other words, a natural number shares no common factor greater than `1` with `2` precisely when it is odd, which is defined as there existing a natural number `k` such that `n = 2*k + 1`.
More concisely: A natural number `n` is coprime to 2 if and only if `n` is odd.
|
Nat.not_prime_zero
theorem Nat.not_prime_zero : ¬Nat.Prime 0
The theorem `Nat.not_prime_zero` states that zero is not a prime number. In other words, it asserts that the natural number zero does not satisfy the prime number property, where a prime number is defined as a natural number that is at least 2 and its only divisors are itself and 1.
More concisely: Zero is not a prime number in the natural numbers.
|
Nat.minFac_has_prop
theorem Nat.minFac_has_prop : ∀ {n : ℕ}, n ≠ 1 → Nat.minFacProp n n.minFac
This theorem states that for every natural number `n` that is not equal to 1, the function `Nat.minFac` returns a number that has the property described by `Nat.minFacProp`. Specifically, this property is that the returned number is a prime factor of `n`, and is the smallest such factor.
More concisely: For every natural number `n` not equal to 1, there exists a prime factor `p` of `n` such that `p` = `Nat.minFac n`.
|
Nat.prime_two
theorem Nat.prime_two : Nat.Prime 2
The theorem `Nat.prime_two` asserts that the number 2 is a prime number. In the context of natural numbers, a prime number is defined as a natural number greater than or equal to 2 whose only divisors are itself and 1. Therefore, this theorem is confirming that 2, which is divisible only by itself and 1, satisfies this property and is therefore a prime number.
More concisely: The theorem `Nat.prime_two` asserts that 2 is a prime number in the natural numbers, i.e., it is a natural number greater than 1 that has no divisors other than 1 and itself.
|