lift_insepDegree_eq_of_equiv — Mathlib

English

If i : E ≃ₐ[F] K, then finInsepDegree F E = finInsepDegree F K.

Русский

Если E и K изоморфны как F-алгебры, то конечные сепарабельные степени равны.

LaTeX

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

Lean4

/-- If `E` and `K` are isomorphic as `F`-algebras, then they have the same
inseparable degree over `F`. -/
theorem lift_insepDegree_eq_of_equiv (i : E ≃ₐ[F] K) :
    Cardinal.lift.{w} (insepDegree F E) = Cardinal.lift.{v} (insepDegree F K) :=
  Algebra.lift_rank_eq_of_equiv_equiv i.separableClosure i rfl

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