cast_prod — Mathlib

English

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

Русский

Пусть f: индексы → Nat и 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_prod [CommSemiring R] (f : ι → ℕ) (s : Finset ι) : (↑(∏ i ∈ s, f i) : R) = ∏ i ∈ s, (f i : R) :=
  map_prod (castRingHom R) _ _

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