cast_finsum_mem — Mathlib

English

For a finite set s, casting the finsum over s of f x to M equals finsum over s of the casts, i.e., ↑(∑ᶠ x ∈ s, f x) = ∑ᶠ x ∈ s, (f x).

Русский

Для конечного множества s приводимая сумма finsum приводится к M равна финсумме приведения.

LaTeX

$$$ \\uparrow(\\\\sum^\\\\mathrm{f}_{x \\in s} f x) = \\\\sum^\\\\mathrm{f}_{x \\in s} (f x)^{\\\\uparrow} $$$

Lean4

@[simp, norm_cast]
theorem cast_finsum_mem {s : Set ι} (hs : s.Finite) {M : Type*} [AddCommMonoidWithOne M] (f : ι → ℕ) :
    ↑(∑ᶠ x ∈ s, f x : ℕ) = ∑ᶠ x ∈ s, (f x : M) :=
  (Nat.castAddMonoidHom M).map_finsum_mem _ hs

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