finsuppSum_mem — Mathlib

English

A standard finitary sum of finitely supported elements lies in a submodule provided each summand lies in the submodule when its coefficient is nonzero.

Русский

Сумма по finitely supported элементам принадлежит подмодулю, если каждый ненулевой вклад лежит в подмодуле.

LaTeX

$$\forall {ι β} [Zero β] (S : Submodule R M) (f : ι →_0 β) (g : ι → β → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S), f.sum g ∈ S$$

Lean4

protected theorem finsuppSum_mem {ι β : Type*} [Zero β] (S : Submodule R M) (f : ι →₀ β) (g : ι → β → M)
    (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
  AddSubmonoidClass.finsuppSum_mem S f g h

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