Theorems · Theorem · ring theory

Multiset.prod_map_add

∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : Multiset ι} {f g : ι → R},
  (Multiset.map (fun i => f i + g i) s).prod =
    (Multiset.map (fun p => (Multiset.map f p.1).prod * (Multiset.map g p.2).prod) s.antidiagonal).sum

Defined in

Mathlib.Algebra.BigOperators.Ring.Multiset

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiring