lcm_dvd_mul

Mathlib.Algebra.GCDMonoid.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lcm_dvd_mul : lcm m n ∣ m * n :=
  lcm_dvd (by simp) (by simp)

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

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

Разделы

Аффилиация

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