smul_comp

Mathlib.Algebra.Module.LinearMap.Defs

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

English

The scalar action commutes with composition on the left: g ∘ (a • f) = a • (g ∘ f).

Русский

Скалярное действие слева commuting with composition: g ∘ (a • f) = a • (g ∘ f).

LaTeX

$$g.comp (instHSMul.hSMul a f) = instHSMul.hSMul a (g.comp f)$$

Lean4

theorem smul_comp (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) : (a • g).comp f = a • g.comp f :=
  rfl

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

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

Разделы

Аффилиация

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