alternatizeUncurryFinLM — Mathlib

English

The operation of scalar multiplication commutes with alternatizeUncurryFin: alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f.

Русский

Операция умножения на скаляр коммутирует с alternatizeUncurryFin: alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f.

LaTeX

$$$ alternatizeUncurryFin (c \cdot f) = c \cdot alternatizeUncurryFin f$$$

Lean4

/-- `AlternatingMap.alternatizeUncurryFin` as a linear map. -/
@[simps! apply]
def alternatizeUncurryFinLM : (M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) →ₗ[R] M [⋀^Fin (n + 1)]→ₗ[R] N
    where
  toFun := alternatizeUncurryFin
  map_add' := alternatizeUncurryFin_add
  map_smul' := alternatizeUncurryFin_smul

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