im

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

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

English

Imaginary part on the upper half-plane is defined by taking the imaginary part of the underlying complex number.

Русский

Мнимая часть на верхней полуплоскости определяется как мнимая часть соответствующего комплексного числа.

LaTeX

$$$\operatorname{im}(z) = (z : \mathbb{C}).im$ for $z \in \mathbb{H}$$$

Lean4

/-- Imaginary part -/
def im (z : ℍ) :=
  (z : ℂ).im

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

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

Разделы

Аффилиация

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