lcm_mono

Mathlib.Algebra.GCDMonoid.Multiset

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

English

If s1 ⊆ s2, then s1.lcm divides s2.lcm.

Русский

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

LaTeX

$$s1 ⊆ s2 → s1.lcm ∣ s2.lcm$$

Lean4

theorem lcm_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₁.lcm ∣ s₂.lcm :=
  lcm_dvd.2 fun _ hb ↦ dvd_lcm (h hb)

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

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

Разделы

Аффилиация

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