lift_insepDegree_bot' — Mathlib

English

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

Русский

Поднятие сохраняет неинsep-степень вдоль нижнего эквивалента: lift(insepDegree F (⊥ E K)) = lift(insepDegree F E).

LaTeX

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

Lean4

theorem lift_insepDegree_bot' :
    Cardinal.lift.{v} (insepDegree F (⊥ : IntermediateField E K)) = Cardinal.lift.{w} (insepDegree F E) :=
  lift_insepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

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