sepDegree_mul_insepDegree — Mathlib

English

Under an algebra isomorphism i, lift(sepDegree F E) = lift(sepDegree F K).

Русский

При изоморфизме алгебр i: E ≃... K сохраняется значение под лифт.

LaTeX

$$$\\mathrm{lift}(\\mathrm{sepDegree}(F,E)) = \\mathrm{lift}(\\mathrm{sepDegree}(F,K))$$$

Lean4

/-- The separable degree multiplied by the inseparable degree is equal
to the (infinite) field extension degree. -/
theorem sepDegree_mul_insepDegree : sepDegree F E * insepDegree F E = Module.rank F E :=
  rank_mul_rank F (separableClosure F E) E

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