mul_finsum_mem' — Mathlib

English

For a finite set s, (r * ∑ᶠ a∈s, f(a)) = ∑ᶠ a∈s, r * f(a).

Русский

Для конечного множества s: (r · ∑ᶠ a∈s, f(a)) = ∑ᶠ a∈s, r · f(a).

LaTeX

$$(r * ∑^F a ∈ s, f(a)) = ∑^F a ∈ s, r * f(a)$$

Lean4

/-- For finite sets, multiplication commutes with `finsum_mem`. See `mul_finsum_mem'` for a statement
assuming finiteness of support.
-/
theorem mul_finsum_mem' {R : Type*} [NonUnitalNonAssocSemiring R] {s : Set α} (f : α → R) (r : R) (hs : s.Finite) :
    (r * ∑ᶠ a ∈ s, f a) = ∑ᶠ a ∈ s, r * f a :=
  (AddMonoidHom.mulLeft r).map_finsum_mem f hs

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