curryLeft_apply — Mathlib

English

There is a canonical linear equivalence between multilinear maps in n+1 variables and linear maps into multilinear maps in n variables obtained by separating the first variable.

Русский

Существуют канонические линейные эквивалентности между много-линейными отображениями в n+1 переменных и линейными отображениями в n переменных после отделения первой переменной.

LaTeX

$$$$MultilinearMap\;M\;M_2 \cong_l[R] M_0 \to MultilinearMap R (fun i => M_i.succ) M_2.$$$$

Lean4

@[simp]
theorem curryLeft_apply (f : MultilinearMap R M M₂) (x : M 0) (m : ∀ i : Fin n, M i.succ) :
    f.curryLeft x m = f (cons x m) :=
  rfl

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