sigmaFinsuppEquivDFinsupp_smul — Mathlib

English

The action of a scalar on f translates through sigmaFinsuppEquivDFinsupp: applying the smul to f corresponds to smul on the image.

Русский

Скалярное умножение на f через sigmaFinsuppEquivDFinsupp соответствует скаляру на образе.

LaTeX

$$$\\sigmaFinsuppEquivDFinsupp (r \\cdot f) = r \\cdot \\sigmaFinsuppEquivDFinsupp f$$$

Lean4

@[simp]
theorem sigmaFinsuppEquivDFinsupp_smul {R} [Monoid R] [AddMonoid N] [DistribMulAction R N] (r : R)
    (f : (Σ i, η i) →₀ N) : sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f :=
  by
  ext
  rfl

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