le_perfectClosure — Mathlib

English

If L is a purely inseparable intermediate field over F, then L is contained in the perfect closure of F in E.

Русский

Если L — чисто бесразделимое подрасширение над F, то L ⊆ perfectClosure(F,E).

LaTeX

$$IsPurelyInseparable F L → L ≤ perfectClosure F E$$

Lean4

/-- An intermediate field of `E / F` is contained in the relative perfect closure of `F` in `E`
if it is purely inseparable over `F`. -/
theorem le_perfectClosure (L : IntermediateField F E) [h : IsPurelyInseparable F L] : L ≤ perfectClosure F E :=
  by
  rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)] at h
  intro x hx
  obtain ⟨n, y, hy⟩ := h ⟨x, hx⟩
  exact ⟨n, y, congr_arg (algebraMap L E) hy⟩

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