English
Let s be a finite set of indices, and f a function from these indices to a Cancel–CommMonoidWithZero α which is also a NormalizedGCDMonoid. If a is an element of α that is a multiple of every f(b) with b in s, then the least common multiple of the family {f(b) | b ∈ s} divides a.
Русский
Пусть s — конечное множество индексов, и f: β → α. Если для некоторого a ∈ α верно, что a является кратным каждого f(b) для слабоведения b ∈ s, тогда наименьшее общее кратное семейства {f(b) | b ∈ s} делит a.
LaTeX
$$$\displaystyle \forall a:\alpha,\;\Big(\forall b\in s\; f(b) \mid a\Big) \Rightarrow s.lcm f \mid a$$$
Lean4
theorem lcm_dvd {a : α} : (∀ b ∈ s, f b ∣ a) → s.lcm f ∣ a :=
lcm_dvd_iff.2
