sepDegree_bot' — Mathlib

English

Separable degree of bottom field equals separable degree of the base field: sepDegree F (⊥ : IntermediateField E K) = sepDegree F E.

Русский

Сеп Degree нижнего поля равна сеп Degree базового поля: sepDegree F (⊥) = sepDegree F E.

LaTeX

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

Lean4

@[simp]
theorem sepDegree_bot' : sepDegree F (⊥ : IntermediateField E K) = sepDegree F E :=
  sepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

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