dvd_lcm_left

Mathlib.Algebra.GCDMonoid.Basic

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

English

For any a and b in α, a divides lcm(a,b).

Русский

Для любых a и b из α, a делит lcm(a,b).

LaTeX

$$$ a \mid \operatorname{lcm}(a,b) $$$

Lean4

theorem dvd_lcm_left [GCDMonoid α] (a b : α) : a ∣ lcm a b :=
  (lcm_dvd_iff.1 (dvd_refl (lcm a b))).1

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

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

Разделы

Аффилиация

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