dvd_mul_of_dvd_left

Mathlib.Algebra.Divisibility.Basic

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

English

If a divides b, then a divides b·c for any c.

Русский

Если a делит b, то a делит b·c для любого c.

LaTeX

$$$$a\mid b \Rightarrow a\mid (b\cdot c)$$$$

Lean4

theorem dvd_mul_of_dvd_left (h : a ∣ b) (c : α) : a ∣ b * c :=
  h.trans (dvd_mul_right b c)

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

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

Разделы

Аффилиация

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