curryLeft_add

Mathlib.LinearAlgebra.Alternating.Curry

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

English

CurryLeft is additive: curryLeft(f+g) = curryLeft f + curryLeft g.

Русский

CurryLeft сохраняет сложение: curryLeft(f+g) = curryLeft f + curryLeft g.

LaTeX

$$$\\text{curryLeft}(f+g) = \\text{curryLeft}(f) + \\text{curryLeft}(g)$$$

Lean4

@[simp]
theorem curryLeft_add (f g : M [⋀^Fin n.succ]→ₗ[R] N) : curryLeft (f + g) = curryLeft f + curryLeft g :=
  rfl

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

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

Разделы

Аффилиация

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