insepDegree_top_le_insepDegree_of_isScalarTower

English

Lifting preserves the separable degree along a bottom equivalence (root form).

Русский

Преобразование по нижнему эквиваленту сохраняет сеп-степень.

LaTeX

$$$ \operatorname{Cardinal}.lift(\operatorname{sepDegree} F (\perp : \text{IntermediateField } E K)) = \operatorname{Cardinal}.lift(\operatorname{sepDegree} F E) $$$

Lean4

theorem _root_.Field.insepDegree_top_le_insepDegree_of_isScalarTower : insepDegree E K ≤ insepDegree 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.rank_top_le_rank_of_isScalarTower (separableClosure F K) ((separableClosure E K).restrictScalars F) K

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