cast_prod — Mathlib

English

For a Finset s and f: ι → ℚ, the cast of the product equals the product of the casts: ∏ i∈s f(i) cast = ∏ i∈s (f(i) cast).

Русский

Для конечного множества s и функции f: ι → ℚ приведение произведения к α равно произведению приведённых элементов.

LaTeX

$$$ \prod i \in s, f i \ cast\ (i) = \prod i \in s, (f i) cast$$$

Lean4

@[simp, norm_cast]
theorem cast_prod (s : Finset ι) (f : ι → ℚ) : ∏ i ∈ s, f i = ∏ i ∈ s, (f i : α) :=
  map_prod (Rat.castHom α) _ _

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