dfinsuppSumAddHom_mem — Mathlib

English

If s is an additive submonoid of γ and f is a dfinsupp, then sumAddHom g f ∈ s provided each nonzero f_i maps into s via g_i.

Русский

Если s — подмоноид сложения в γ, то сумма по f через g лежит в s, если для каждого ненулевого i g_i(f_i) ∈ s.

LaTeX

$$$\mathrm{sumAddHom}(g,f) \in s$ under the stated hypotheses$$

Lean4

theorem dfinsuppSumAddHom_mem [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] {S : Type*} [SetLike S γ]
    [AddSubmonoidClass S γ] (s : S) (f : Π₀ i, β i) (g : ∀ i, β i →+ γ) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) :
    DFinsupp.sumAddHom g f ∈ s := by
  classical
  rw [DFinsupp.sumAddHom_apply]
  exact dfinsuppSum_mem s f (g ·) h

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