im_eq_zero_iff_isSelfAdjoint — Mathlib

English

For x ∈ ℂ, Im(x) = 0 if and only if x is self-adjoint (i.e., equal to its conjugate).

Русский

Для x ∈ ℂ, Im(x) = 0 тогда и только тогда, когда x является самопряжённым (равен своему сопряжённому).

LaTeX

$$$\\\\operatorname{Im}(x) = 0 \\\\iff \\\\text{IsSelfAdjoint}(x)$$$

Lean4

theorem im_eq_zero_iff_isSelfAdjoint (x : ℂ) : Complex.im x = 0 ↔ IsSelfAdjoint x :=
  by
  rw [← RCLike.im_eq_complex_im]
  exact RCLike.im_eq_zero_iff_isSelfAdjoint

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