trans — Mathlib

English

If α is algebraic, finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ iff IsSeparable F α.

Русский

Если α алгебраичен, тогда finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ тогда и только тогда IsSeparable F α.

LaTeX

$$$ finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ \iff IsSeparable F α $$$

Lean4

/-- If `E / F` and `K / E` are both separable extensions, then `K / F` is also separable. -/
@[stacks 09HB]
theorem trans [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] [Algebra.IsSeparable E K] :
    Algebra.IsSeparable F K :=
  ⟨fun x ↦ IsSeparable.of_algebra_isSeparable_of_isSeparable F (Algebra.IsSeparable.isSeparable E x)⟩

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