lsum_single — Mathlib

English

The linear equivalence lsum with lsingle is the standard linear iso between DFinsupp and the product form.

Русский

Линейное эквивалентное отображение lsum вместе с lsingle является стандартным линейным взаимодиском между DFinsupp и производной формой.

LaTeX

$$$\\mathrm{lsum}\\; S \\; (\\mathrm{lsingle}\\; (R := R) (M := M)) = \\mathrm{id}$$$

Lean4

/-- While `simp` can prove this, it is often convenient to avoid unfolding `lsum` into `sumAddHom`
with `DFinsupp.lsum_apply_apply`. -/
theorem lsum_single [Semiring S] [Module S N] [SMulCommClass R S N] (F : ∀ i, M i →ₗ[R] N) (i) (x : M i) :
    lsum S F (single i x) = F i x := by simp

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