lsum_piSingle — Mathlib

English

The value of linear sum on a given index equals the sum over i of the i-th component evaluated at the projection onto i.

Русский

Значение линейной суммы на данном индексе равно сумме по i от i-й компоненты, взятой на проекции на i.

LaTeX

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

Lean4

theorem lsum_piSingle (S) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M]
    (f : (i : ι) → φ i →ₗ[R] M) (i : ι) (x : φ i) : lsum R φ S f (Pi.single i x) = f i x := by
  simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']

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