Theorems · Theorem · ring theory

Finsupp.prod_add_index

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

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

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClassCommMonoid