top_toSubfield — Mathlib

English

Let F ⊆ E be a field extension. The top intermediate field, when viewed as a subfield of E, is the entire field E.

Русский

Пусть F ⊆ E — расширение полей. Верхнее промежуточное поле, рассматриваемое как подполье E, совпадает с полем E.

LaTeX

$$$ (\\top : \\text{IntermediateField}(F,E)).toSubfield = \\top $$$

Lean4

@[simp]
theorem top_toSubfield : (⊤ : IntermediateField F E).toSubfield = ⊤ :=
  rfl

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