Theorems · Theorem · ring theory

Finsupp.prod_add_index_of_disjoint

∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] {f1 f2 : α →₀ M},
  Disjoint f1.support f2.support →
    ∀ {β : Type u_16} [inst_1 : CommMonoid β] (g : α → M → β), (f1 + f2).prod g = f1.prod g * f2.prod g

For disjoint f1 and f2, and function g, the product of the products of g over f1 and f2 equals the product of g over f1 + f2

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidCommMonoid