currySum_add

Mathlib.LinearAlgebra.Multilinear.Curry

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

English

Applying uncurrySum to currySum returns the original multilinear map: uncurrySum (currySum f) = f.

Русский

Применение uncurrySum к currySum даёт исходное много-линейное отображение: uncurrySum (currySum f) = f.

LaTeX

$$$\\text{uncurrySum}(\\text{currySum}(f)) = f$$$

Lean4

@[simp]
theorem currySum_add (f₁ f₂ : MultilinearMap R N M₂) : currySum (f₁ + f₂) = currySum f₁ + currySum f₂ :=
  rfl

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

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

Разделы

Аффилиация

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