prod_left_iff — Mathlib

English

The product ∏_{i∈t} s(i) is coprime to x iff every s(i) is coprime to x.

Русский

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

LaTeX

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

Lean4

theorem prod_left_iff : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x := by
  classical
  refine Finset.induction_on t (iff_of_true isRelPrime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
  rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]

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