sub_im — Mathlib

English

Let z and w be complex numbers. Then the imaginary part of their difference equals the difference of their imaginary parts: Im(z − w) = Im(z) − Im(w).

Русский

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

LaTeX

$$$\\Im(z - w) = \\Im(z) - \\Im(w)$$$

Lean4

@[simp]
theorem sub_im (z w : ℂ) : (z - w).im = z.im - w.im :=
  rfl

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