conj_eq_iff_re — Mathlib

English

Let z be an element in a complex-like field with conjugation. Then z is real (i.e., equals its real part) if and only if its conjugate equals itself.

Русский

Пусть z — элемент поля, над которым определено сопряжение. Тогда z реален (равен своей вещественной части) тогда и только тогда, когда сопряжённое к z равно самому z.

LaTeX

$$$$\\overline{z} = z \\quad\\Longleftrightarrow\\quad \\operatorname{Re}(z) = z.$$$$

Lean4

theorem conj_eq_iff_re {z : K} : conj z = z ↔ (re z : K) = z :=
  (is_real_TFAE z).out 0 2

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