smul_apply

Mathlib.Topology.Algebra.Module.Alternating.Basic

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

English

For any continuous alternating map f and any scalar c, the scaled map c · f evaluated at v equals c · f(v).

Русский

Для любой непрерывной чередующейся карты f и любого скаляра c верно: (c · f)(v) = c · f(v).

LaTeX

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

Lean4

theorem smul_apply (f : M [⋀^ι]→L[A] N) (c : R') (v : ι → M) : (c • f) v = c • f v :=
  rfl

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

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

Разделы

Аффилиация

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