Nat.Coprime.prod_left
theorem Nat.Coprime.prod_left :
∀ {ι : Type u_1} {t : Finset ι} {s : ι → ℕ} {x : ℕ}, (∀ i ∈ t, (s i).Coprime x) → (t.prod fun i => s i).Coprime x
This theorem states that for any type `ι`, any finite set `t` of `ι`, any function `s` mapping `ι` to natural numbers, and any natural number `x`, if every element of `t` mapped through `s` is coprime with `x`, then the product of all elements of `t` through the function `s` is also coprime with `x`. In mathematical terms, if for any \(i \in t\), \(\gcd(s(i),x) = 1\), then we have \(\gcd(\prod_{i \in t} s(i), x) = 1\).
More concisely: If the greatest common divisor of each element and a natural number `x` in a finite set is 1, then the greatest common divisor of their product and `x` is also 1.
|
Nat.coprime_list_prod_right_iff
theorem Nat.coprime_list_prod_right_iff : ∀ {k : ℕ} {l : List ℕ}, k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n
The theorem states that for any natural number 'k' and any list of natural numbers 'l', 'k' is coprime with the product of all the numbers in 'l' if and only if 'k' is coprime with every individual number 'n' in the list 'l'. In other words, 'k' shares no common divisors other than 1 with the product of the numbers in 'l' precisely when 'k' shares no common divisors other than 1 with each number in 'l'.
More concisely: A natural number 'k' is coprime with the product of a list of natural numbers 'l' if and only if it is coprime with every number in the list.
|
Nat.Coprime.prod_right
theorem Nat.Coprime.prod_right :
∀ {ι : Type u_1} {x : ℕ} {t : Finset ι} {s : ι → ℕ}, (∀ i ∈ t, x.Coprime (s i)) → x.Coprime (t.prod fun i => s i)
This theorem in Lean 4 states that for any type `ι`, natural number `x`, finite set `t` of type `ι`, and function `s` from `ι` to ℕ, if `x` is coprime to each natural number `s i` for all `i` in `t`, then `x` is also coprime to the product of all `s i` for each `i` in `t`. This mirrors the mathematical property that coprimality is preserved under finite product, i.e., if a number is coprime to each number in a set, it is also coprime to their product.
More concisely: If a natural number `x` is coprime to each `s i` in the finite set `t` of natural numbers, then `x` is coprime to the product of all `s i` in `t`.
|