coprime_prod_left_iff — Mathlib

English

Let t be a finite set and s a function on t. Then Coprime (∏ i ∈ t, s i) x iff ∀ i ∈ t, Coprime (s i) x.

Русский

Пусть t конечное множество, s — функция на t. Тогда Coprime (произведение) с x равносильно тому, что ∀ i ∈ t, Coprime (s i) x.

LaTeX

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

Lean4

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

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