equivRealProdLm_symm_apply — Mathlib

English

The inverse of the canonical real-linear isomorphism ℂ ≅ ℝ × ℝ sends (a,b) to a + b i.

Русский

Обратная к каноническому вещественному линейному изоморфизму ℂ ≅ ℝ × ℝ отправляет (a,b) в a + b i.

LaTeX

$$$ (\mathbb{C} \cong_{\mathbb{R}} \mathbb{R} \times \mathbb{R})^{-1}(p) = p_1 + p_2 \cdot i, \quad p = (p_1,p_2). $$$

Lean4

theorem equivRealProdLm_symm_apply (p : ℝ × ℝ) : Complex.equivRealProdLm.symm p = p.1 + p.2 * Complex.I :=
  Complex.equivRealProd_symm_apply p

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