neg_comp

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.neg_comp

English

The negation commutes with composition on the right: (-g).comp f = - (g.comp f).

Русский

Отрицание отображения г коммутирует слева с композицией: (-g).comp f = - (g.comp f).

LaTeX

$$(-g).comp f = - g.comp f$$

Lean4

@[simp]
theorem neg_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) : (-g).comp f = -g.comp f :=
  rfl

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

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

Разделы

Аффилиация

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