toSubfield

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.toSubfield

← MathLib Explorer

English

An intermediate field is naturally a subfield of the ambient field L.

Русский

Промежуточное поле естественным образом является подпольем L.

LaTeX

$$$\text{IntermediateField}(K,L) \ni S \implies S \text{ is a subfield of } L$$$

Lean4

/-- Reinterpret an `IntermediateField` as a `Subfield`. -/
def toSubfield : Subfield L :=
  { S.toSubalgebra with neg_mem' := S.neg_mem, inv_mem' := S.inv_mem' }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru