coprime_list_prod_left_iff — Mathlib

English

For a list l of natural numbers and k, Coprime l.prod k iff every n in l is Coprime with k.

Русский

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

LaTeX

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

Lean4

theorem coprime_list_prod_left_iff {l : List ℕ} {k : ℕ} : Coprime l.prod k ↔ ∀ n ∈ l, Coprime n k := by
  induction l <;> simp [Nat.coprime_mul_iff_left, *]

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