botEquiv — Mathlib

English

The bottom intermediate field is isomorphic to the base field F as an F-algebra.

Русский

Нижнее промежуточное поле изоморфно базовому полю F как F-алгебра.

LaTeX

$$$ \\bot : \\text{IntermediateField}(F,E) \\cong_{F} F $$$

Lean4

/-- The bottom intermediate_field is isomorphic to the field. -/
noncomputable def botEquiv : (⊥ : IntermediateField F E) ≃ₐ[F] F :=
  (Subalgebra.equivOfEq _ _ bot_toSubalgebra).trans (Algebra.botEquiv F E)

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