isPurelyInseparable_iff_perfectClosure_eq_top

English

A field extension E/F is purely inseparable if and only if the relative perfect closure equals the entire field E.

Русский

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

LaTeX

$$IsPurelyInseparable F E ↔ perfectClosure F E = ⊤$$

Lean4

/-- A field extension `E / F` is purely inseparable if and only if the relative perfect closure of
`F` in `E` is equal to `E`. -/
theorem isPurelyInseparable_iff_perfectClosure_eq_top : IsPurelyInseparable F E ↔ perfectClosure F E = ⊤ :=
  by
  rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]
  exact ⟨fun H ↦ top_unique fun x _ ↦ H x, fun H _ ↦ H.ge trivial⟩

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