finInsepDegree_eq — Mathlib

English

Finite inseparable degree equals finite rank; specifically finInsepDegree F E = finrank F E.

Русский

Конечная бесприводная степень равна конечному рангу: finInsepDegree F E = finrank F E.

LaTeX

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

Lean4

/-- A purely inseparable extension has finite inseparable degree equal to degree. -/
theorem finInsepDegree_eq [IsPurelyInseparable F E] : finInsepDegree F E = finrank F E :=
  congr(Cardinal.toNat $(insepDegree_eq F E))

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