sepDegree_le_rank

Mathlib.FieldTheory.SeparableClosure

URI: https://scilib.ai/kg/mathlib#Field.sepDegree_le_rank

English

sepDegree F E ≤ rank_F E.

Русский

sepDegree F E не превосходит размерности расширения E над F.

LaTeX

$$$\\mathrm{sepDegree}(F,E) \\le \\operatorname{rank}_F(E)$$$

Lean4

theorem sepDegree_le_rank : sepDegree F E ≤ Module.rank F E :=
  Module.rank_bot_le_rank_of_isScalarTower _ _ _

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

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

Разделы

Аффилиация

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