uncurryRight_apply

Mathlib.LinearAlgebra.Multilinear.Curry

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

← MathLib Explorer

English

Applying uncurryRight to inputs yields the evaluation at init m and last coordinate.

Русский

Применение uncurryRight к аргументам даёт значение на init m и m(last).

LaTeX

$$$$f.uncurryRight m = f (init m) (m (last n)).$$$$

Lean4

@[simp]
theorem uncurryRight_apply (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂))
    (m : ∀ i, M i) : f.uncurryRight m = f (init m) (m (last n)) :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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