conj_eq_iff_real — Mathlib

English

Conjugate z equals z if and only if z is a real number; equivalently, ∃ r ∈ ℝ with z = ofReal r.

Русский

Сопряжение z равно z тогда и только тогда, когда z вещественно; эквивалентно существованию r ∈ ℝ с z = ofReal r.

LaTeX

$$$\operatorname{conj} z = z \;\Leftrightarrow\; \exists r \in \mathbb{R},\; z = \operatorname{ofReal}(r)$$$

Lean4

theorem conj_eq_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=
  calc
    _ ↔ ∃ r : ℝ, (r : K) = z := (is_real_TFAE z).out 0 1
    _ ↔ _ := by simp only [eq_comm]

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