linear_comb

Mathlib.Algebra.Ring.Divisibility.Basic

URI: https://scilib.ai/kg/mathlib#Dvd.dvd.linear_comb

English

If d|x and d|y in a commutative semiring, then d | a x + b y for any a, b.

Русский

Если d делит x и y в коммутативном полугруппе, то d делит a x + b y для любых a, b.

LaTeX

$$$d|x \Rightarrow d| (a x + b y)$ зафиксировано для любых a,b$$

Lean4

theorem linear_comb {d x y : α} (hdx : d ∣ x) (hdy : d ∣ y) (a b : α) : d ∣ a * x + b * y :=
  dvd_add (hdx.mul_left a) (hdy.mul_left b)

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

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

Разделы

Аффилиация

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