rank_mul_sepDegree_of_isSeparable

English

In a separable setting, the q^n-th power map on a basis gives another basis with the same span.

Русский

В разделяемом случае отображение по q^n на базис дает другой базис той же линейной оболочки.

LaTeX

$$$\text{new basis spans same space as old}$$$

Lean4

/-- The same-universe version of `Field.lift_rank_mul_lift_sepDegree_of_isSeparable`. -/
theorem rank_mul_sepDegree_of_isSeparable (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K]
    [Algebra.IsSeparable F E] : Module.rank F E * sepDegree E K = sepDegree F K := by
  simpa only [Cardinal.lift_id] using lift_rank_mul_lift_sepDegree_of_isSeparable F E K

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