lcm_dvd_lcm_mul_left_right

Mathlib.Algebra.GCDMonoid.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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