instSMul

Mathlib.Topology.Algebra.Module.Alternating.Basic

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

English

Scalar multiplication commutes with evaluation: (c • f)(v) = c • f(v).

Русский

Умножение на скаляр commute с применением: (c • f)(v) = c • f(v).

LaTeX

$$$\\forall f : \\mathrm{ContinuousAlternatingMap}(M,N,\\iota),\\; \\forall c:\\, R',\\; (c \\cdot f)(v) = c \\cdot f(v)$$$

Lean4

instance : SMul R' (M [⋀^ι]→L[A] N) :=
  ⟨fun c f => ⟨c • f.1, (c • f.toAlternatingMap).map_eq_zero_of_eq⟩⟩

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

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

Разделы

Аффилиация

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