imaginaryPart_realPart

Mathlib.LinearAlgebra.Complex.Module

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

English

The imaginary part of the real part equals the imaginary part: Im(Re(x)) = Im(x).

Русский

Мнимая часть действительной части равна мнимой части: Im(Re(x)) = Im(x).

LaTeX

$$$\\operatorname{imaginaryPart}(\\operatorname{realPart}(x)) = \\operatorname{imaginaryPart}(x)$$$

Lean4

theorem imaginaryPart_realPart {x : A} : ℑ (ℜ x : A) = 0 :=
  (ℜ x).property.imaginaryPart

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

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

Разделы

Аффилиация

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