cast_sum — Mathlib

English

Let f: index → ℤ and s a Finset of indices. The cast of the product over s equals the product of the casts: (↑(∏ i∈s, f i) : R) = ∏ i∈s, (f i : R).

Русский

Пусть f: индексы → ℤ, s — множество. Образ произведения по s равен произведению образов: (↑(∏ i∈s, f i) : R) = ∏ i∈s, (f i : R).

LaTeX

$$$\left(\prod_{i\in s} f(i)\right)^{\uparrow} = \prod_{i\in s} f(i)^{\uparrow}$$$

Lean4

@[simp, norm_cast]
theorem cast_sum [AddCommGroupWithOne R] (s : Finset ι) (f : ι → ℤ) : ↑(∑ x ∈ s, f x : ℤ) = ∑ x ∈ s, (f x : R) :=
  map_sum (castAddHom R) _ _

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