sepDegree_eq_of_equiv — Mathlib

English

The same-universe version: sepDegree F E = sepDegree F K given i : E ≃ₐ[F] K.

Русский

Тождество сепарабельной степени в одном универсуме: sepDegree F E = sepDegree F K при i : E ≃ₐ[F] K.

LaTeX

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

Lean4

/-- The same-universe version of `Field.lift_sepDegree_eq_of_equiv`. -/
theorem sepDegree_eq_of_equiv (K : Type v) [Field K] [Algebra F K] (i : E ≃ₐ[F] K) : sepDegree F E = sepDegree F K :=
  i.separableClosure.toLinearEquiv.rank_eq

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