prod_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prod_left : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x := by
  classical
  refine Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_
  rw [Finset.prod_insert hbt]
  rw [Finset.forall_mem_insert] at H
  exact H.1.mul_left (ih H.2)

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