dvd_of_lcm_left_dvd

Mathlib.Algebra.GCDMonoid.Basic

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

English

Let p be a prime in a gcd-monoid α. If p divides lcm(a,b), then p divides a or p divides b.

Русский

Пусть p — простое в gcd-монойде α. Если p делит lcm(a,b), то p делит a или p делит b.

LaTeX

$$$$ \\text{Prime } p: \\ p \\mid \\operatorname{lcm}(a,b) \\Rightarrow p \\mid a \\text{ or } p \\mid b. $$$$

Lean4

theorem dvd_of_lcm_left_dvd (h : lcm a b ∣ c) : b ∣ c :=
  (dvd_lcm_right a b).trans h

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

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

Разделы

Аффилиация

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