smul_apply

Mathlib.LinearAlgebra.Multilinear.Basic

URI: https://scilib.ai/kg/mathlib#MultilinearMap.smul_apply

English

Evaluating the scaled map is the scalar times the evaluation: (c•f)(m) = c•f(m).

Русский

Оценка масштабированного отображения равна масштабированию значения: (c•f)(m) = c•f(m).

LaTeX

$$$ (c \cdot f) m = c \cdot f m$$$

Lean4

@[simp]
theorem smul_apply (f : MultilinearMap R M₁ M₂) (c : S) (m : ∀ i, M₁ i) : (c • f) m = c • f m :=
  rfl

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

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

Разделы

Аффилиация

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