lcm_mono

Mathlib.Algebra.GCDMonoid.Finset

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

English

If s1 is a subset of s2, then s1.lcm f divides s2.lcm f.

Русский

Если s1 ⊆ s2, то s1.lcm f делит s2.lcm f.

LaTeX

$$$s_1 \subseteq s_2 \Rightarrow s_1.lcm f \mid s_2.lcm f$$$

Lean4

theorem lcm_mono (h : s₁ ⊆ s₂) : s₁.lcm f ∣ s₂.lcm f :=
  lcm_dvd fun _ hb ↦ dvd_lcm (h hb)

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

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

Разделы

Аффилиация

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