finiteDimensional

Mathlib.FieldTheory.Galois.IsGaloisGroup

URI: https://scilib.ai/kg/mathlib#IsGaloisGroup.finiteDimensional

← MathLib Explorer

English

L is finite-dimensional over K; equivalently, L is a finite-dimensional vector space over K.

Русский

Поле L является конечномерным над полем K.

LaTeX

$$$\\dim_K L < \\infty$$$

Lean4

theorem finiteDimensional [Finite G] [IsGaloisGroup G K L] : FiniteDimensional K L :=
  FiniteDimensional.of_finrank_pos (card_eq_finrank G K L ▸ Nat.card_pos)

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

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

Разделы

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

Аффилиация

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