re_eq_ofReal_of_isSelfAdjoint — Mathlib

English

If x is self-adjoint and y ∈ ℝ, then Re(x) = y iff x = real number y.

Русский

Если x является самопряжённым и y ∈ ℝ, то Re(x) = y тогда и только тогда x = комплексное число y.

LaTeX

$$$IsSelfAdjoint(x) \\rightarrow (\\\\operatorname{Re}(x) = y \\\\Rightarrow x = \\\\operatorname{ofReal}(y))$$$

Lean4

theorem re_eq_ofReal_of_isSelfAdjoint {x : ℂ} {y : ℝ} (hx : IsSelfAdjoint x) : Complex.re x = y ↔ x = y :=
  by
  rw [← RCLike.re_eq_complex_re]
  exact RCLike.re_eq_ofReal_of_isSelfAdjoint hx

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