finInsepDegree_bot' — Mathlib

English

The finite inseparable degree of the bottom intermediate field equals that of the base field: finInsepDegree F (⊥ E K) = finInsepDegree F E.

Русский

Конечная неинsep-степень нижнего поля равна степенью исходного поля: finInsepDegree F (⊥ E K) = finInsepDegree F E.

LaTeX

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

Lean4

@[simp]
theorem finInsepDegree_bot' : finInsepDegree F (⊥ : IntermediateField E K) = finInsepDegree F E := by
  simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat (lift_insepDegree_bot' F E K)

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