mem_perfectClosure_iff_natSepDegree_eq_one

English

An element lies in the perfect closure if and only if its minimal polynomial over F has separable degree equal to 1.

Русский

Элемент принадлежит совершенном замыканию тогда и только тогда, когда минимальный многочлен над F имеет сепарабельную степень, равную 1.

LaTeX

$${x ∈ perfectClosure F E} ↔ (minpoly F x).natSepDegree = 1$$

Lean4

/-- An element is contained in the relative perfect closure if and only if its minimal polynomial
has separable degree one. -/
theorem mem_perfectClosure_iff_natSepDegree_eq_one {x : E} : x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1 :=
  by rw [mem_perfectClosure_iff, minpoly.natSepDegree_eq_one_iff_pow_mem (ringExpChar F)]

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