smul_prod' — Mathlib

English

For a Finset s and a function f: γ → N with a scalar action of M, the scalar distributes over the Finset product: r • ∏ x∈s f x = ∏ x∈s r • f x.

Русский

Для конечного множества s и функции f, скалярное умножение распределяется по произведению над s: r • ∏_{x∈s} f(x) = ∏_{x∈s} (r • f(x)).

LaTeX

$$$\\forall {M} {N} [\\mathsf{Monoid} M] [\\mathsf{CommMonoid} N] [\\mathsf{MulDistribMulAction} M N] (r:M) (f: γ \\to N) (s:\\mathsf{Finset} γ),\\; r \\cdot \\prod_{x\\in s} f(x) = \\prod_{x\\in s} (r \\cdot f(x))$$$

Lean4

theorem smul_prod' {r : M} {f : γ → N} {s : Finset γ} : (r • ∏ x ∈ s, f x) = ∏ x ∈ s, r • f x :=
  map_prod (MulDistribMulAction.toMonoidHom N r) f s

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