curryLeftLinearMap — Mathlib

English

The curryLeft construction itself is a linear map from alternating maps to linear maps between the appropriate spaces.

Русский

Конструкция curryLeft сама является линейным отображением между пространствами.

LaTeX

$$$\\text{curryLeftLinearMap} : (M [⋀^Fin n.succ]→ₗ[R] N) \\to_ℓ[R] (M →ₗ[R] (M [⋀^Fin n]→ₗ[R] N))$$$

Lean4

/-- `AlternatingMap.curryLeft` as a `LinearMap`. This is a separate definition as dot notation
does not work for this version. -/
@[simps]
def curryLeftLinearMap : (M [⋀^Fin n.succ]→ₗ[R] N) →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
    where
  toFun f := f.curryLeft
  map_add' := curryLeft_add
  map_smul' := curryLeft_smul

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