insepDegree_le_of_left_le — Mathlib

English

If E and F are related by an isScalarTower through K, then the insepDegree cannot increase with the top extension: insepDegree E K ≤ insepDegree F K.

Русский

При цилиндрической башне из E в K через F неинsep-степень не возрастает: insepDegree E K ≤ insepDegree F K.

LaTeX

$$$ \operatorname{insepDegree} E K \le \operatorname{insepDegree} F K $$$

Lean4

theorem _root_.Field.insepDegree_le_of_left_le {E₁ E₂ : IntermediateField F K} (H : E₁ ≤ E₂) :
    insepDegree E₂ K ≤ insepDegree E₁ K :=
  by
  letI := (IntermediateField.inclusion H).toAlgebra
  have : IsScalarTower E₁ E₂ K := .of_algebraMap_eq' rfl
  exact insepDegree_top_le_insepDegree_of_isScalarTower _ _ _

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