le_separableClosure' — Mathlib

English

If every element of an intermediate field L is separable over F, then L ≤ separableClosure F E.

Русский

Если каждый элемент поля L над F является разделимым, тогда L ⊆ separableClosure F E.

LaTeX

$$∀ x ∈ L, IsSeparable F x ⇒ L ≤ separableClosure F E$$

Lean4

/-- An intermediate field of `E / F` is contained in the separable closure of `F` in `E`
if all of its elements are separable over `F`. -/
theorem le_separableClosure' {L : IntermediateField F E} (hs : ∀ x : L, IsSeparable F x) : L ≤ separableClosure F E :=
  fun x h ↦ by simpa only [IsSeparable, minpoly_eq] using hs ⟨x, h⟩

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