English
For a finite index set s and a real-valued function f: α → ℝ, the complex embedding of the product equals the product of the complex embeddings: (∏ i ∈ s, f i) as a real number, viewed in ℂ, equals ∏ i ∈ s, (f i) viewed in ℂ.
Русский
Для конечного множества индексов s и функции f: α → ℝ верно, что комплексизация произведения равна произведению комплексизаций: ∏_{i∈s} f(i), взятое как элемент ℂ, равно ∏_{i∈s} f(i), взятое в ℂ.
LaTeX
$$$$ \operatorname{ofReal}\left( \prod_{i \in s} f(i) \right) = \prod_{i \,\in\, s} \operatorname{ofReal}\big( f(i) \big) $$$$
Lean4
@[simp, norm_cast]
theorem ofReal_prod (f : α → ℝ) : ((∏ i ∈ s, f i : ℝ) : ℂ) = ∏ i ∈ s, (f i : ℂ) :=
map_prod ofRealHom _ _
