complexEmbedding_isReal — Mathlib

English

If K is totally real and φ: K → ℂ is a ring hom, then φ is real (i.e., its complex embedding is real).

Русский

Если K полностью вещественно и φ: K → ℂ — кольцевое отображение, то φ является действительным отображением.

LaTeX

$$If [IsTotallyReal K] and φ: K →+* ℂ then ComplexEmbedding.IsReal φ.$$

Lean4

theorem complexEmbedding_isReal [IsTotallyReal K] (φ : K →+* ℂ) : ComplexEmbedding.IsReal φ :=
  isReal_mk_iff.mp <| isReal (InfinitePlace.mk φ)

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