le_separableClosure — Mathlib

English

A separable intermediate field L of E over F is contained in the separable closure of F in E.

Русский

Разделимое промежуточное поле L над F содержится в separableClosure F E.

LaTeX

$$L ≤ separableClosure F E$$

Lean4

/-- An intermediate field of `E / F` is contained in the separable closure of `F` in `E`
if it is separable over `F`. -/
theorem le_separableClosure (L : IntermediateField F E) [Algebra.IsSeparable F L] : L ≤ separableClosure F E :=
  le_separableClosure' F E (Algebra.IsSeparable.isSeparable F)

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