instFiniteSubtypeMemBot

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

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

English

The bottom intermediate field, viewed as an F-vector space, is finite dimensional.

Русский

Нижнее промежуточное поле, рассматриваемое как векторное пространство над F, конечномерно.

LaTeX

$$$\operatorname{finrank}_F\bigl(\perp:\text{IntermediateField } F E\bigr) < \infty$$$

Lean4

instance : Module.Finite F (⊥ : IntermediateField F E) :=
  Subalgebra.finite_bot

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

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

Разделы

Аффилиация

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