dvd_gcd

Mathlib.Algebra.GCDMonoid.Finset

URI: https://scilib.ai/kg/mathlib#Finset.dvd_gcd

English

If a divides every f(b) for b ∈ s, then a divides s.gcd f.

Русский

Если a делит каждое f(b) на b ∈ s, то a делит s.gcd f.

LaTeX

$$$(\forall b \in s, a \mid f(b)) \Rightarrow a \mid s.gcd f$$$

Lean4

theorem dvd_gcd {a : α} : (∀ b ∈ s, a ∣ f b) → a ∣ s.gcd f :=
  dvd_gcd_iff.2

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

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

Разделы

Аффилиация

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