dvd_lcm_left

Mathlib.Data.PNat.Prime

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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