isSeparable_algebraMap — Mathlib

English

For any x ∈ F, the image under the algebra map to K is separable.

Русский

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

LaTeX

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

Lean4

theorem isSeparable_algebraMap (x : F) : IsSeparable F (algebraMap F K x) :=
  Polynomial.Separable.of_dvd (Polynomial.separable_X_sub_C (x := x))
    (minpoly.dvd F (algebraMap F K x) (by simp only [map_sub, aeval_X, aeval_C, sub_self]))

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