subfield_ne_real_of_isComplex — Mathlib

English

If an infinite place is complex, then the real subfield embedding is not equal to the complex one; i.e., the real subfield is proper.

Русский

Если место комплексное, то подполе вещественных отображений не совпадает с подполем комплексных.

LaTeX

$$subfield_ne_real_of_isComplex hv$$

Lean4

theorem subfield_ne_real_of_isComplex {v : InfinitePlace K} (hv : IsComplex v) :
    (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange :=
  by
  contrapose! hv
  simp only [not_isComplex_iff_isReal, isReal_iff]
  ext x
  obtain ⟨r, hr⟩ := hv ▸ extensionEmbedding_coe v x ▸ RingHom.mem_fieldRange_self _ _
  simp only [ComplexEmbedding.conjugate_coe_eq, ← hr, Complex.ofRealHom_eq_coe, Complex.conj_ofReal]

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