alternatizeUncurryFin_smul — Mathlib

English

Relation between curryLeft and the original map up to scaling.

Русский

Связь между curryLeft и исходным отображением с учётом масштабирования на (n+1).

LaTeX

$$$\\text{alternatizeUncurryFin}(\\text{curryLeft} f) = (n+1) \\cdot f$$$

Lean4

@[simp]
theorem alternatizeUncurryFin_smul {S : Type*} [Monoid S] [DistribMulAction S F] [ContinuousConstSMul S F]
    [SMulCommClass 𝕜 S F] (c : S) (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) :
    alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f :=
  by
  ext v
  simp [alternatizeUncurryFin_apply, smul_comm _ c, Finset.smul_sum]

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