sub_comp

Mathlib.Algebra.Module.LinearMap.Defs

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

English

The subtraction inside the second factor distributes over composition: (g - f) ∘ h = g ∘ h - f ∘ h.

Русский

Внутри второй позиции композиции распределяется вычитание: (g - f) ∘ h = g ∘ h - f ∘ h.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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