coprime_fintype_prod_right_iff — Mathlib

English

If a finite type ι is given, then Coprime x (∏ i, s i) iff ∀ i, Coprime x (s i).

Русский

Для конечного типа ι: Coprime x (произведение по i) эквивалентно ∀ i, Coprime x (s i).

LaTeX

$$$[Fintype ι] \implies \operatorname{Coprime}\left(x, \prod_{i} s(i)\right) \iff \forall i, \operatorname{Coprime}(x, s(i))$$$

Lean4

theorem coprime_fintype_prod_right_iff [Fintype ι] {x : ℕ} {s : ι → ℕ} : Coprime x (∏ i, s i) ↔ ∀ i, Coprime x (s i) :=
  by simp [coprime_prod_right_iff]

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