coprime_multiset_prod_left_iff — Mathlib

English

For a multiset m of naturals and k, Coprime m.prod k iff all elements n in m satisfy Coprime n k.

Русский

Для мультимножества m натуральных чисел и числа k, 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_multiset_prod_left_iff {m : Multiset ℕ} {k : ℕ} : Coprime m.prod k ↔ ∀ n ∈ m, Coprime n k := by
  induction m using Quotient.inductionOn; simpa using coprime_list_prod_left_iff

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