dvd_lcm

Mathlib.Algebra.GCDMonoid.Finset

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

English

Let s be a finite set of indices and f: β → α. If b ∈ s, then f(b) divides the least common multiple s.lcm f.

Русский

Пусть s — конечное множество индексов и f: β → α. Если b принадлежит s, то f(b) делит число s.lcm f.

LaTeX

$$$\displaystyle b \in s \Rightarrow f(b) \mid s.lcm f$$$

Lean4

theorem dvd_lcm {b : β} (hb : b ∈ s) : f b ∣ s.lcm f :=
  lcm_dvd_iff.1 dvd_rfl _ hb

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

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

Разделы

Аффилиация

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