insepDegree_le_rank

Mathlib.FieldTheory.SeparableClosure

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

English

insepDegree F E ≤ rank_F E.

Русский

insepDegree F E не превосходит rank_F E.

LaTeX

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

Lean4

theorem insepDegree_le_rank : insepDegree F E ≤ Module.rank F E :=
  Module.rank_top_le_rank_of_isScalarTower _ _ _

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

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

Разделы

Аффилиация

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