smul_prod — Mathlib

English

For any r ∈ M and multiset s ⊆ N, r • s.prod = (s.map (r • ·)).prod.

Русский

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

LaTeX

$$$\\forall {M} {N} [\\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

@[to_additive]
theorem smul_prod [Monoid M] [CommMonoid N] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (s : Multiset N)
    (b : M) : b ^ card s • s.prod = (s.map (b • ·)).prod :=
  Quot.induction_on s <| by simp [List.smul_prod]

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