Nat.Coprime.gcd_mul_left_cancel
theorem Nat.Coprime.gcd_mul_left_cancel : ∀ {k n : ℕ} (m : ℕ), k.Coprime n → (k * m).gcd n = m.gcd n
The theorem `Nat.Coprime.gcd_mul_left_cancel` states that for any natural numbers `k`, `n` and `m`, if `k` and `n` are coprime (their greatest common divisor is `1`), then the greatest common divisor of `k * m` and `n` is the same as the greatest common divisor of `m` and `n`. In other words, multiplying `m` with a number that is coprime to `n` does not change the greatest common divisor of `m` and `n`.
More concisely: If natural numbers `k`, `n`, and `m` are coprime, then the greatest common divisor of `k * m` and `n` equals the greatest common divisor of `m` and `n`.
|
Nat.coprime_one_left_eq_true
theorem Nat.coprime_one_left_eq_true : ∀ (n : ℕ), Nat.Coprime 1 n = True
The theorem states that for every natural number `n`, `n` is coprime with 1. In other words, the greatest common divisor (gcd) of 1 and any natural number `n` is 1. This is a general property of numbers, as the gcd of 1 and any number is always 1, hence every number is relatively prime to 1.
More concisely: For every natural number `n`, the greatest common divisor of `1` and `n` is equal to `1`.
|
Nat.Coprime.dvd_of_dvd_mul_left
theorem Nat.Coprime.dvd_of_dvd_mul_left : ∀ {k m n : ℕ}, k.Coprime m → k ∣ m * n → k ∣ n
The theorem `Nat.Coprime.dvd_of_dvd_mul_left` states that for any three natural numbers `k`, `m`, and `n`, if `k` and `m` are coprime (that is, their greatest common divisor is 1), and if `k` divides the product `m * n`, then `k` must also divide `n`. This is a property related to the concept of coprimality and divisibility in number theory.
More concisely: If `k` is coprime to `m` and `k` divides `m * n`, then `k` divides `n`.
|
Nat.Coprime.mul_right
theorem Nat.Coprime.mul_right : ∀ {k m n : ℕ}, k.Coprime m → k.Coprime n → k.Coprime (m * n)
This theorem states that for any three natural numbers `k`, `m`, and `n`, if `k` is coprime with `m` and `k` is coprime with `n`, then `k` is also coprime with the product of `m` and `n`. In other words, if the greatest common divisor (gcd) of `k` and `m` is 1, and the gcd of `k` and `n` is 1, then the gcd of `k` and `m*n` is also 1.
More concisely: If `k` is coprime to both `m` and `n`, then `k` is coprime to their product `m * n`.
|
Nat.coprime_iff_gcd_eq_one
theorem Nat.coprime_iff_gcd_eq_one : ∀ {m n : ℕ}, m.Coprime n ↔ m.gcd n = 1
This theorem states that for any two natural numbers `m` and `n`, the numbers `m` and `n` are coprime (or relatively prime) if and only if their greatest common divisor (gcd) equals 1. Here, two numbers are said to be coprime if they have no common divisor other than 1, which is precisely when their gcd is 1. Thus, this theorem establishes the equivalence between the notion of coprimality and the condition that the gcd is 1.
More concisely: Two natural numbers `m` and `n` are coprime if and only if their greatest common divisor equals 1.
|
Nat.Coprime.coprime_dvd_left
theorem Nat.Coprime.coprime_dvd_left : ∀ {m k n : ℕ}, m ∣ k → k.Coprime n → m.Coprime n
The theorem `Nat.Coprime.coprime_dvd_left` states that for any three natural numbers `m`, `k`, and `n`, if `m` divides `k` and `k` and `n` are coprime (meaning their greatest common divisor is 1), then `m` and `n` are also coprime. In other words, the property of being coprime is preserved under division. In the language of number theory, this theorem implies that if `m` is a factor of a number `k` that is coprime with another number `n`, then `m` must also be coprime with `n`.
More concisely: If natural numbers `m`, `k`, and `n` satisfy `m` divides `k` and `gcd(k, n) = 1`, then `gcd(m, n) = 1`.
|
Nat.coprime_div_gcd_div_gcd
theorem Nat.coprime_div_gcd_div_gcd : ∀ {m n : ℕ}, 0 < m.gcd n → (m / m.gcd n).Coprime (n / m.gcd n)
The theorem `Nat.coprime_div_gcd_div_gcd` states that for any two natural numbers `m` and `n`, if the greatest common divisor (gcd) of `m` and `n` is greater than zero, then the result of dividing `m` by the gcd of `m` and `n` and the result of dividing `n` by the gcd of `m` and `n` are coprime. In other words, the numbers obtained by dividing `m` and `n` by their gcd are relatively prime, that is, their greatest common divisor is 1.
More concisely: If the greatest common divisor of natural numbers `m` and `n` is positive, then `m` divided by their gcd and `n` divided by their gcd are coprime.
|
Nat.Coprime.coprime_dvd_right
theorem Nat.Coprime.coprime_dvd_right : ∀ {n m k : ℕ}, n ∣ m → k.Coprime m → k.Coprime n
The theorem `Nat.Coprime.coprime_dvd_right` states that for all natural numbers `n`, `m`, and `k`, if `n` divides `m` and `k` is coprime to `m` (i.e., the greatest common divisor of `k` and `m` is 1), then `k` is also coprime to `n` (i.e., the greatest common divisor of `k` and `n` is also 1). This expresses a property of coprime numbers in number theory, specifically addressing the scenario when a number `n` that divides another number `m` maintains coprimality with a number `k` if `k` is already coprime to `m`.
More concisely: If `n` divides `m`, and `k` is coprime to `m`, then `k` is coprime to `n`.
|
Nat.coprime_zero_left
theorem Nat.coprime_zero_left : ∀ (n : ℕ), Nat.Coprime 0 n ↔ n = 1
This theorem states that for any natural number `n`, `n` is coprime to 0 if and only if `n` is equal to 1. In other words, a natural number `n` and 0 are said to be relatively prime (i.e., their greatest common divisor (gcd) is 1) if `n` itself is equal to 1.
More concisely: A natural number `n` is coprime to 0 if and only if `n` equals 1.
|
Nat.Coprime.mul_dvd_of_dvd_of_dvd
theorem Nat.Coprime.mul_dvd_of_dvd_of_dvd : ∀ {m n a : ℕ}, m.Coprime n → m ∣ a → n ∣ a → m * n ∣ a
The theorem `Nat.Coprime.mul_dvd_of_dvd_of_dvd` states that for any three natural numbers `m`, `n`, and `a`, if `m` and `n` are coprime (i.e., the greatest common divisor of `m` and `n` is 1), and both `m` and `n` divide `a`, then the product of `m` and `n` also divides `a`. This theorem provides a condition under which the product of two numbers is a divisor of another number.
More concisely: If natural numbers `m` and `n` are coprime, and both `m` and `n` divide `a`, then `m * n` divides `a`.
|
Nat.coprime_comm
theorem Nat.coprime_comm : ∀ {n m : ℕ}, n.Coprime m ↔ m.Coprime n
The theorem `Nat.coprime_comm` states that for all natural numbers `n` and `m`, the property of `n` and `m` being coprime (or relatively prime), which is defined as their greatest common divisor (gcd) being 1, is commutative. In other words, `n` and `m` are coprime if and only if `m` and `n` are coprime. Thus, the order in which the numbers are considered does not affect whether or not they are coprime.
More concisely: The theorem `Nat.coprime_comm` asserts that for all natural numbers `n` and `m`, `n` and `m` are coprime if and only if `m` and `n` are coprime.
|
Nat.Coprime.dvd_of_dvd_mul_right
theorem Nat.Coprime.dvd_of_dvd_mul_right : ∀ {k n m : ℕ}, k.Coprime n → k ∣ m * n → k ∣ m
This theorem states that for any natural numbers `k`, `n`, and `m`, if `k` and `n` are coprime (i.e., their greatest common divisor is 1), and `k` divides the product of `m` and `n`, then `k` also divides `m`. In other words, if a number `k` shares no common factors with `n` other than 1, and `k` is a divisor of `m*n`, then `k` is necessarily a divisor of `m`.
More concisely: If `k` is coprime to `n` and `k` divides the product `m * n`, then `k` divides `m`.
|
Nat.Coprime.gcd_eq_one
theorem Nat.Coprime.gcd_eq_one : ∀ {m n : ℕ}, m.Coprime n → m.gcd n = 1
The theorem `Nat.Coprime.gcd_eq_one` states that for any two natural numbers `m` and `n`, if `m` and `n` are coprime (i.e., their greatest common divisor is 1), then the greatest common divisor of `m` and `n` is indeed 1. In mathematical terms, for all natural numbers `m` and `n`, if `gcd(m, n) = 1`, then it is guaranteed that `gcd(m, n) = 1`.
More concisely: If `m` and `n` are coprime natural numbers, then their greatest common divisor equals 1.
|
Nat.coprime_one_left
theorem Nat.coprime_one_left : ∀ (n : ℕ), Nat.Coprime 1 n
The theorem `Nat.coprime_one_left` asserts that for any natural number `n`, the number `n` and `1` are coprime. In other words, the greatest common divisor (gcd) of `n` and `1` is `1`, which is the definition of two numbers being coprime. This is a universal property of natural numbers as `1` is a unit in the ring of integers and has no other divisors apart from `1` and `-1`, making it coprime with every number.
More concisely: For every natural number n, the greatest common divisor of n and 1 is 1. (i.e. n and 1 are coprime.)
|
Nat.coprime_one_right
theorem Nat.coprime_one_right : ∀ (n : ℕ), n.Coprime 1
This theorem states that for every natural number `n`, `n` and `1` are coprime. The term "coprime" means that the greatest common divisor (gcd) of the two numbers is `1`. In other words, any natural number `n` shares no other common divisor with `1` except `1` itself.
More concisely: For every natural number `n`, `gcd(n, 1) = 1`.
|
Nat.Coprime.symm
theorem Nat.Coprime.symm : ∀ {n m : ℕ}, n.Coprime m → m.Coprime n
This theorem states that the property of two natural numbers being coprime is symmetric. In other words, if two natural numbers `n` and `m` are coprime (that is, their greatest common divisor (gcd) is 1), then swapping their order doesn't change their coprimality: `m` and `n` are also coprime.
More concisely: If natural numbers `n` and `m` are coprime, then `m` and `n` are also coprime.
|
Nat.Coprime.mul
theorem Nat.Coprime.mul : ∀ {m k n : ℕ}, m.Coprime k → n.Coprime k → (m * n).Coprime k
The theorem `Nat.Coprime.mul` states that for any natural numbers `m`, `k`, and `n`, if `m` and `k` are coprime (i.e., their greatest common divisor (gcd) is 1), and `n` and `k` are also coprime, then `m * n` and `k` are coprime. In other words, the product of two numbers each of which is coprime to a third number, is itself coprime to that third number.
More concisely: If `m` and `k`, as well as `n` and `k`, are pairwise coprime, then `m * n` and `k` are coprime.
|
Nat.coprime_zero_right
theorem Nat.coprime_zero_right : ∀ (n : ℕ), n.Coprime 0 ↔ n = 1
The theorem `Nat.coprime_zero_right` states that for any natural number `n`, `n` is coprime with zero if and only if `n` equals to one. In mathematical terms, this is saying that the greatest common divisor (gcd) of `n` and `0` is `1` if and only if `n` is `1`.
More concisely: The natural number `n` is coprime to zero if and only if `n` equals one. (equivalently, gcd(n, 0) = 1 if and only if n = 1)
|
Nat.Coprime.pow_left
theorem Nat.Coprime.pow_left : ∀ {m k : ℕ} (n : ℕ), m.Coprime k → (m ^ n).Coprime k
The theorem `Nat.Coprime.pow_left` states that for any natural numbers `m`, `k`, and `n`, if `m` and `k` are coprime (i.e., their greatest common divisor is 1), then `m` raised to the power `n` and `k` are also coprime. This captures the property of coprimeness being preserved under exponentiation of one of the numbers.
More concisely: If natural numbers `m` and `k` are coprime, then `m^n` and `k` are coprime for any natural number `n`.
|