equivRealProd — Mathlib

English

The complex numbers are naturally equivalent to the product ℝ × ℝ, via z ↦ (Re z, Im z) with inverse (a,b) ↦ a + bi.

Русский

Комплексные числа естественно эквивалентны произведению ℝ × ℝ через отображение z ↦ (Re z, Im z) и обратное (a,b) ↦ a + bi.

LaTeX

$$$$\mathbb{C} \simeq \mathbb{R} \times \mathbb{R},\; z \mapsto (\Re z, \Im z),\; (a,b) \mapsto a + b i.$$$$

Lean4

/-- The equivalence between the complex numbers and `ℝ × ℝ`. -/
@[simps apply]
def equivRealProd : ℂ ≃ ℝ × ℝ where
  toFun z := ⟨z.re, z.im⟩
  invFun p := ⟨p.1, p.2⟩

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