sepDegree_bot — Mathlib

English

The separable degree of the bottom intermediate field is 1.

Русский

СепDegree нижней грани промежуточного поля равна 1.

LaTeX

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

Lean4

@[simp]
theorem sepDegree_bot : sepDegree F (⊥ : IntermediateField F E) = 1 :=
  by
  have := lift_sepDegree_eq_of_equiv _ _ _ (botEquiv F E)
  rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this

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