separableClosure_le — Mathlib

English

If an intermediate field L of E/F is separable over F and E is purely inseparable over L, then L equals the separable closure of F in E.

Русский

Если L над F внутри E/ F сепарабельна, и E/F/L чисто бесприводно, то L = separableClosure(F,E).

LaTeX

$$$L = \mathrm{separableClosure} (F,E)$$$

Lean4

/-- An intermediate field of `E / F` contains the separable closure of `F` in `E`
if `E` is purely inseparable over it. -/
theorem separableClosure_le (L : IntermediateField F E) [h : IsPurelyInseparable L E] : separableClosure F E ≤ L :=
  fun x hx ↦
  by
  obtain ⟨y, rfl⟩ := h.inseparable' _ <| IsSeparable.tower_top L (mem_separableClosure_iff.1 hx)
  exact y.2

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