pos_real_im

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.pos_real_im

English

The imaginary part of x • z equals z.im, and the real part equals x · z.re.

Русский

Мнимая часть x • z равна z.im, действительная часть равна x · z.re.

LaTeX

$$ (x • z).im = z.im and (x • z).re = x * z.re $$

Lean4

@[simp]
theorem pos_real_im : (x • z).im = x * z.im :=
  Complex.smul_im _ _

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

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

Разделы

Аффилиация

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