prod_dvd_of_coprime

Mathlib.RingTheory.Coprime.Lemmas

URI: https://scilib.ai/kg/mathlib#Fintype.prod_dvd_of_coprime

← MathLib Explorer

English

The lemma is simp-annotated: IsCoprime (m : ℤ) n ↔ Nat.Coprime m n.

Русский

Лемма упрощения: IsCoprime (m : ℤ) n ⇔ Nat.Coprime m n.

LaTeX

$$$IsCoprime\ (m : \mathbb Z)\ n \iff Nat.Coprime\ m\ n$$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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