isPurelyInseparable_iff_natSepDegree_eq_one

English

If E/F is purely inseparable, then the separable closure of F in E is F itself.

Русский

Если расширение E/F чисто безразделимо, то сепарабельное замыкание F в E равно F.

LaTeX

$$separableClosure F E = ⊥$$

Lean4

/-- A field extension `E / F` is purely inseparable if and only if for every element `x` of `E`,
its minimal polynomial has separable degree one. -/
theorem isPurelyInseparable_iff_natSepDegree_eq_one :
    IsPurelyInseparable F E ↔ ∀ x : E, (minpoly F x).natSepDegree = 1 :=
  by
  obtain ⟨q, _⟩ := ExpChar.exists F
  simp_rw [isPurelyInseparable_iff_pow_mem F q, minpoly.natSepDegree_eq_one_iff_pow_mem q]

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