sepDegree_eq_one — Mathlib

English

The separable degree of a purely inseparable extension is 1.

Русский

Сепарабельная степень чисто бесприводного расширения равна 1.

LaTeX

$$$\operatorname{sepDegree} F E = 1$$$

Lean4

/-- A purely inseparable extension has separable degree one. -/
theorem sepDegree_eq_one [IsPurelyInseparable F E] : sepDegree F E = 1 := by
  rw [sepDegree, separableClosure.eq_bot_of_isPurelyInseparable, IntermediateField.rank_bot]

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