tower_top — Mathlib

English

The image of an element x ∈ F under the algebra map to K is separable over F.

Русский

Образ элемента x ∈ F под алгебраическим отображением в K разделим над F.

LaTeX

$$IsSeparable F (algebraMap F K x)$$

Lean4

/-- If `E / L / F` is a scalar tower and `x : E` is separable over `F`, then it's also separable
over `L`. -/
@[stacks 09H2 "first part"]
theorem tower_top {x : E} (h : IsSeparable F x) : IsSeparable L x :=
  .of_dvd (.map h) (minpoly.dvd_map_of_isScalarTower ..)

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