sum_smul_index_linearMap' — Mathlib

English

For a semilinear family h, the scalar c acts on the sum by pulling out σ(c) from the scalar to the sum.

Русский

Для семейства полупрорефирований h скаляр c действует через отображение σ на сумму, вытягивая σ(c) за пределы суммы.

LaTeX

$$$$ (c \cdot v).sum h = \sigma(c) \cdot v.sum h. $$$$

Lean4

theorem sum_smul_index_linearMap' [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂]
    {v : α →₀ M} {c : R} {h : α → M →ₗ[R] M₂} : ((c • v).sum fun a => h a) = c • v.sum fun a => h a :=
  sum_smul_index_semilinearMap'

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