mem_maximalRealSubfield_iff — Mathlib

English

An element x lies in the maximal real subfield of K precisely when all complex embeddings send x to real numbers.

Русский

Элемент x принадлежит максимум вещественного подполя K тогда и только тогда, когда все комплексные вложения отправляют x в вещественные числа.

LaTeX

$$$x\in \mathrm{maximalRealSubfield}(K) \iff \forall \varphi : K \to \mathbb{C}, \overline{\varphi(x)} = \varphi(x)$$$

Lean4

theorem mem_maximalRealSubfield_iff (x : K) : x ∈ maximalRealSubfield K ↔ ∀ φ : K →+* ℂ, star (φ x) = φ x :=
  .rfl

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