coprime_list_prod_right_iff — Mathlib

English

For a multiset m of natural numbers, Coprime m.prod k iff every n in m is Coprime with k.

Русский

Для мультимножества m натуральных чисел Coprime m.prod k эквивалентно тому, что каждый элемент n из m удовлетворяет Coprime n k.

LaTeX

$$$\forall {m : Multiset \mathbb{N}} {k : \mathbb{N}}, \operatorname{Coprime}(m.\mathrm{prod}, k) \iff \forall n \in m, \operatorname{Coprime}(n, k)$$$

Lean4

theorem coprime_list_prod_right_iff {k : ℕ} {l : List ℕ} : Coprime k l.prod ↔ ∀ n ∈ l, Coprime k n := by
  simp_rw [coprime_comm (n := k), coprime_list_prod_left_iff]

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