natSepDegree_eq_one — Mathlib

English

For a purely inseparable extension, the separable degree of the minimal polynomial of every element is 1.

Русский

Для чисто безразделимого расширения сепарабельная степень минимального многочлена каждого элемента равна 1.

LaTeX

$$[IsPurelyInseparable F E] (x ∈ E) ⇒ (minpoly F x).natSepDegree = 1$$

Lean4

theorem natSepDegree_eq_one [IsPurelyInseparable F E] (x : E) : (minpoly F x).natSepDegree = 1 :=
  (isPurelyInseparable_iff_natSepDegree_eq_one F).1 ‹_› x

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