coprime_prod_right_iff — Mathlib

English

For x, t, s, Coprime x (∏ i ∈ t, s i) iff ∀ i ∈ t, Coprime x (s i).

Русский

Для x, t, s: Coprime x (∏ i ∈ t, s i) эквивалентно ∀ i ∈ t, Coprime x (s i).

LaTeX

$$$\forall {x} {t : Finset \iota} {s : \iota \to \mathbb{N}}, \operatorname{Coprime}\left(x, \prod_{i\in t} s(i)\right) \iff \forall i \in t, \operatorname{Coprime}(x, s(i))$$$

Lean4

theorem coprime_prod_right_iff {x : ℕ} {t : Finset ι} {s : ι → ℕ} :
    Coprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, Coprime x (s i) := by
  simpa using coprime_multiset_prod_right_iff (m := t.val.map s)

Похожие утверждения