equivRealProdAddHom — Mathlib

English

There is an additive isomorphism between ℂ and ℝ × ℝ given by z ↦ (Re z, Im z).

Русский

Существует аддитивный изоморфизм между ℂ и ℝ × ℝ, который переводит z в (Re z, Im z).

LaTeX

$$$\\mathbb{C} \\cong_{+} \\mathbb{R} \\times \\mathbb{R}$$$

Lean4

/-- The natural `AddEquiv` from `ℂ` to `ℝ × ℝ`. -/
@[simps! +simpRhs apply symm_apply_re symm_apply_im]
def equivRealProdAddHom : ℂ ≃+ ℝ × ℝ :=
  { equivRealProd with map_add' := by simp }

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