finSepDegree_top — Mathlib

English

For a tower of field extensions, the separable degree from F to the top intermediate field equals the separable degree from F to the ambient field K.

Русский

Для башни полей сепарабельная степень от F до верхнего поля равна сепарабельной степени от F до полного поля K.

LaTeX

$$$\operatorname{finSepDegree}(F, \top_E^K) = \operatorname{finSepDegree}(F, K)$$$

Lean4

@[simp]
theorem finSepDegree_top : finSepDegree F (⊤ : IntermediateField E K) = finSepDegree F K :=
  finSepDegree_eq_of_equiv _ _ _ ((topEquiv (F := E) (E := K)).restrictScalars F)

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