of_prod_left

Mathlib.RingTheory.Coprime.Lemmas

URI: https://scilib.ai/kg/mathlib#IsRelPrime.of_prod_left

English

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

Русский

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

LaTeX

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

Lean4

theorem of_prod_left (H1 : IsRelPrime (∏ i ∈ t, s i) x) (i : I) (hit : i ∈ t) : IsRelPrime (s i) x :=
  IsRelPrime.prod_left_iff.1 H1 i hit

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru