multiset_prod_apply — Mathlib

English

For a finite multiset S of functions f: α → M with commutative monoid M(a) for each a,

Русский

Пусть S — конечная мультисет функций f: α → M, и для каждого a моноид M(a) коммутативен. Тогда

LaTeX

$$$$ s.\\,prod\_a = (s.map(\\lambda f, f(a))).prod. $$$$

Lean4

@[to_additive]
theorem multiset_prod_apply {α : Type*} {M : α → Type*} [∀ a, CommMonoid (M a)] (a : α) (s : Multiset (∀ a, M a)) :
    s.prod a = (s.map fun f : ∀ a, M a ↦ f a).prod :=
  (evalMonoidHom M a).map_multiset_prod _

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