prod_left — Mathlib

English

If the product ∏ s_i is coprime to x, then each s_i is coprime to x.

Русский

Если произведение ∏ s_i взаимно простое с x, то каждый s_i взаимно прост с x.

LaTeX

$$$IsCoprime\ (\prod i\in t\, s_i)\ x \Rightarrow \forall i\in t, IsCoprime\ (s_i)\ x$$$

Lean4

theorem prod_left (h : ∀ i ∈ t, IsCoprime (s i) x) : IsCoprime (∏ i ∈ t, s i) x := by
  induction t using Finset.cons_induction with
  | empty => apply isCoprime_one_left
  | cons b t hbt ih =>
    rw [Finset.prod_cons]
    rw [Finset.forall_mem_cons] at h
    exact h.1.mul_left (ih h.2)

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