lift_sepDegree_eq_of_equiv — Mathlib

English

If E and K are isomorphic as F-algebras, then lift(sepDegree F E) = lift(sepDegree F K).

Русский

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

LaTeX

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

Lean4

/-- If `E` and `K` are isomorphic as `F`-algebras, then they have the same
separable degree over `F`. -/
theorem lift_sepDegree_eq_of_equiv (i : E ≃ₐ[F] K) :
    Cardinal.lift.{w} (sepDegree F E) = Cardinal.lift.{v} (sepDegree F K) :=
  i.separableClosure.toLinearEquiv.lift_rank_eq

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