conj_eq_iff_im — Mathlib

English

Conjugation equals the identity exactly when the imaginary part vanishes; equivalently, conj z = z iff Im(z) = 0.

Русский

Сопряжение совпадает с тождественным отображением тогда, когда мнимая часть равна нулю; conj z = z ⇔ Im(z) = 0.

LaTeX

$$$\overline{z} = z \iff \operatorname{Im}(z) = 0$$$

Lean4

theorem conj_eq_iff_im {z : ℂ} : conj z = z ↔ z.im = 0 :=
  ⟨fun h => add_self_eq_zero.mp (neg_eq_iff_add_eq_zero.mp (congr_arg im h)), fun h =>
    ext rfl (neg_eq_iff_add_eq_zero.mpr (add_self_eq_zero.mpr h))⟩

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