smul_finprod' — Mathlib

English

For any finite index type ι and a function f: ι → N, and r ∈ M, r • (finprod x∈ι, f x) = finprod x∈ι, r • f x.

Русский

Для конечного индекса ι и функции f: ι → N верно: r • (финальное произведение) = произведение по r • f x.

LaTeX

$$$\\forall {ι} [Finite ι] {f: ι \\to N} (r:M),\\; r \\cdot \\mathrm{finprod}\\ x:ι, f x = \\mathrm{finprod}\\ x:ι, r \\cdot (f x)$$$

Lean4

theorem smul_finprod' {ι : Sort*} [Finite ι] {f : ι → N} (r : M) : r • ∏ᶠ x : ι, f x = ∏ᶠ x : ι, r • (f x) :=
  by
  cases nonempty_fintype (PLift ι)
  simp only [finprod_eq_prod_plift_of_mulSupport_subset (s := Finset.univ) (by simp), Finset.smul_prod']

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