complexEmbedding_not_isReal — Mathlib

English

For a totally complex K, every complex embedding φ is non-real (its image is not a real number).

Русский

Для полностью комплексного K каждый вложение φ не является вещественным (его образ не вещественен).

LaTeX

$$[IsTotallyComplex K] \Rightarrow \forall \varphi, \neg \text{ComplexEmbedding.IsReal}(\varphi)$$

Lean4

theorem complexEmbedding_not_isReal [IsTotallyComplex K] (φ : K →+* ℂ) : ¬ComplexEmbedding.IsReal φ :=
  isReal_mk_iff.not.mp <| not_isReal_iff_isComplex.mpr <| isComplex (InfinitePlace.mk φ)

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