cast_finprod_mem — Mathlib

English

For a finite set s and a semiring R, casting the finsum over s of f x into R equals finsum over s of casted f x into R.

Русский

Для конечного множества s и кольца R равенство сохраняется: преобразование суммы finsum через приведение к R эквивалентно сумме приведений.

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_finprod_mem {s : Set ι} (hs : s.Finite) {R : Type*} [CommSemiring R] (f : ι → ℕ) :
    ↑(∏ᶠ x ∈ s, f x : ℕ) = ∏ᶠ x ∈ s, (f x : R) :=
  (Nat.castRingHom R).map_finprod_mem _ hs

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