English
The maximal real subfield of K is the subfield consisting of those elements whose images under every complex embedding lie in the real numbers.
Русский
Максимальное вещественное подполе K состоит из элементов, чьи образы при каждом комплексном вложении лежат в вещественных числах.
LaTeX
$$$\mathrm{maximalRealSubfield}(K) = \{ x \in K \mid \forall \varphi : K \to \mathbb{C}, \overline{\varphi(x)} = \varphi(x) \}$$$
Lean4
/-- The maximal real subfield of `K`. It is totally real,
see `NumberField.isTotallyReal_maximalRealSubfield`, and contains all the other totally real
subfields of `K`, see `NumberField.IsTotallyReal.le_maximalRealSubfield`.
-/
def maximalRealSubfield : Subfield K
where
carrier := {x | ∀ φ : K →+* ℂ, star (φ x) = φ x}
mul_mem' hx hy _ := by rw [map_mul, star_mul, hx, hy, mul_comm]
one_mem' := by simp
add_mem' hx hy _ := by rw [map_add, star_add, hx, hy]
zero_mem' := by simp
neg_mem' := by simp
inv_mem' := by simp
