coprime_multiset_prod_right_iff — Mathlib

English

For a multiset m of naturals, Coprime x m.prod iff for every n in m, Coprime x n.

Русский

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

LaTeX

$$$\forall {m : Multiset \mathbb{N}} {x : \mathbb{N}}, Coprime x m.prod \iff \forall n \in m, Coprime x n$$$

Lean4

theorem coprime_multiset_prod_right_iff {k : ℕ} {m : Multiset ℕ} : Coprime k m.prod ↔ ∀ n ∈ m, Coprime k n := by
  induction m using Quotient.inductionOn; simpa using coprime_list_prod_right_iff

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