alternatizeUncurryFinCLM_apply — Mathlib

English

The CLM construction and the uncurry construction produce the same map when applied to f.

Русский

Конструкция CLM совпадает с конструкцией uncurry при применении к f.

LaTeX

$$$\\text{alternatizeUncurryFinCLM}_{\\mathbb{k},E,F} f = \\text{alternatizeUncurryFin} f$$$

Lean4

@[simp]
theorem alternatizeUncurryFinCLM_apply (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) :
    alternatizeUncurryFinCLM 𝕜 E F f = alternatizeUncurryFin f :=
  rfl

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