add_im

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.add_im

English

Let z and w be complex numbers. The imaginary part is additive over addition: Im(z + w) = Im(z) + Im(w).

Русский

Пусть z и w — комплексные числа. Мнимая часть суммирования равна сумме мнимых частей: Im(z + w) = Im(z) + Im(w).

LaTeX

$$$\operatorname{Im}(z+w) = \operatorname{Im}(z) + \operatorname{Im}(w)$$$

Lean4

@[simp]
theorem add_im (z w : ℂ) : (z + w).im = z.im + w.im :=
  rfl

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

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

Разделы

Аффилиация

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