vadd_im

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

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

English

The imaginary part of x +ᵥ z equals z.im.

Русский

Мнимая часть x +ᵥ z равна z.im.

LaTeX

$$ (x +ᵥ z).im = z.im $$

Lean4

@[simp]
theorem vadd_im : (x +ᵥ z).im = z.im :=
  zero_add _

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

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

Разделы

Аффилиация

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