prod_natCast — Mathlib

English

For a finite set s and a map f: s → Nat, the natural cast of the product ∏ f(i) equals the product in R of the casted values, i.e., ↑(∏ i∈s f(i)) = ∏ i∈s (f(i) : R).

Русский

Для конечного множества s и отображения f: s → Nat верно, что приведение к R произведения ∏ i∈s f(i) равно произведению приведения каждого f(i) к R.

LaTeX

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

Lean4

@[norm_cast]
theorem prod_natCast (s : Finset ι) (f : ι → ℕ) : ↑(∏ i ∈ s, f i : ℕ) = ∏ i ∈ s, (f i : R) :=
  map_prod (Nat.castRingHom R) f s

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