normalClosure_eq_self — Mathlib

English

The normal closure in E/F of the separable closure of F in E is equal to the separable closure itself.

Русский

Нормальное замыкание в E/F от separableClosure F E равно сам separableClosure F E.

LaTeX

$$normalClosure F (separableClosure F E) E = separableClosure F E$$

Lean4

/-- The normal closure in `E/F` of the separable closure of `F` in `E` is equal to itself. -/
theorem normalClosure_eq_self : normalClosure F (separableClosure F E) E = separableClosure F E :=
  le_antisymm
    (normalClosure_le_iff.2 fun i ↦
      have : Algebra.IsSeparable F i.fieldRange := (AlgEquiv.Algebra.isSeparable (AlgEquiv.ofInjectiveField i))
      le_separableClosure F E _)
    (le_normalClosure _)

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