sub_re — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem sub_re (z w : ℂ) : (z - w).re = z.re - w.re :=
  rfl

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