topEquiv — Mathlib

English

The top intermediate field is algebraically isomorphic to the field E.

Русский

Верхнее промежуточное поле алгебраически изоморфно полю E.

LaTeX

$$$ \\top : \\text{IntermediateField}(F,E) \\cong_A[F] E $$$

Lean4

/-- The top `IntermediateField` is isomorphic to the field.

This is the intermediate field version of `Subalgebra.topEquiv`. -/
@[simps!]
def topEquiv : (⊤ : IntermediateField F E) ≃ₐ[F] E :=
  Subalgebra.topEquiv

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