finiteDimensional_right

Mathlib.FieldTheory.IntermediateField.Algebraic

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

English

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

Русский

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

LaTeX

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

Lean4

instance finiteDimensional_right [FiniteDimensional K L] : FiniteDimensional F L :=
  .right K F L

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

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

Разделы

Аффилиация

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