finInsepDegree_top — Mathlib

English

Finite inseparable degree of the top extension equals that of the ambient extension (reprise).

Русский

Конечная неинsep степень верхнего расширения равна степени над полем, в которое расширяется.

LaTeX

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

Lean4

@[simp]
theorem finInsepDegree_top : finInsepDegree F (⊤ : IntermediateField E K) = finInsepDegree F K := by
  rw [finInsepDegree_def', insepDegree_top, ← finInsepDegree_def']

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