realPart_imaginaryPart

Mathlib.LinearAlgebra.Complex.Module

URI: https://scilib.ai/kg/mathlib#realPart_imaginaryPart

English

Real part and imaginary part commute to give original element via sum: Re(a) + i Im(a) = a.

Русский

Действительная и мнимая части складываются обратно: Re(a) + i Im(a) = a.

LaTeX

$$$\\operatorname{realPart}(a) + i \\operatorname{imaginaryPart}(a) = a$$$

Lean4

theorem realPart_imaginaryPart {x : A} : ℜ (ℑ x : A) = ℑ x :=
  Subtype.ext <| (ℑ x).property.coe_realPart

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

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

Разделы

Аффилиация

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