mul_finsum' — Mathlib

English

Multiplication commutes with finsums: for f: α → R, r ∈ R, (r · ∑ᶠ a, f(a)) = ∑ᶠ a, r · f(a).

Русский

Умножение коммутирует с финсуммами: (r · ∑ᶠ a, f(a)) = ∑ᶠ a, r · f(a).

LaTeX

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

Lean4

/-- For functions with finite support, multiplication commutes with finsums. See `mul_finsum` for a
statement assuming that `R` has no zero divisors.
-/
theorem mul_finsum' {R : Type*} [NonUnitalNonAssocSemiring R] (f : α → R) (r : R) (h : (support f).Finite) :
    (r * ∑ᶠ a : α, f a) = ∑ᶠ a : α, r * f a :=
  (AddMonoidHom.mulLeft r).map_finsum h

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