top_toSubalgebra — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem top_toSubalgebra : (⊤ : IntermediateField F E).toSubalgebra = ⊤ :=
  rfl

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