finInsepDegree_top_le_finInsepDegree_of_isScalarTower

English

The inseparable degree of the top intermediate field equals that of the ambient extension: insepDegree F (⊤ : IntermediateField E K) = insepDegree F K.

Русский

Неинsep-степень верхнего поля равна неинsep-степени окружающего расширения: insepDegree F (⊤) = insepDegree F K.

LaTeX

$$$ \operatorname{insepDegree} F (\top : \text{IntermediateField } E K) = \operatorname{insepDegree} F K $$$

Lean4

theorem _root_.Field.finInsepDegree_top_le_finInsepDegree_of_isScalarTower [Module.Finite F K] :
    finInsepDegree E K ≤ finInsepDegree F K :=
  by
  letI := (IntermediateField.inclusion (separableClosure.le_restrictScalars F E K)).toAlgebra
  have : IsScalarTower (separableClosure F K) ((separableClosure E K).restrictScalars F) K := .of_algebraMap_eq' rfl
  exact
    Module.finrank_top_le_finrank_of_isScalarTower (separableClosure F K) ((separableClosure E K).restrictScalars F) K

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