coe_currySumEquiv

Mathlib.LinearAlgebra.Multilinear.Curry

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

English

The currySum equivalence is symmetric with its inverse uncurrySum.

Русский

Эквивалентность currySum симметрична по отношению к обратному uncurrySum.

LaTeX

$$$\\text{currySumEquiv}^{-1} = \\text{uncurrySum}$$$

Lean4

@[simp]
theorem coe_currySumEquiv : ⇑(currySumEquiv (R := R) (N := N) (M₂ := M₂)) = currySum :=
  rfl

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

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

Разделы

Аффилиация

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