dvd_of_lcm_right_dvd

Mathlib.Algebra.GCDMonoid.Basic

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

English

If lcm(m,n) | c, then m | c.

Русский

Если lcm(m,n) делит c, то m делит c.

LaTeX

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

Lean4

theorem dvd_of_lcm_right_dvd (h : lcm a b ∣ c) : a ∣ c :=
  (dvd_lcm_left a b).trans h

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

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

Разделы

Аффилиация

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