equivRealProdCLM_symm_apply

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.equivRealProdCLM_symm_apply

English

The inverse map satisfies (equivRealProdCLM)^{-1}(p) = p_1 + p_2 i.

Русский

Обратное отображение удовлетворяет (equivRealProdCLM)^{-1}(p) = p_1 + p_2 i.

LaTeX

$$$$ (\\operatorname{equivRealProdCLM})^{-1}(p) = p_{1} + p_{2} i. $$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru