prod_dvd_of_isRelPrime — Mathlib

English

If the index set I is finite and the family s(i) is pairwise coprime and every s(i) divides z, then the product over all i divides z.

Русский

Если множество индексов I конечно, семейство s(i) взаимно простое попарно и каждый s(i) делится на z, то произведение по всем i делит z.

LaTeX

$$[Fintype I] (Pairwise (Function.onFun IsRelPrime s)) → (∀ i, s i ∣ z) → (Finset.univ.prod (fun x => s x)) ∣ z$$

Lean4

theorem prod_dvd_of_isRelPrime [Fintype I] (Hs : Pairwise (IsRelPrime on s)) (Hs1 : ∀ i, s i ∣ z) : (∏ x, s x) ∣ z :=
  Finset.prod_dvd_of_isRelPrime (Hs.set_pairwise _) fun i _ ↦ Hs1 i

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