lcm_dvd_lcm_mul_left — Mathlib

English

Let α be a gcd-monoid. For all m, n, k in α, the least common multiple of m and n divides the least common multiple of k·m and n.

Русский

Пусть α — gcd-монойд. Тогда для любых m, n, k в α наименьшее общее кратное m и n делит наименьшее общее кратное 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 [GCDMonoid α] (m n k : α) : lcm m n ∣ lcm (k * m) n :=
  lcm_dvd_lcm (dvd_mul_left _ _) dvd_rfl

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