dvd_lcm_of_dvd_left

Mathlib.Algebra.GCDMonoid.Basic

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

English

If a | b, then a | lcm(b,c) in a gcd-monoid.

Русский

Если a делит b, то a делит lcm(b,c) в gcd-монойде.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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