dvd_lcm_of_dvd_right

Mathlib.Data.Nat.GCD.Basic

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

English

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

Русский

Если a делится на b, то a делится на lcm(c,b) для любого c.

LaTeX

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

Lean4

theorem dvd_lcm_of_dvd_right {a b : ℕ} (h : a ∣ b) (c : ℕ) : a ∣ lcm c b :=
  h.trans (dvd_lcm_right c b)

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

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

Разделы

Аффилиация

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