smul_prod' — Mathlib

English

Let M,N be monoids with a distributive action of M on N. For any r ∈ M and list l of N, the scalar action distributes over the product: r • (l.prod) = (l.map (r • ·)).prod.

Русский

Пусть M,N — моноиды, на N действует дистрибутивно M. Для любого r∈M и списка l элементов N верно: r • (l.prod) = (l.map (r • ·)).prod.

LaTeX

$$$\\forall {M} {N} [\\mathsf{Monoid} M] [\\mathsf{Monoid} N] [\\mathsf{MulDistribMulAction} M N] (r:M) (l:\\text{List }N),\\; r \\cdot l.prod = (l.map (r \\cdot \\cdot)).prod$$$

Lean4

theorem smul_prod' {r : M} {l : List N} : r • l.prod = (l.map (r • ·)).prod :=
  map_list_prod (MulDistribMulAction.toMonoidHom N r) l

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