toContinuousMultilinearMap_smul — Mathlib

English

Let f be a continuous alternating map; then converting the scalar-multiplied map to a continuous multilinear map commutes with the scalar: toContinuousMultilinearMap(c · f) = c · toContinuousMultilinearMap(f).

Русский

Пусть f — непрерывное чередующееся отображение; переход к соответствующей мультилитерной карте сохраняет умножение на скаляры: toContinuousMultilinearMap(c · f) = c · toContinuousMultilinearMap(f).

LaTeX

$$$ \operatorname{toContinuousMultilinearMap}(c \cdot f) = c \cdot \operatorname{toContinuousMultilinearMap}(f) $$$

Lean4

@[simp]
theorem toContinuousMultilinearMap_smul (c : R') (f : M [⋀^ι]→L[A] N) :
    (c • f).toContinuousMultilinearMap = c • f.toContinuousMultilinearMap :=
  rfl

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