lift_sepDegree_bot' — Mathlib

English

Lifting preserves the separable degree along a bottom equivalence: lift(sepDegree F (⊥ E K)) = lift(sepDegree F E).

Русский

Преобразование по нижнему эквиваленту сохраняет сеп степени: lift(sepDegree F (⊥ E K)) = lift(sepDegree F E).

LaTeX

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

Lean4

theorem lift_sepDegree_bot' :
    Cardinal.lift.{v} (sepDegree F (⊥ : IntermediateField E K)) = Cardinal.lift.{w} (sepDegree F E) :=
  lift_sepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

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