add_left

Mathlib.Algebra.Ring.Semiconj

URI: https://scilib.ai/kg/mathlib#SemiconjBy.add_left

← MathLib Explorer

English

If SemiconjBy a x y and SemiconjBy b x y, then SemiconjBy (a+b) x y.

Русский

Если SemiconjBy a x y и SemiconjBy b x y, то SemiconjBy (a+b) x y.

LaTeX

$$$ (SemiconjBy a x y) \land (SemiconjBy b x y) \Rightarrow SemiconjBy (a+b) x y $$$

Lean4

@[simp]
theorem add_left [Distrib R] {a b x y : R} (ha : SemiconjBy a x y) (hb : SemiconjBy b x y) : SemiconjBy (a + b) x y :=
  by simp only [SemiconjBy, left_distrib, right_distrib, ha.eq, hb.eq]

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

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

Разделы

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

Аффилиация

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