mk_smul_linearMap_apply

Mathlib.Algebra.Module.LinearMap.Basic

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

English

For any a and f, (DomMulAct.mk a • f) x = f(a • x).

Русский

Для любого a и f, (DomMulAct.mk a • f) x = f(a • x).

LaTeX

$$ (DomMulAct.mk a • f)(x) = f(a • x) $$

Lean4

@[simp]
theorem _root_.DomMulAct.mk_smul_linearMap_apply (a : S') (f : M →ₛₗ[σ₁₂] M') (x : M) :
    (DomMulAct.mk a • f) x = f (a • x) :=
  rfl

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

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

Разделы

Аффилиация

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