nonempty_algEquiv_or — Mathlib

English

Let F be a field with an ℝ-algebra structure and algebraic over ℝ. Then there exists an ℝ-algebra isomorphism either F ≅ ℝ or F ≅ ℂ.

Русский

Пусть F — поле с ℝ-алгеброй, алгебрично над ℝ. Тогда найдётся изоморфизм ℝ-алгебр между F и либо ℝ, либо ℂ.

LaTeX

$$$$ \\text{If } F \\text{ is an algebraic extension of } \\mathbb{R}, \\ exists \\; F \\cong_{\\mathbb{R}} \\mathbb{R} \\text{ or } F \\cong_{\\mathbb{R}} \\mathbb{C}. $$$$

Lean4

/-- An algebraic extension of ℝ is isomorphic to either ℝ or ℂ as an ℝ-algebra. -/
theorem nonempty_algEquiv_or (F : Type*) [Field F] [Algebra ℝ F] [Algebra.IsAlgebraic ℝ F] :
    Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ) :=
  IsAlgClosed.nonempty_algEquiv_or_of_finrank_eq_two F Complex.finrank_real_complex

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