lsum_lsingle — Mathlib

English

The lsum with lsingle acts as the identity on the space of dfinsupps when coefficients are scalar-compatible.

Русский

LSum с lsingle действует как тождество на пространстве dfinsupp при совместимости скаляра.

LaTeX

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

Lean4

theorem lsum_lsingle [Semiring S] [∀ i, Module S (M i)] [∀ i, SMulCommClass R S (M i)] :
    lsum S (lsingle (R := R) (M := M)) = .id :=
  lhom_ext (lsum_single _ _)

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