dvd_lcm_right

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.dvd_lcm_right

English

For positive integers n and m, m divides the least common multiple of n and m.

Русский

Для положительных чисел n и m, m делит наименьшее общее кратное n и m.

LaTeX

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

Lean4

theorem dvd_lcm_right (n m : ℕ+) : m ∣ lcm n m :=
  dvd_iff.2 (Nat.dvd_lcm_right (n : ℕ) (m : ℕ))

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

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

Разделы

Аффилиация

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