isNormalClosure_normalClosure — Mathlib

English

If K/F is algebraic and L is any extension, then the IsNormalClosure F K (normalClosure F K L) holds, i.e., the normal closure over the next stage is itself normal.

Русский

Если K/F алгебраическое, то IsNormalClosure F K (normalClosure F K L) выполняется; нормальное замыкание в следующем уровне нормально.

LaTeX

$$$IsNormalClosure\ F\ K\ (normalClosure\ F\ K\ L)$$$

Lean4

instance isNormalClosure_normalClosure [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] :
    IsNormalClosure F K (normalClosure F K L) := by
  have ⟨φ⟩ := ne
  apply (h.toIsAlgebraic.of_injective φ φ.injective).isNormalClosure_normalClosure
  simp_rw [← minpoly.algHom_eq _ φ.injective]
  exact fun _ ↦ h.splits _

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