isReal_iff — Mathlib

English

IsReal w is equivalent to ComplexEmbedding.IsReal (embedding w).

Русский

IsReal w эквивалентно ComplexEmbedding.IsReal (embedding w).

LaTeX

$$$IsReal(w) \iff \\mathrm{ComplexEmbedding.IsReal}(\\mathrm{embedding}(w)).$$$

Lean4

theorem isReal_iff {w : InfinitePlace K} : IsReal w ↔ ComplexEmbedding.IsReal (embedding w) :=
  by
  refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
  rintro ⟨φ, ⟨hφ, rfl⟩⟩
  rwa [embedding_mk_eq_of_isReal hφ]

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