prod_right — Mathlib

English

If x is coprime with each s(i), then x is coprime with the product ∏_{i∈t} s(i).

Русский

Если x взаимно просто с каждым s(i), то x взаимно просто с произведением ∏_{i∈t} s(i).

LaTeX

$$(∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)$$

Lean4

theorem prod_right : (∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i) := by
  simpa only [isRelPrime_comm] using IsRelPrime.prod_left (α := α)

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