prod_bind — Mathlib

English

With a commutative monoid B, (s.bind t).prod = (s.map (λ a => (t a).prod)).prod.

Русский

Для коммутативного моноида B выполняется: (s.bind t).prod = (s.map (λ a => (t a).prod)).prod.

LaTeX

$$[Prod] $(s.bind t).prod = (s.map (\\lambda a. (t a).prod)).prod$$

Lean4

@[to_additive (attr := simp)]
theorem prod_bind [CommMonoid β] (s : Multiset α) (t : α → Multiset β) :
    (s.bind t).prod = (s.map fun a => (t a).prod).prod := by simp [bind]

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