add_right

Mathlib.Algebra.Ring.Commute

URI: https://scilib.ai/kg/mathlib#Commute.add_right

English

If a commutes with b and with c, then a commutes with b + c.

Русский

Если a коммутирует с b и с c, то a коммутирует с b + c.

LaTeX

$$$\\text{Commute } a b \\to \\text{Commute } a c \\to \\text{Commute } a (b+c)$$$

Lean4

@[simp]
theorem add_right [Distrib R] {a b c : R} : Commute a b → Commute a c → Commute a (b + c) :=
  SemiconjBy.add_right

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

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

Разделы

Аффилиация

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