ofReal_prod — Mathlib

English

For finite s and f: α → ℝ, the embedding preserves finite products: ((∏ i ∈ s, f i : ℝ) : K) = ∏ i ∈ s, (f i : K).

Русский

Для конечного множества s и функции f: α → ℝ отображение сохраняет произведение: ((∏ i ∈ s, f i) : K) = ∏ i ∈ s, (f i : K).

LaTeX

$$$\left(\prod_{i \in s} f_i : \mathbb{R}\right) : K = \prod_{i \in s} (f_i : K)$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_prod {α : Type*} (s : Finset α) (f : α → ℝ) : ((∏ i ∈ s, f i : ℝ) : K) = ∏ i ∈ s, (f i : K) :=
  map_prod (algebraMap ℝ K) _ _

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