sepDegree_top — Mathlib

English

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

Русский

Конечная неинsep-степень верхнего поля равна степени над полем K: finInsepDegree F (⊤) = finInsepDegree F K.

LaTeX

$$$ \mathrm{finInsepDegree} F (\top : \text{IntermediateField } E K) = \mathrm{finInsepDegree} F K $$$

Lean4

@[simp]
theorem sepDegree_top : sepDegree F (⊤ : IntermediateField E K) = sepDegree F K :=
  sepDegree_eq_of_equiv _ _ _ ((topEquiv (F := E) (E := K)).restrictScalars F)

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