smul_prod' — Mathlib

English

For any r in a monoid M and a multiset s of N, r • s.prod = (s.map (r • ·)).prod.

Русский

Для любого r в моноиде M и мультимножества s над N выполняется r • (s.prod) = (s.map (r • ·)).prod.

LaTeX

$$$\\forall {M} [\\mathsf{Monoid} M] [\\mathsf{CommMonoid} N] [\\mathsf{MulDistribMulAction} M N] (r:M) (s:\\mathsf{Multiset} N),\\; r \\cdot s.prod = (s.map (r \\cdot \\cdot)).prod$$$

Lean4

theorem smul_prod' {r : M} {s : Multiset N} : r • s.prod = (s.map (r • ·)).prod :=
  (MulDistribMulAction.toMonoidHom N r).map_multiset_prod s

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