Theorems · Theorem · ring theory

Finsupp.sum_add_index

∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : DecidableEq α] [inst_1 : AddZeroClass M]
  [inst_2 : AddCommMonoid N] {f g : α →₀ M} {h : α → M → N},
  (∀ a ∈ f.support ∪ g.support, h a 0 = 0) →
    (∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f + g).sum h = f.sum h + g.sum h

Taking the product under h is an additive homomorphism of finsupps, if h is an additive homomorphism on the support. This is a more general version of Finsupp.sum_add_index'; the latter has simpler hypotheses.

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

18 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqAddZeroClassAddCommMonoid