PNat.gcd_comm
theorem PNat.gcd_comm : ∀ {m n : ℕ+}, m.gcd n = n.gcd m
This theorem states that the greatest common divisor (gcd) of two positive natural numbers is commutative. In other words, for any two positive natural numbers `m` and `n`, the gcd of `m` and `n` is the same as the gcd of `n` and `m`. This corresponds to the mathematical principle that the order of the numbers does not influence the outcome when computing the gcd, i.e., $\gcd(m, n) = \gcd(n, m)$.
More concisely: The theorem asserts that the gcd of two positive natural numbers is commutative, i.e., gcd(m, n) = gcd(n, m) for all positive natural numbers m and n.
|
PNat.gcd_eq_left_iff_dvd
theorem PNat.gcd_eq_left_iff_dvd : ∀ {m n : ℕ+}, m ∣ n ↔ m.gcd n = m
This theorem states that for any two positive natural numbers `m` and `n`, `m` divides `n` if and only if the greatest common divisor of `m` and `n` is `m`. In other words, a positive natural number `m` is a divisor of another positive natural number `n` if and only if the greatest common factor they share is `m`.
More concisely: A positive natural number `m` divides `n` if and only if their greatest common divisor equals `m`.
|
PNat.coprime_coe
theorem PNat.coprime_coe : ∀ {m n : ℕ+}, (↑m).Coprime ↑n ↔ m.Coprime n
The theorem `PNat.coprime_coe` states that for every pair of positive natural numbers `m` and `n`, `m` and `n` are coprime in the natural numbers if and only if `m` and `n` are coprime in the positive natural numbers. In other words, the property of being coprime is preserved when transitioning between the domains of natural numbers and positive natural numbers. In mathematical terms, two numbers are said to be coprime if their greatest common divisor (gcd) is 1.
More concisely: The theorem `PNat.coprime_coe` asserts that for all natural numbers `m` and `n`, `m` and `n` are coprime in the natural numbers if and only if they are coprime in the positive natural numbers, i.e., their greatest common divisor is 1.
|