lsum_apply — Mathlib

English

Applying lsum to a family f and base objects shows the equality with the coordinate-wise description of the sum.

Русский

Применение lsum к семейству отображений даёт равенство с координатным описанием суммы.

LaTeX

$$$\\text{lsum } R \\; \\varphi \\; S \\; f = \\sum_{i}\\; (f_i) \\circ \\mathrm{proj}_i.$$$

Lean4

@[simp]
theorem lsum_apply (S) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M]
    (f : (i : ι) → φ i →ₗ[R] M) : lsum R φ S f = ∑ i : ι, (f i).comp (proj i) :=
  rfl

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