of_algebra — Mathlib

English

If K is totally real and F → K, then F is totally real (via a different formulation).

Русский

Если K полностью вещественно и F → K, то F также полностью вещественно (альтернативная формулировка).

LaTeX

$$[IsTotallyReal K] and [Algebra F K] ⇒ IsTotallyReal F$$

Lean4

theorem of_algebra [IsTotallyReal K] [Algebra F K] : IsTotallyReal F where
  isReal
    w := by
    obtain ⟨W, rfl⟩ : ∃ W : InfinitePlace K, W.comap (algebraMap F K) = w := comap_surjective w
    exact IsReal.comap _ (IsTotallyReal.isReal W)

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