ofReal_eq_re_of_isSelfAdjoint — Mathlib

English

If x is self-adjoint, then y = Re(x) if and only if y = x (for y ∈ ℝ).

Русский

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

LaTeX

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

Lean4

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

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