sepDegree_eq — Mathlib

English

If E/F is a separable extension, then the separable degree equals the ordinary degree: sepDegree(F,E) = rank_F(E).

Русский

Если расширение E над F является разделимым, то разделяемая степень равна обычной степени: sepDegree(F,E) = rank_F(E).

LaTeX

$$$\\operatorname{sepDegree} F E = \\operatorname{rank}_F E$$$

Lean4

/-- A separable extension has separable degree equal to degree. -/
theorem sepDegree_eq [Algebra.IsSeparable F E] : sepDegree F E = Module.rank F E := by
  rw [sepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top']

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