Finset.prod_dvd_of_coprime
theorem Finset.prod_dvd_of_coprime :
∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {z : R} {s : I → R} {t : Finset I},
(↑t).Pairwise (IsCoprime on s) → (∀ i ∈ t, s i ∣ z) → (t.prod fun x => s x) ∣ z
The theorem `Finset.prod_dvd_of_coprime` states that for any type `R` with a commutative semiring structure, any type `I`, any `z` of type `R`, any function `s` from `I` to `R`, and any finite set `t` of type `I`, if the function `s` induces pairwise coprime elements on the set `t` and each element of `s i` for `i` in `t` divides `z`, then the product of `s x` for `x` in `t` also divides `z`. This means, if we have a finite set of elements which are pairwise coprime (i.e., any two distinct elements have no common divisors other than 1) and each of these elements divides a given number, then their product also divides that number.
More concisely: Let `R` be a commutative semiring, `I` a type, `z` an element of `R`, `s : I -> R`, and `t` a finite set of pairwise coprime elements of `I` such that `s i` divides `z` for all `i` in `t`, then `∏(s x for x in t)` divides `z`.
|
IsCoprime.nat_coprime
theorem IsCoprime.nat_coprime : ∀ {m n : ℕ}, IsCoprime ↑m ↑n → m.Coprime n
This theorem states that for all natural numbers `m` and `n`, if `m` and `n` (when cast to a commutative semiring) are coprime, then `m` and `n` are coprime in the natural numbers. Here, two numbers being coprime is defined as the existence of two other numbers such that their linear combination equals 1. Note that the theorem only states the forward direction of the equivalence between the natural number coprimality and the general coprimality in a commutative semiring.
More concisely: If `m` and `n` are natural numbers that are coprime in the sense of being coprime in any commutative semiring, then they are coprime as natural numbers.
|
Int.isCoprime_iff_gcd_eq_one
theorem Int.isCoprime_iff_gcd_eq_one : ∀ {m n : ℤ}, IsCoprime m n ↔ m.gcd n = 1
This theorem states that for any two integers `m` and `n`, `m` and `n` are coprime (i.e., there exist integers `a` and `b` such that `a * m + b * n = 1`) if and only if the greatest common divisor of `m` and `n` is 1. In other words, two integers are coprime if their greatest common divisor is 1, and if two integers are coprime, their greatest common divisor must be 1.
More concisely: Two integers `m` and `n` are coprime if and only if their greatest common divisor equals 1.
|
Nat.Coprime.isCoprime
theorem Nat.Coprime.isCoprime : ∀ {m n : ℕ}, m.Coprime n → IsCoprime ↑m ↑n
This theorem, `Nat.Coprime.isCoprime`, is essentially an alias of the reverse direction of another theorem, `Nat.isCoprime_iff_coprime`. It states that for all natural numbers `m` and `n`, if `m` and `n` are coprime (that is, their greatest common divisor is 1), then `m` and `n` satisfy the property `IsCoprime`. In terms of mathematics, if `m` and `n` are coprime natural numbers, there exist integers `a` and `b` such that `a * m + b * n = 1`, which is the definition of `IsCoprime`.
More concisely: If natural numbers `m` and `n` are coprime, then `m` and `n` have no common positive divisor besides 1, or equivalently, there exist integers `a` and `b` such that `a * m + b * n = 1`.
|
IsCoprime.prod_right
theorem IsCoprime.prod_right :
∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {x : R} {s : I → R} {t : Finset I},
(∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (t.prod fun i => s i)
The theorem `IsCoprime.prod_right` states that for any given type `R` with a commutative semiring structure, a type `I`, an element `x` of type `R`, a function `s` from `I` to `R`, and a finite set `t` of elements of type `I`, if for every element `i` in `t`, `x` and `s i` are coprime (that is, there exist elements `a` and `b` such that `a * x + b * s i = 1`), then `x` is also coprime with the product of `s i` as `i` ranges over the elements of `t` (denoted as ∏ `i` in `t`, `s i`). In other words, if a number is coprime with all elements of a set, it is also coprime with the product of the elements of the set.
More concisely: If `x` is coprime to every `s i` in the finite set `t`, then `x` is coprime to the product of `s i` as `i` ranges over `t`.
|