isTotallyReal_iff_le_maximalRealSubfield

English

A subfield E of K is totally real if and only if E is contained in the maximal real subfield of K.

Русский

Подполе E K полностью вещественное тогда и только тогда, когда E ⊆ максимальное вещественное подполье K.

LaTeX

$$$\text{IsTotallyReal}(E) \iff E \subseteq \mathrm{maximalRealSubfield}(K)$$$

Lean4

theorem isTotallyReal_iff_le_maximalRealSubfield {E : Subfield K} : IsTotallyReal E ↔ E ≤ maximalRealSubfield K :=
  ⟨fun h ↦ h.le_maximalRealSubfield, fun h ↦
    IsTotallyReal.ofRingEquiv (RingEquiv.ofBijective _ (Subfield.inclusion h).rangeRestrictField_bijective).symm⟩

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