re_eq_ofReal_of_isSelfAdjoint — Mathlib

English

If x is self-adjoint, then its real part completely determines x: re(x) = y iff x = ofReal(y).

Русский

Если x самосопряжён, то его вещевая часть полностью определяет x: re(x) = y тогда и только тогда, когда x = ofReal(y).

LaTeX

$$$$\\operatorname{Re}(x) = y \\;\\Longleftrightarrow\\; x = \\operatorname{ofReal}(y)\\quad(\\text{if } x^* = x).$$$$

Lean4

theorem re_eq_ofReal_of_isSelfAdjoint {x : K} {y : ℝ} (hx : IsSelfAdjoint x) : re x = y ↔ x = y := by
  simp [RCLike.ext_iff (K := K), hx, im_eq_zero_iff_isSelfAdjoint]

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