toAlternatingMap_smul — Mathlib

English

Let c be a scalar and f a continuous alternating map. Then applying the scalar to f and then converting to an alternating map is the same as applying the scalar to the alternating map of f: (c · f).toAlternatingMap = c · f.toAlternatingMap.

Русский

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

LaTeX

$$$ (c \\cdot f).toAlternatingMap = c \\cdot f.toAlternatingMap $$$

Lean4

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

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