instAddSemigroup

Mathlib.LinearAlgebra.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.instAddSemigroup

← MathLib Explorer

English

The addition on LinearPMap is associative: (f+g)+h = f+(g+h).

Русский

Сложение на LinearPMap ассоциативно: (f+g)+h = f+(g+h).

LaTeX

$$$(f + g) + h = f + (g + h)$$$

Lean4

instance instAddSemigroup : AddSemigroup (E →ₗ.[R] F) :=
  ⟨fun f g h => by
    ext x y hxy
    · simp only [add_domain, inf_assoc]
    · simp only [add_apply, add_assoc]⟩

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

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

Разделы

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

Аффилиация

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