le_separableClosure_iff — Mathlib

English

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

Русский

Промежуточное поле L содержится в separableClosure F E тогда и только тогда, когда L разделимо над F.

LaTeX

$$L ≤ separableClosure F E ↔ Algebra.IsSeparable F L$$

Lean4

/-- An intermediate field of `E / F` is contained in the separable closure of `F` in `E`
if and only if it is separable over `F`. -/
theorem le_separableClosure_iff (L : IntermediateField F E) : L ≤ separableClosure F E ↔ Algebra.IsSeparable F L :=
  ⟨fun h ↦ ⟨fun x ↦ by simpa only [IsSeparable, minpoly_eq] using h x.2⟩, fun _ ↦ le_separableClosure _ _ _⟩

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