alternatizeUncurryFin_smul — Mathlib

English

The construction alternatizeUncurryFinLM packages alternatizeUncurryFin as a linear map between endomorphism spaces, i.e., a linear map LM that takes a linear map f and returns AlternatingMap on Fin(n+1).

Русский

Конструкция alternatizeUncurryFinLM оформляет AlternatingMap как линейное отображение между пространствами линейных отображений, т.е. линейное отображение LM, принимающее f и возвращающее чередующее отображение на Fin(n+1).

LaTeX

$$$ alternatizeUncurryFinLM : (M \to_{R} M [⋀^{Fin n}]\to_{R} N) \to_{R} (M [⋀^{Fin (n+1)}] \to_{R} N)$$$

Lean4

@[simp]
theorem alternatizeUncurryFin_smul (c : S) (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
    alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f :=
  by
  ext v
  simp [alternatizeUncurryFin_apply, smul_comm _ c, Finset.smul_sum]

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