cast_finprod — Mathlib

English

For a finite index set and a semiring N, casting the finprod of naturals into N equals the finprod of the casted values.

Русский

Для конечного множества индексов и полусетей N, приведение значения финпроизведения кодом ℕ в N сохраняет равенство.

LaTeX

$$$ \\uparrow(\\\\prod^\\\\mathrm{f}_{i}, f i) = \\\\prod^\\\\mathrm{f}_{i}, (f i)^{\\\\uparrow} $$$

Lean4

@[simp, norm_cast]
theorem cast_finprod [Finite ι] {R : Type*} [CommSemiring R] (f : ι → ℕ) : ↑(∏ᶠ x, f x : ℕ) = ∏ᶠ x, (f x : R) :=
  (Nat.castRingHom R).map_finprod f.mulSupport.toFinite

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