finiteDimensional_left

Mathlib.FieldTheory.IntermediateField.Algebraic

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

English

If L is finite-dimensional over K and F is an intermediate field in L/K, then F is finite-dimensional over K.

Русский

Если L конечномер над K и F — промежуточное поле между K и L, то F также конечномер над K.

LaTeX

$$$ [FiniteDimensional K L] \Rightarrow [FiniteDimensional K F] $$$

Lean4

instance finiteDimensional_left [FiniteDimensional K L] : FiniteDimensional K F :=
  .left K F L

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

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

Разделы

Аффилиация

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