dfinsuppSumAddHom_mem — Mathlib

English

Analogous statement for sumAddHom: the dfinsupp sum lands in S under the analogous hypotheses.

Русский

Аналогично для sumAddHom: dfinsuppSumAddHom принадлежит S при соответствующих предположениях.

LaTeX

$$$\\mathrm{DFinsupp.sumAddHom}\\; g\\; f ∈ S$ under the given assumptions$$

Lean4

theorem dfinsuppSumAddHom_mem {β : ι → Type*} [∀ i, AddZeroClass (β i)] (S : Submodule R N) (f : Π₀ i, β i)
    (g : ∀ i, β i →+ N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : DFinsupp.sumAddHom g f ∈ S :=
  _root_.dfinsuppSumAddHom_mem S f g h

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