finSepDegree_eq_of_equiv — Mathlib

English

Same as above: finSepDegree is preserved under F-algebra isomorphisms.

Русский

Повтор: финальная разделяемая степень сохраняется при изоморфизма F-алгебр.

LaTeX

$$$\\operatorname{finSepDegree} F E = \\operatorname{finSepDegree} F K$ if $E \\cong_F K$$$

Lean4

/-- If `E` and `K` are isomorphic as `F`-algebras, then they have the same `Field.finSepDegree`
over `F`. -/
theorem finSepDegree_eq_of_equiv (i : E ≃ₐ[F] K) : finSepDegree F E = finSepDegree F K :=
  Nat.card_congr (embEquivOfEquiv F E K i)

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