isSeparable_tower_top_of_isSeparable

English

The base field F is trivially separable over itself.

Русский

Базовое поле F тривиально разделяемо над самим собой.

LaTeX

$$instance isSeparable_self : Algebra.IsSeparable F F := ⟨isSeparable_algebraMap⟩$$

Lean4

/-- If `E / K / F` is an extension tower, `E` is separable over `F`, then it's also separable
over `K`. -/
@[stacks 09H2 "second part"]
theorem isSeparable_tower_top_of_isSeparable [Algebra.IsSeparable F E] : Algebra.IsSeparable L E :=
  ⟨fun x ↦ IsSeparable.tower_top _ (Algebra.IsSeparable.isSeparable F x)⟩

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