lcm_mono_fun

Mathlib.Algebra.GCDMonoid.Finset

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

English

If for all b ∈ s we have f(b) ∣ g(b), then s.lcm f ∣ s.lcm g.

Русский

Если для всех b∈s выполняется f(b) ∣ g(b), то s.lcm f ∣ s.lcm g.

LaTeX

$$$\Big(\forall b \in s, f(b) \mid g(b)\Big) \Rightarrow s.lcm f \mid s.lcm g$$$

Lean4

theorem lcm_mono_fun {g : β → α} (h : ∀ b ∈ s, f b ∣ g b) : s.lcm f ∣ s.lcm g :=
  lcm_dvd fun b hb ↦ (h b hb).trans (dvd_lcm hb)

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

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

Разделы

Аффилиация

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