dvd_lcm_of_dvd_left

Mathlib.Data.Nat.GCD.Basic

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

English

If a divides b, then a divides lcm(b,c) for any c.

Русский

Если a делится на b, то a делится на произведение на наименьшем общего кратном lcm(b,c) для любого c.

LaTeX

$$$a \mid b \Rightarrow a \mid \mathrm{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