lcm_dvd_lcm_mul_right_right

Mathlib.Algebra.GCDMonoid.Basic

URI: https://scilib.ai/kg/mathlib#lcm_dvd_lcm_mul_right_right

English

In a gcd-monoid α, for all m, n, k ∈ α, lcm(m,n) divides lcm(m, n·k).

Русский

В gcd-монойде α для любых m, n, k верно lcm(m,n) делит lcm(m, n·k).

LaTeX

$$$$ \\forall m,n,k \\in \\alpha:\\, \\operatorname{lcm}(m,n) \\mid \\operatorname{lcm}(m, n k). $$$$

Lean4

theorem lcm_dvd_lcm_mul_right_right [GCDMonoid α] (m n k : α) : lcm m n ∣ lcm m (n * k) :=
  lcm_dvd_lcm dvd_rfl (dvd_mul_right _ _)

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

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

Разделы

Аффилиация

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