finInsepDegree_eq — Mathlib

English

A separable extension has finite inseparable degree equal to 1.

Русский

Разделяемое расширение имеет конечную неразделимую степень равную 1.

LaTeX

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

Lean4

/-- A separable extension has finite inseparable degree one. -/
theorem finInsepDegree_eq [Algebra.IsSeparable F E] : finInsepDegree F E = 1 :=
  Cardinal.one_toNat ▸ congr(Cardinal.toNat $(insepDegree_eq F E))

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