conj_eq_iff_real — Mathlib

English

Conjugation fixes z iff z is real. Equivalently, conj z = z iff ∃ r ∈ ℝ with z = r.

Русский

Сопряжение фиксирует z тогда и только тогда, когда z вещественно. Иными словами, conj z = z ⇔ ∃ r ∈ ℝ: z = r.

LaTeX

$$$\overline{z} = z \iff \exists r \in \mathbb{R}, z = r$$$

Lean4

theorem conj_eq_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r :=
  ⟨fun h => ⟨z.re, ext rfl <| eq_zero_of_neg_eq (congr_arg im h)⟩, fun ⟨h, e⟩ => by rw [e, conj_ofReal]⟩

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