cast_list_prod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem cast_list_prod (s : List ℚ) : (↑s.prod : α) = (s.map (↑)).prod :=
  map_list_prod (Rat.castHom α) _

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