isTotallyReal_maximalRealSubfield

English

The maximal real subfield of K is totally real.

Русский

Максимальное вещественное подполье K является полностью вещественным.

LaTeX

$$$\text{IsTotallyReal}(\mathrm{maximalRealSubfield}(K))$$$

Lean4

instance isTotallyReal_maximalRealSubfield : IsTotallyReal (maximalRealSubfield K) where
  isReal
    w := by
    rw [InfinitePlace.isReal_iff, ComplexEmbedding.isReal_iff]
    ext x
    rw [RingHom.star_apply, ← lift_algebraMap_apply K w.embedding]
    exact x.prop _

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