smul_linearMap_apply

Mathlib.Algebra.Module.LinearMap.Basic

URI: https://scilib.ai/kg/mathlib#DomMulAct.smul_linearMap_apply

English

For a DomMulAct action a and a σ-linear map f, we have (a • f) x = f (a • x) for all x.

Русский

Для действия DomMulAct и σ-линейного отображения f выполняется (a • f) x = f (a • x) для всех x.

LaTeX

$$(a \cdot f)(x) = f(a \cdot x)$$

Lean4

theorem _root_.DomMulAct.smul_linearMap_apply (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') (x : M) :
    (a • f) x = f (DomMulAct.mk.symm a • x) :=
  rfl

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

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

Разделы

Аффилиация

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