uncurryLeft_apply — Mathlib

English

Uncurrying converts a linear map into a multilinear map by fixing the first argument and treating the rest as a multilinear map.

Русский

Развёртывание превращает линейное отображение в много-линейное, фиксируя первый аргумент.

LaTeX

$$uncurryLeft : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂ → MultilinearMap R M M₂$$

Lean4

@[simp]
theorem uncurryLeft_apply (f : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂) (m : ∀ i, M i) :
    f.uncurryLeft m = f (m 0) (tail m) :=
  rfl

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