dvd_add

Mathlib.Algebra.Ring.Divisibility.Basic

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

← MathLib Explorer

English

If d|x and d|y in a semiring, then d | x + y.

Русский

Если d делит x и d делит y в полусложном кольце, то d делит x+y.

LaTeX

$$$d|x \wedge d|y \Rightarrow d|(x+y)$$$

Lean4

theorem dvd_add [LeftDistribClass α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
  Dvd.elim h₁ fun d hd => Dvd.elim h₂ fun e he => Dvd.intro (d + e) (by simp [left_distrib, hd, he])

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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