curryLeft_smul

Mathlib.LinearAlgebra.Alternating.Curry

URI: https://scilib.ai/kg/mathlib#AlternatingMap.curryLeft_smul

English

CurryLeft is linear with respect to scalars: curryLeft(r • f) = r • curryLeft f.

Русский

CurryLeft линейна по скаляру: curryLeft(r • f) = r • curryLeft f.

LaTeX

$$$\\text{curryLeft}(r \\cdot f) = r \\cdot \\text{curryLeft}(f)$$$

Lean4

@[simp]
theorem curryLeft_smul (r : R) (f : M [⋀^Fin n.succ]→ₗ[R] N) : curryLeft (r • f) = r • curryLeft f :=
  rfl

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

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

Разделы

Аффилиация

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